However, system E is afflicted with a number of shortcomings. Several of them have already been pointed at both by the deep relevantist school headed by Richard Sylvan in [RLR] and in many other places -- as well as by the already mentioned Méndez and Avron. Other among the shortcomings have not been emphasized yet.
Let me enumerate some of those drawbacks. First and foremost, the Adjunction rule -- Adj for short -- (namely «p», «q» ∴ «p∧q») is introduced as an additional primitive inference-rule, with no justification, but, worse than that, it is in fact crippled in any natural-deduction implementation of the system -- in fact the rule applies only within the domain of logic, the system failing to allow a general application of the rule in virtue of which from any two premises «p» and «q» the conclusion «p∧q» could be drawn. Any application of system E to a non-logical theory will have to fall back on accepting only one nonlogical axiom of the theory, which will be the conjunction of all its «ordinary» axioms. To that extent, system E is in a very appropriate sense a non-conjunctive or non-copulative system, even though it falls short of renouncing Adj altogether as do other paraconsistent systems (Jaskowski's discussive logic (see [Cos&Dub]) or Rescher & Brandom's modal approach (see [Res&Bra]).
Moreover, the core motivation of entailmental logic was the Entailment Principle ([And&Bel], pp. 277-8), viz. that an inference of «p» from premises «q¹», «q²», ..., «qn» is valid iff «r→p» is a logical theorem, where «r» is the conjunction of «q¹», «q²», ..., «qn». Thus, system E -- unlike «deep» relevant logics -- countenances Conjunctive Assertion («p→q∧p→q»). But without a full-fledged or unshackled Adj we cannot in general conclude «p→q∧p» from «p→q» and «p». Thus, E debars us from applying the Entailment Principle in ou inferring practice, i.e. to first draw from from {«p→q», «p»} the conclusion «p→q∧p» and then from that conjunction alone to infer «q».
Furthermore, system E postulates a principle of distributivity which also causes serious trouble for the natural-deduction and Gentzen implementations of the system (see [Dunn]), and which anyway is sufficiently convoluted to deserve being a proved theorem rather than postulated as an axiom.
No less surprising is the failure of Factor, a principle investigated by R. Sylvan. (On this point, my arguments borrow from [Syl&Urb], which is the main extant study of Factor.) Factor is «p→q→.p∧r→.q∧r». Due to lack thereof, system E does not allow us to conclude that heads of horses are heads of animals from the premise that horses are animals. For let `p' mean `x is a horse'; `q', `x is an animal'; `r', `z is x's head'; then the wanted inference would be: ∀x(p→q) ∴∀x(∃z(p∧r)→∃z(q∧r)); but within a quantificational extension of E we can prove only this: ∀x,z(p→q∧.r→r)) ∴ ∀x(∃z(p∧r)→∃z(q∧r). (The axioms for introducing quantifiers are unproblematic.) In other words, we cannot simply assume that what is a creature's head is its head; we need to state it as an additional premise, despite its being a logical theorem. Likewise, lack of Factor entails that set theory is going to become useless; for define inclusion, `x⊂z', as `∀u(u∈x→u∈z)'; then without Factor we'll lose the following set-theoretical principles: «x⊂z→∀v(x∩v⊂z∩v)»; «x=z→∀u(u∩x=u∩z)», with equality defined as mutual inclusion; and even if we lay down the principle of extensionality, «∀x,z(x=z→∀v(x∈v→z∈v))», we'll be -- without Factor -- unable to conclude that «x=z→.p[x]→p[x/z]» (let `p' be, e.g., `x∈u∧u∈y'). On the other hand, laying down extensionality in the stronger version of the schema «∀x,z(x=z→.p[x]→p[x/z])» yields «x=z→.p→p», even with no occurrence of `x' in `p'; which is precisely a set-theoretical version of what A&B tried to avoid by banning Factor, namely «p→q→.r→r».
Interestingly, Factor is -- not just when added to E but even upon much weaker systems of «deep relevant logic» -- tantamount to Inclusion, namely the principle «p→qI.p∧qIp», where `I' is mutual implication. The rationale for Inclusion is that «p» implies «q» iff the «content» of «q» is included in that of «p», i.e. iff «p» is equivalent to «p∧q» -- so that by reaching «q» you are only expressing something implicitly contained in «p». Such an idea has been widely invoked in support of relevant logic. And yet only extremely weak relevant logics can admit of Factor (or Inclusion); for, if a logic has MP, Adj, the transitivity rule («p→q», «q→r» ∴ «p→r»), Commutativiy of both disjunction and conjunction, Addition («p→.p∨q») and Simplification («p∧q→p»), then, if it has either Idempotence of either conjunction («p→.p∧p») or disjunction («p∨p→p»), or else mutual Distributivity, it has as a theorem «p→p→.q→q». (See [Syl&Urb] again.)
Most of all, system E allows suppression (or omission) of proved entailments in exported form only, not in imported form. That is very odd, since A&B ([And&Bel], p.262 top) allege that omission is what leads to the erroneous law of exportation in CL. E bestows a privileged status to implicational formulae and countenances such principles as Suppression («p→p→q→q») and exported transitivity («p→q→.q→r→.p→r»), the only natural way of justifying which is to allow Exportation for implicational formulae, due to their special status -- something E falls short of accepting. Thus although from «p¹→p²→.q→r→s» -- provided «q→r» is a theorem -- we can deduce «p¹→p²→s», we cannot draw the conclusion from «p¹→p²∧(q→r)→s», even if «q→r» is a logical theorem. So «p→q∧(r→r)→s→.p→q→s» is not a theorem of E. Accordingly a conjunction of two implicative formulae is not to count as an implicative formula at all!
Although those different shortcomings may seem unrelated, in fact they arise from the same source: the weakened status of conjunction and the lack of what we can call interpolation axioms -- axioms, that is, which are simpler and through which the less obvious axioms of E would become provable theorems.
Taking as my starting point the considerations put forward above, I am going to propose a chain of strengthenings of system E which cure it from the anomalies. What is most interesting is that the emerging systems are clearly interpretable as logics of fuzziness or graduality. Thus the E functor `→', duly strengthened, receives an appealing construal as meaning `to the extent [at least] that'.
Provided with such a reading, the functor has to be stronger than the original E arrow, under natural assumptions concerning the structure of truth degrees.
So, the resulting systems are closer to CL (Classical Logic). They are not relevant, in the sense that they do not comply with the relevantist constraints, or at least not with the one of variable-sharing. They comply with the constraint of use in proof, with some adaptations. But that natural-deduction implementation lies beyond the scope of the present paper.
The resulting systems of fuzzy or gradualistic logic are intermediary between classical and entailmental logic. The approximation to CL goes further than that. In fact, several of the systems contain all of CL, and are indeed conservative extensions of CL. Only, the CL negation `¬' is given a different reading from what is customary. It is now read `not...at all'. Classical negation is complete negation -- the functor which maps anything true, to whatever extent, into complete falsehood, and the utterly false into complete truth. In some important sense, those systems are to CL as relevant logic was meant to be to intuitionistic logic.
All those systems have the laws of non-contradiction and excluded middle. They are paraconsistent copulative systems. I proceed to constructing the chain.
It can be proved that P8 contains P7; that P10 contains P9; that P9 contains P5; that P8 is a conservative extension of CL (if classical negation, `¬', is defined as `HN'), and that P5 and such systems as contain P5 are not just paraconsistent but contradictorial (they have the theorem of Heracleitus: «N(p→p)»). (In fact, «N(p→p)→(p→p)→(p→p)→N(p→p)→N(N(p→p)→(p→p)→(p→p)→N(p→p))» is a theorem of E; the apodosis is the negation of the protasis; when we add Aristotle or Boethius, the result is immediate: the negation of the theorem is also a theorem. But in P1 we prove «p∧Np→N(q→q)».)
Among all those systems, P5 and P10 are by far the most important ones. They are the most stable. The main motivation in going from P4 to P6 and up is to encompass CL within fuzzy logic, as the extreme case wherein it is a question of either complete falseness or not (alternatively of either complete truth or not). System P8 and those above it allow to implement classical conditional (which can be defined in the usual way with strong negation, `¬', and disjunction, `∨') in the relevantly recommended way: p⊃q iff there is some truth, namely α, such that p∧α→q.
A number of Hilbert style axiomatizations are provided below, which are more elegant than the genetic presentation just described. Here is an axiomatization for P5 with ten axioms and one primitive inference rule:
Primitive symbols:
`p', `q' etc are used as schematic letters. Notational conventions are à la Church: all two-place functors have the same weight and associate leftwards; a dot after a two-place functor stands for a left parenthesis with its mate as far to the right as possible.
Definitions:
Inference rule: DMP (i.e. disjunctive modus ponens): for n≥1:
p¹→q∨(p²→q)∨...∨.pn→q, p¹, ..., pn ∴ q
MP [Modus Ponens] is a particular case of the rule -- the one wherein n=1. Adj is a derived inference-rule.
The significance of DMP is that to deduce «q» from a number of premises is to show that «q» is deduced from at least one of them. Which does not mean that necessarily there is a proof from one of the premises alone, since the whole proof of the conclusion from the premises consists in showing that it either follows from the first premise, or from the second premise, and so on. Those deductions are not complete proofs, but proof-branches or alternative sub-proofs.
Five alternative axiomatizations of system P5 are now provided.
2d axiomatisation.
Same defintions and same inference-rule (DMP) as above.
3d axiomatisation.
Same definitions and same inference rule (DMP) as above.
4th axiomatisation.
Same definitions; same inference-rule (DMP).
5th axiomatisation.
Same definitions; same inference-rule (DMP). (The rule can be weakened to n≥2 alone, thanks to P5e05, i.e. IF -- taking as an instance thereof «p→q→q∨.p→q»; as much applies to any other formulation with the same disjunctive wording of the axiom, e.g. the 4th axiomatisation with P5d05. In that sense MP can be looked upon as enthymematic.)
6th axiomatisation
Primitives:
`t' is a new primitive (which is meant to be the conjunction of all implicative truths). `Θ' is a sentential constant whose meaning does not concern us here. Two inference rules: MP and Adj.
We then prove that «Θ↔t». In fact, we could use just one of those two primitives, except that for philosophical reasons it is better to prove their equivalence than to postulate it.
Upon the basis of P4 all the follwing are equivalent (and all of them bring about a collapse into CL):
Now we present an axiomatisation for P10 by adding to P5 the following axiom schemata (`H' is a one-place primitive functor, while «¬p» abbr «HNp» and «p⊃q» abbr «¬p∨q»):
Since in P10 we can prove Funnel (namely «p→q∨p»), IF (as it stands in all the foregoing formulations of P5 -- whether as such or as implicational Peirce, i.e. «p→q→p→p» provided «p» is implicational) becomes redundant. Thus a more elegant axiomatisation of P10 has to be found.
Here is a short list of theorem-schemata and rules which can be proved and derived, respectively, within P10:
It can be easily proved that the fragment of P10 in <∧,∨,⊃,¬> is exactly CL -- of which, therefore, P10 is a conservative extension. We had rather look upon P10 as the result of enlarging CL with new functors, a nonstrong negation, `N', and an implication, `→'. The intended sense is that «p→q» is true iff the degree of truth of «p» is smaller than or equal to that of «q», whereas «Np» is as true {false} as «p» is false {true} -- in other words, simple or natural negation reverses the order expressed by `→,' and that is all it does. In the present context we'd better read classical negation, `¬', as `not...at all'.
The existence of two conditionals (the mere conditional `&sup' and implication, `→') entails that there are in P10 two different deduction relations. We can keep `∴' as expressing mere inference, while using `||-' as expressing a stronger inference relation, namely: p¹, ..., pn ||-P10q iff «p¹...pn→q» is a theorem of P10; whereas for `∴' we do have the classical deduction metatheorem, viz. p¹, ..., pn, r ∴P10q iff p¹,...,pn ∴P10r⊃q -- theorems being such formulae as are ∴-inferred from an empty antecedent. Clearly if p||-q then p∴q. Our proof theory has to be implemented in such a way that those differences are taken into account.
Entailment, duly strengthened, is a functor sensitive to degree differences, whereas the mere conditional, `⊃', only takes into account whether formulae are completely false or not. CL is a poor system, not a wrong one. Its flaw consists in the fact that, by lacking an implication and a negation which are degree sensitive, CL compels people to think, legislate and act in terms of all or nothing -- since for all CL knows `wholly' and `just a little' are merely stylistic variations, with no semantic difference between its being altogether true that and its being [just] true.
Here is a semantic treatment of P5 and P10. By a P5-matrix we mean an algebra A=<A,O,D> where A is a well-ordered set of entities, D⊂A, and O is an ordered set of operations <N,∨,∧,→>, N being unary and the other binary and such that there are three elements ½, 0, 1 satisfying these postulates: 0 is the minimum; 1, the maximum; x∨z = max(x,z); x∧z = min(x,z); x≤z iff Nx≥Nz; N½=½; D is a proper filter such that ½∈D; x→z =: ½ if x≤z, and else 0; N0=1; NNx=x. Let T be an extension of P5. A valuation, v is a mapping from T into a P5-matrix, A, such that for any two formulae, «p», «q», the usual conditions are met: v(p∧q) = v(p)∧v(q), and the like for the remaining functors and operations. A formula «p» of T is valid iff every valuation, v, is such that v(p)∈D (the respective set of designated entities within its range). An inference (i.e. an ordered pair <C,«p»> where C is a set of formulae) is valid iff every valuation v such that, for every «q»∈C, v(q)∈D is such that v(p)∈D. Clearly, P5-matrices are Kleene algebras (i.e. Quasi-Boolean algebras satisfying the Kleene postulate that x∧Nx ≤ z∨Nz). In fact it is easily proved that each finite P5-matrix is isomorphic to one whose carrier is a finite subset of the set of the integers such that for every positive integer therein its negative also belongs, and conversely: the algebraic ½ will be the numeric zero, while the algebraic 1 will be the greatest number in the set. Soundness and completeness are straightforwardly proved. Notice, though, that none of those [finite] matrices is characteristic. But let us form an infinite P5-matrix, A∞, whose carrier comprises any infinite subset of the natural numbers, including zero, and their respective negatives, plus ∞ and -∞. Let D be [0,∞]. Then A∞ is characteristic in the sense that only all P5 theorems are mapped into designated elements, but it is not strongly characteristic in that there are valid inferences (with respect to A∞) which are not derivable in the system P5 (e.g. {«p»,«Np»,«q»,«Nq»} ∴ «p→q»). On the other hand, if we let the set of designated values to comprise all elements except -∞, there will be valid formulae which are not theorems of P5, e.g. «p→q∨p» (Funnel).
Let us form a P10-matrix by adding to a P5-matrix an additional unary operation, H, and additional elements, ω and α, such that: ω=Nα; x≥α if xØ0; Hx=: 1 if x=1, and else 0 (1 and 0 are the algebraic 1 and 0 respectively). A valuation is a mapping from a P10 theory T into a P10-matrix (we lay down that v(α)=α and so on). Now, not only are soundness and completeness attained but, more importantly, a strongly characteristic matrix becomes available: the set of all integers plus four additional elements, ∞> ω ≥ every integer; and of course every integer ≥ -ω = α > -∞, with D comprising all elements except -∞. That matrix is the canonic P10 matrix.
Thus P10 has the finite model property, namely that every [nondeliquescent, i.e. Post-consistent] non-conservative extension thereof has a finite characteristic matrix. For let L be such an extension of P10. There is a formula or a schema «p» within the vocabulary of P10 which is a theorem in L but not in P10. Let B and v be a P10 algebra and a valuation, respectively, such that v(p) is designated. The reason cannot be that the set of designated elements has been enlarged, of course. If the carrier of B is infinite, then B is isomorphic to the canonic matrix of P10. Therefore, B is finite. Which entails that for some natural number n L is P10 plus the Dugundji formula in n disjuncts, namely: «p¹↔p²∨....∨.p¹↔pn∨....∨.pn-¹↔pn». None of those formulae is a theorem of P10.
Most interestingly, when propositional quantifiers are used with the usual postulates for them (see [And_Bel_Dun], pp. 19ff), -- using `j' as a propositional variable -- we define «~p» as «p→∀jj», and «p⇒q» as «∃j(j∧p→q∧j)»; the fragment of the ensuing system, P10∃∀j, in <∧,∨,⇒,~> is exactly CL. In that sense, P10 is to CL precisely as E is to intuitionistic logic.Foot note 1_1
1. The research leading to this paper was developed mainly during my stay as a Visitor to the Australian National University in Canberra (from 01-11-1992 to 30-04-1993), thanks to a scholarship granted by the Spanish Ministry of Education. I owe my heartfelt appreciation to Richard Sylvan, whose friendly and supportive advice has a greater value than I can express here. My gratefulness, too, to Graham Priest, R.K. Meyer and J. Slaney for their helpful suggestions and comments. An ancestor of this paper was delivered at the Mini-Conference on Finite and Infinite Models and Related Issues, Canberra, April 4 1993.Back to main body of the paper