Stanford Encyclopedia of Philosophy
This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Connexive Logic

First published Fri Jan 6, 2006; substantive revision Tue Oct 10, 2006

Connexive logic is a comparatively little-known and to some extent neglected branch of nonclassical logic. Systems of connexive logic are neither subsystems nor extensions of classical logic. Connexive logics have a standard logical vocabulary and comprise certain non-theorems of classical logic as theses. Since classical propositional logic is Post-complete, any additional axiom in its language gives rise to the trivial system, so that any non-trivial system of connexive logic will have to leave out some theorems of classical logic. The name ‘connexive logic’ suggests that systems of connexive logic are motivated by some ideas about coherence or connection between premises and conclusions of valid inferences or between formulas of a certain shape. The kind of coherence in question concerns the meaning of implication and negation. One basic idea is that no formula provably implies or is implied by its own negation. This conception may be expressed by requiring that for every formula A,

⊬ ~A → A and ⊬ A → ~ A,

but usually the underlying intuitions are expressed by requiring that certain schematic formulas are theorems:

AT: ~(~A →A) and
AT′: ~(A→ ~A).

The first formula is often called Aristotle's Thesis. If this non-theorem of classical logic is found plausible, then the second principle, AT′, would seem to enjoy the same degree of plausibility. Indeed, also AT′ is sometimes referred to as Aristotle's Thesis. As McCall (1975, 435) explains,

[c]onnexive logic may be seen as an attempt to formalize the species of implication recommended by Chrysippus:
And those who introduce the notion of connection say that a conditional is sound when the contradictory of its consequent is incompatible with its antecedent. (Sextus Empiricus, translated in Kneale and Kneale 1962, p. 129.)

Using intuitionistically acceptable means only, the pair of theses AT and AT′ is equivalent in deductive power with another pair of schemata, which in established terminology are called (Strong) Boethius' Theses and which may be viewed (in addition with their converses) as capturing Chrysippus' idea:

BT: (A →B) → ~(A → ~B) and
BT′: (A→ ~B) → ~ (A→B).

The names ‘Aristotle's Theses’ and ‘Boethius' Theses’ are, of course, not arbitrarily chosen. AT, for example, is assumed at Aristotle's Prior Analytics 57b3, where it is explained that:

[I]t is impossible that the same thing should be necessitated by the being and by the not-being of the same thing. I mean, for example, that it is impossible that B should necessarily be great since A is white and that B should necessarily be great since A is not white.

Moreover, Boethius, for instance, holds that ‘if A then ~B’ is the negation of ‘if A, then B’ (Kneale and Kneale 1962, p. 191). Additional historical remarks may be found in Kneale and Kneale 1962, Priest 1999, and Nasti De Vincentis 2006.

Let L be a language containing a unary connective ~ (negation) and a binary connective → (implication). A logical system in a language extending L is called a connexive logic, if AT, AT′, BT, and BT′ are theorems and, moreover, (A→B) → (B→A) fails to be a theorem (so that → can hardly be understood as a bi-conditional). The connective → in a system of connexive logic is said to be a connexive implication.

Routley (1978) suggested a narrower conception of connexive logic. If the requirement of a connection between antecedent and succedent of a valid implication is understood as a content connection, and if a content connection obtains if antecedent and succedent are relevant to each other, then "the general classes of connexive and relevant logics are one and the same" (Routley 1978, p. 393). Since every non-trivial system of connexive logic has to omit some classical tautologies, and since the standard paradoxes of non-relevant, material implication can be avoided by rejecting Conjunctive Simplification, i.e., (A ∧ B) → A and (A ∧ B) → B, Routley requires for a connexive logic the rejection or qualification of Conjunctive Simplification (or equivalent schemata). If the contraposition rule and uniform substitution are assumed, the combination of Conjunctive Simplification and Aristotle's Theses results in inconsistency, see, for example, Thompson 1991. Mortensen (1984) pointed out that there are inconsistent but non-trivial systems satisfying both AT′ and Simplification. Examples of non-trivial inconsistent systems of connexive logic satisfying Conjunctive Simplification are presented in Sections 1.4 and 1.5.

Motivation for systems of connexive logic not only comes from considerations about a content connection between antecedent and succedent in valid implications, but also from more instrumental considerations. In MacCall 1967, connexive implication is motivated by reproducing in a first-order language all valid moods of Aristotle's syllogistic. In particular, the classically invalid inference from ‘All A is B’ to ‘Some A is B’ is obtained by translating ‘Some A is B’ as ∃x(~(A(x) → ~B(x)), where → is a connexive implication. In Wansing 2007 connexive implication is motivated by introducing a negation connective into Categorial Grammar in order to express negative information about membership in syntactic categories.

1. Systems of connexive logic

1.1 Algebraic connexive logic

Whereas the basic ideas of connexive logic are traced back to antiquity, the search for formal systems with connexive implication seems to have begun only in the 19th century in the work of H. MacColl (1878). The more recent formal study of systems of connexive logic started in the 1960s. In McCall 1966, S. McCall presented an axiomatization of a system of propositional connexive logic introduced by Angell (1962) in terms of certain four-valued matrices. The language of McCall's logic CC1 contains as primitive (notation adjusted) a unary connective ~ (negation) and the binary connectives ∧ (conjunction) and → (implication). Disjunction ∨ and equivalence ↔ are defined in the usual way. The schematic axioms and the rules of CC1 are as follows:

A1 (A →B) → ((B → C) → (A → C))
A2 ((A →A) →B) → B
A3 (A→B) → ((A ∧ C) → (B ∧ C))
A4 (A ∧ A) → (B → B)
A5 (A ∧ (B ∧ C)) → (B ∧ (A ∧ C))
A6 (A ∧ A) → ((A → A) → (A ∧ A))
A7 A → (A ∧ (A ∧ A))
A8 ((A → ~B) ∧ B) → ~A
A9 (A ∧ ~(A ∧ ~B)) → B
A10 ~(A ∧ ~(A ∧ A))
A11 (~A ∨ ((A → A) →A)) ∨ (((A → A) ∨ (A → A)) → A)
A12 (A →A) → ~(A → ~ A)
R1 if ⊢ A and ⊢ (A → B), then ⊢ B (modus ponens)
R2 if ⊢ A and ⊢ B, then ⊢ (A ∧ B) (adjunction)

Among these axiom schemata, only A12 is supraclassical. The system CC1 is characterized by the following four-valued truth tables with designated values 1 and 2:

~
1 4
2 3
3 2
4 1
∧ 1 2 3 4
1 1 2 3 4
2 2 1 4 3
3 3 4 3 4
4 4 3 4 3
→ 1 2 3 4
1 1 4 3 4
2 4 1 4 3
3 1 4 1 4
4 4 1 4 1

McCall emphasizes that the logic CC1 is only one among many possible systems satisfying the theses of Aristotle and Boethius. Although CC1 is a system of connexive logic, its algebraic semantics appears to be only a formal tool with little explanatory capacity. In CC1, the constant truth functions 1, 2, 3, and 4 can be defined as follows (McCall1966, p. 421): 1 := (p →p), 2 := ~(p ↔ ~p)}, 3 := (p ↔ ~p), 4 := ~(p→p), for some sentence letter p. As Routley and Montgomery (1968, p. 95) point out, CC1 "can be given a semantics by associating the matrix value 1 with logical necessity, value 4 with logical impossibility, value 2 with contingent truth, and value 3 with contingent falsehood. However, many anomalies result; e.g. the conjunction of two contingent truths yields a necessary truth". Moreover, McCall points out that CC1 has some properties that are difficult to justify, if the name ‘connexive logic’ is meant to reflect the fact that in a valid implication A→ B there exists some form of connection between the antecedent A and the succedent B. Axiom A4, for example, is bad in this respect. On the other hand, CC1 might be said to undergenerate, since (A ∧ A) → A and A → (A ∧ A) fail to be theorems of CC1. Routley and Montgomery (1968) showed that the addition of the latter formulas to only a certain subsystem of CC1 leads to inconsistency.

These observations may well have distracted many non-classical logicians from connexive logic. If the validity of Aristotle's and Boethius' Theses is distinctive of connexive logics, it is, however, not quite clear how damaging the above criticism is. In order to construct a more satisfactory system of connexive logic, McCall (1975) defined the notions of a connexive algebra and a connexive model and presented an axiom system CFL that is characterized by the class of all connexive models. In the language of CFL, however, every implication is first-degree, i.e., no nesting of → is permitted. McCall refers to a result by R. Meyer showing that the valid implications of CFL form a subset of the set of valid material equivalences and briefly discusses giving up the syntactic restriction to first-degree implication. In summary, it seems fair to say that as the result of the investigations into connexive logic in the 1960s and 1970s, connexive logic, its ancient roots notwithstanding, appeared as a sort of exotic branch of non-classical logic.

1.2 Connexive logic based on ternary frames for relevance logics

In the late 1970s and the 1980s, connexive logic was subjected to semantical investigations based on ternary frames for relevance logics. Routley (1978) obtained a semantic characterization of Aristotle's Thesis AT′ and Boethius' Thesis BT using a ‘generation relation’ G between a formula A and a possible world s. The semantics employs model structures F = <T, K, R, S, U, G, *>, where K is a non-empty set of possible worlds, T ∈ K is a distinguished world (the ‘real world’), R, S, and U are ternary relations on K, G is a generation relation, and * is a function on K mapping every world s to its ‘opposite’ or ‘reverse’ s*. A valuation is a function v that sends pairs of worlds and propositional variables into {0,1}, satisfying the following heredity condition: if R(T, s, u) and v(p, s) = 1, then v(p, u) = 1. Intuitively, G(A, t) is supposed to mean that everything that holds in world t is implied by A. A model is a structure M = <F, v>. The relation M, t ⊨ A (A is true at t in M) is inductively defined as follows:

M, t ⊨ p iff v(p, t) = 1
M, t ⊨ ~A iff M, t* ⊭ A
M, t ⊨ (A ∧ B) iff there are s, u with Stsu M, s ⊨ A and M, u ⊨ B
M, t ⊨ (A ∨ B) iff there are s, u with Utsu M, s ⊨ A or M, u ⊨ B
M, t ⊨ (A → B) iff for all s, u if Rtsu and M, s ⊨ A, then M, u ⊨ B

[Note: whenever there is little chance for ambiguity, we replace R(x, y, z) by Rxyz.]

Moreover, it is required that for every formula A and world t, G(A, t) implies M, t ⊨ A. A formula A is true in model M iff M, T ⊨ A, and A is valid with respect to a class of models, if A is true in all models from that class. AT′ is semantically characterized by the following property of models: ∃t (R(T*, t, t*) and G(A, t)), and BT is characterized by ∀w∃s, t, u (R(w, s, t), R(w*, s, u), G(A, s), and R(T, t, u*)).

Mortensen (1984), who considers AT′, explains that Routley's characterization of AT′ is "not particularly intuitively enlightening" and points out that in certain logics with a ternary relational models semantics another characterization of AT′ is available, namely the condition that for every model M the set CA := {s : M, s ⊨ A and M, s ⊭ ~A} is non-empty. Like Routley's non-recursive requirement that G(A, t) implies M, t ⊨ A, Mortensen's condition is not a purely structural condition, since it mentions the truth relation ⊨. Mortensen (1984, p. 114) maintains that the condition CA ≠ ∅ "is closest to the way we think of Aristotle", and emphasizes that for a self-inconsistent proposition A, the set CA must be empty, whence AT′ is to be denied. Mortensen also critically discusses the addition of AT′ to the relevance logic E. In this context, AT′ amounts to the condition that no implication is true at the world T*.

A more regular semantics for extensions of the basic relevance logic B by either AT′ or BT has been presented in (Brady 1989). In this semantics, conjunction is defined in the standard way, and there is a subset of worlds O ⊆ K. The extended model structures contain a function ℑ that maps sets of worlds, and in particular, interpretations of formulas (alias propositions) I(A) to sets of worlds in such a way that a formula A is true at a world t iff t ∈ ℑ(I(A)). This allows Brady to state model conditions capturing AT′ and BT as follows:

AT′: If t ∈ O, then (∃x, y ∈ ℑ(f)) Rt*xy* , for any proposition f;

BT: (∃x,y ∈ ℑ(f)) (∃z ∈ K) (Rtxz and Rt*yz*), for any proposition f and any t ∈ K.

Note that these clauses still are not purely structural conditions but conditions on the interpretation of formulas. Also the investigations into connexive logics based on ternary frames did not, as it seems, lead to establishing connexive logic as a fully recognized branch of non-classical logic.

1.3 Connexive logic based on subtraction negation

A close relation between connexive logic and the idea of negation as cancellation has been observed by Routley (1978), Routley et al. (1982), and Routley and Routley (1985). However, whereas Routley suggested the semantics using a generation relation, connexive logics based in a straightforward way on the cancellation view of negation have been worked out by Priest (1999). Negation as cancellation (alias subtraction negation) is a conception of negation that can be traced back to Aristotle's Prior Analytics and is often associated with Strawson, who held that a "contradiction cancels itself and leaves nothing" (1952, p. 3). (The idea of ex contradictione nihil sequitur is also discussed in Wagner 1991.) The connection between the subtraction account of negation and the principles distinctive of connexive logic is explained by Routley and Routley (1985, p. 205) as follows:

Entailment is inclusion of logical content. So, if A were to entail ~A, it would include as part of its content, what neutralizes it, ~A, in which event it would entail nothing, having no content. So it is not the case that A entails ~A, that is Aristotle's thesis ~(A → ~A) holds.

Priest (1999) directly translates a definition of entailment that enforces the null-content account of contradictions into evaluation clauses. A model is a structure M = <W, g, v>, where W is a non-empty set of possible worlds, g is a distinguished element from W, and v is a valuation function from the set of propositional variables into the set of classical truth values {1, 0}. Two clauses for evaluating implications at possible worlds are considered (notation adjusted):

(a) M, s ⊨ A → B iff (i) there is a world u with M, u ⊨ A and (ii) for every world u, M, u ⊨ A then M, u ⊨ B;
(b) M, s ⊨ A → B iff (i) there is a world u with M, u ⊨ A, (ii) there is a world u with M, u ⊭ B, and (iii) for every world u, M, u ⊨ A then M, u ⊨ B.

Condition (i) ensures that nothing is implied by an unsatisfiable antecedent. The evaluation clauses for the other connectives are classical. A formula A is true in a model (M ⊨ A) iff M, g ⊨ A; and A is valid if A is true in every model. Condition (ii) ensures that the law of contraposition is valid. A set Δ of formulas is true in a model iff every element of Δ is true in the model.

There are two notions of entailment (Δ ⊨ A), one coming with clause (a) the other with clause (b):

(a) Δ⊨ A iff Δ is true in some model, and every model in which Δ is true is a model in which A is true;
(b) Δ⊨ A iff Δ is true in some model, ~A is true in some model, and every model in which Δ is true is a model in which A is true.

These two connexive logics arise from the idea of negation as cancellation in a straightforward way. They are neither monotonic nor closed under uniform substitution. Proof systems and decision procedures for them can be obtained from a straightforward faithful translation τ into the modal logic S5. For implications A → B the translation is defined as follows, where ⊃ is material implication and ¬ is classical negation:

(a) ◊τ(A) ∧ □(τ(A) ⊃ τ(B));
(b) ◊τ(A) ∧ ◊¬τ(B) ∧ □(τ(A) ⊃ τ(B)).

Although the semantics of Priest's connexive logics is simple and transparent, the underlying idea of subtraction negation is not unproblematic. Priest (1999, p. 146) mentions strong fallibilists who "endorse each of their views, but also endorse the claim that some of their views are false". Their contradictory opinions in fact hardly are contentless, so that the cancellation account of negation and, as a result, systems of connexive logic based on subtraction negation appear not to be very well-motivated.

1.4 Four-valued constructive connexive logic

A system of connexive logic with an intuitively plausible possible worlds semantics using a binary relation has been introduced in Wansing 2005. In this paper it is observed that a modification of the falsification conditions for negated implications in possible worlds models for David Nelson's constructive four-valued logic with strong negation results in a connexive logic, called C, which inherits from Nelson's logic an interpretation in terms of information states pre-ordered by a relation of possible expansion of these states. For Nelson's constructive logics see, for example, (Almukdad and Nelson 1984, Gurevich 1977, Nelson 1949, Odintsov 2003, Routley 1974, Thomason 1969, Wansing 2001).

The key observation for obtaining C is simple: in the presence of the double negation introduction law, it suffices to validate both BT′ and its converse ~(A → B) → (A → ~B). In other words, an interpretation of the falsification conditions of implications is called for, which deviates from the standard conditions. In Nelson's systems of constructive logic, the double negation laws hold, and the relational semantics for these logics is such that falsification and verification of formulas are dealt with separately. However, the falsification conditions of implications are the classical ones expressed by the schema ~(A → B) ↔ (A ∧ ~B). To obtain a connexive implication, it is therefore enough to assume another interpretation of the falsification conditions of implications expressed by ~(A → B) ↔ (A → ~B).

Consider the language L := {∧, ∨, →, ~} based on the denumerable set AtL of propositional variables. Equivalence ↔ is defined as usual. The schematic axioms and rules of the logic C are:

a1 the axioms of intuitionistic positive logic
a2 ~ ~A ↔ A
a3 ~(A ∨ B) ↔ (~A ∧ ~B)
a4 ~(A ∧ B) ↔ (~A ∨ ~B)
a5 ~(A → B) ↔ (A → ~ B)
R1 modus ponens

Clearly, a5 is the only supraclassical axiom of C. The consequence relation ⊢C (derivability in C) is defined as usual. A C-frame is a pair F = <W, ≤ >, where ≤ is a reflexive and transitive binary relation on the non-empty set W. Let <W, ≤ >+ be the set of all X ⊆ W such that if u ∈ X and u ≤ w, then w ∈ X. A C-model is a structure M = <W, ≤, v+, v− >, where <W, ≤ > is a C-frame and v+ and v− are valuation functions from AtL into <W, ≤ >+ . Intuitively, W is a set of information states. The function v+ sends an atom p to the states in W that support the truth of p, whereas v− sends p to the states that support the falsity of p. M = <W, ≤, v+, v− > is said to be the model based on the frame <W, ≤ >. The relations M, t ⊨+ A (M supports the truth of A at t) and M, t ⊨− A (M supports the falsity of A at t) are inductively defined as follows:

M, t ⊨+ p iff t ∈ v+(p)
M, t ⊨− p iff t ∈ v−(p)
M, t ⊨+ (A ∧ B) iff M, t ⊨+ A and M, t ⊨+ B
M, t ⊨− (A ∧ B) iff M, t ⊨− A or M, t ⊨− B
M, t ⊨+ (A ∨ B) iff M, t ⊨+A or M, t ⊨+ B
M, t ⊨− (A ∨ B) iff M, t ⊨− A and M, t ⊨− B
M, t ⊨+ (A→ B) iff for all u ≥ t (M, u ⊨+ A implies M, u ⊨+ B)
M, t ⊨− (A→ B) iff for all u ≥ t (M, u ⊨+ A implies M, u ⊨− B)
M, t ⊨+ ~A iff M, t ⊨− A
M, t ⊨− ~A iff M, t ⊨+ A

If M = <W, ≤, v+, v− > is a C-model, then M ⊨ A (A is valid in M ) iff for every t ∈ W, M, t ⊨+ A. F ⊨ A (A is valid on F) iff M ⊨ A for every model M based on F. A formula is C-valid iff it is valid on every frame. Support of truth and support of falsity for arbitrary formulas are persistent with respect to the relation ≤ of possible expansion of information states. That is, for any C-model M = <W, ≤, v+, v− > and formula A, if s ≤ t, then M, s ⊨+ A implies M, t ⊨+ A and M, s ⊨− A implies M, t ⊨− A. It can easily be shown that a negation normal form theorem holds. The logic C is characterized by the class of all C-frames: for any L-formula A, ⊢C A iff A is C-valid. Moreover, C satisfies the disjunction property and the constructible falsity property. If ⊢C A ∨ B, then ⊢C A or ⊢C B. If ⊢C ~(A ∧ B), then ⊢C ~ A or ⊢C ~B. Decidability of C follows from a faithful embedding into positive intuitionistic propositional logic.

Like Nelson's four-valued constructive logic N4, C is a paraconsistent logic. Note that C contains contradictions, for example: ⊢C ((p ∧ ~ p) → (~ p ∨ p)) and ⊢C ~((p ∧ ~p) → (~ p ∨ p)). It is obvious from the above presentation that C differs from N4 only with respect to the falsification (or support of falsity) conditions of implications. As in N4, provable strong equivalence is a congruence relation, i.e., the set {A : ⊢C A} is closed under the rule A ↔ B, ~ A ↔ ~ B / C(A) ↔ C(B). Wansing (2005) also presents a first-order extension QC of C.

Whereas the direction from right to left of Axiom a5 can be justified by rejecting the view that if A implies B and A is inconsistent, A implies any formula, in particular B, the direction from left to right seems rather strong. If the verification conditions of implications are dynamic (in the sense of referring to other states in addition to the state of evaluation), then a5 indicates that the falsification conditions of implications are dynamic as well. The falsity of (A → B) thus implies that if A is true, B is false. Yet, one might wonder why it is not required that the falsity of (A→ B) implies that if A is true, B is not true. This cannot be expressed in a language with just one negation ~ expressing falsity instead of absence of truth (classically at the state of evaluation or intuitionistically at all related states). If one adds to C the further axiom ~A → (A → B) to obtain a connexive variant of Nelson's three-valued logic N3, intuitionistic negation ¬ is definable by setting: ¬A := A → ~A. Then a5 might be replaced by

a5′: ~(A → B) ↔ (A → ¬ B).

The resulting system satisfies AT, AT′, BT, and BT′, because A → ¬ ~A and ~A → ¬A are theorems. For BT, for example, we have:

1. A→ B assumption
2. B → ¬ ~B theorem
3. A → ¬ ~B 1, 2, transitivity of →
4. (A → ¬ ~B) → ~(A → ~B) axiom a5′
5. ~(A → ~B) 3, 4, R1
6. (A→ B) → ~(A → ~ B) 1, 5, deduction theorem

This logic, however, is the trivial system (a fact not noticed in (Wansing 2005, Section 6)).

1.5 Material connexive logic

If implications A → B are understood as material implications, then a separate treatment of falsity conditions again allows introducing a system of connexive logic. The resulting system MC may be called a system of material connexive logic. The semantics is quite obvious: a model M is just a function from the set of all literals, i.e., atomic formulas or negated atomic formulas, into the set of classical truth values {1, 0}. Truth of a formula A in a model M (M ⊨ A) is inductively defined as follows:

M ⊨ p iff v(p) = 1
M ⊨ (A ∧ B) iff M ⊨ A and M ⊨ B
M ⊨ (A ∨ B) iff M ⊨ A or M ⊨ B
M ⊨ (A → B) iff M ⊭ A or M ⊨ B

M ⊨ ~p iff v(~p) = 1
M ⊨ ~ ~A iff M ⊨ A
M ⊨ ~(A ∧ B) iff M ⊨ ~A or M ⊨ ~B
M ⊨ ~(A ∨ B) iff M ⊨ ~A and M ⊨ ~B
M ⊨ ~ (A → B) iff M ⊭ A or M ⊨ ~B

A formula is valid iff it is true in all models. The set of all valid formulas is axiomatized by the following set of axiom schemata and rules:

a1c the axioms of classical positive logical
a2 ~ ~A ↔ A
a3 ~(A ∨ B) ↔ (~A ∧ ~B)
a4 ~(A ∧ B) ↔ (~A ∨ ~B)
a5 ~(A → B) ↔ (A → ~B)
R1 modus ponens

MC can be faithfully embedded into positive classical logic, whence MC is decidable. The classical tautology ~(A → B) → (A ∧ ~B) is, of course, not a theorem of MC. Like C, MC is a paraconsistent logic containing contradictions.

2. Connexive logics and consequential logics

Aristotle's and Boethius' Theses express, as it seems, some pre-theoretical intuitions about meaning relations between negation and implication. But it is not clear that a language must contain only one negation operation and only one implication. The three-valued constructive connexive logic of Section 1.5 contains two negations, and the language of systems of consequential implication comprises two implication connectives together with one negation, see (Pizzi 1977, 1991, 1993, 1996). In (Pizzi and Williamson 1997), the notion of a normal system of analytic consequential implication is defined. ‘Normal’ here means that such a system contains certain formuals and is closed under certain ruels. The smallest normal consequential logic that satisfies AT is called CI. Alternatively, CI can be characterized as the smallest normal system that satisfies Weak Boethius' Thesis:

(A → B) ⊃ ¬(A → ¬ B),

where → is consequential implication, ⊃ is material implication, and ¬ is classical negation. Pizzi and Williamson show that CI can be faithfully embedded into the normal modal logic KD, and vice versa. Analytic consequential implication is interpreted according to the following translation function φ:

φ(A→ B) = □(φA ⊃ φB) ∧ (□φB ⊃ □φA) ∧ (◊φB ⊃ ◊φA)

As Pizzi and Williamson (1997, 571) point out, their investigation is a "contribution to the modal treatment of logics intermediate between logics of consequential implication and connexive logics." They emphasize a difficulty of regarding consequential implication as a genuine implication connective by showing that in any normal system of consequential logic that admits modus ponens for consequential implication and contains BT, the following formulas are provable:

(a) (A → B) ≡ (B → A),

(b) (A → B) ≡ ¬(A → ¬B),

where ≡ is classical equivalence. Since (A → B) ↔ ~(A → ~B) is a theorem of C, the more problematic fact, from the point of view of this system, is the provability of (a). Pizzi and Williamson also show that in any normal system of consequential logic that contains BT, the formula (A → B) ≡ (A ≡ B) is provable, if (A → B) ⊃ (A ⊃ B) is provable, in other words, consequential implication collapses into classical equivalence if (A → B) ⊃ (A ⊃ B) is provable.

3. Summary

In summary, it may be said that connexive logic, although it is not very well-known and unusual in various respects, is not just a formal game. There are several kinds of systems of connexive logics with different kinds of semantics and proof systems. (A dialogical treatment of connexive logic may be found in (Rahman and Rückert, 2001).) The intuitions captured by systems of connexive logic can be traced back to ancient roots, and applications of connexive logics range from Aristotle's syllogistic to Categorial Grammar. A recent monograph developing a system of connexive logic in the context of solving a braod range of paradoxes is (Angell, 2002).

Bibliography

Other Internet Resources

[Please contact the author with suggestions.]

Related Entries

logic: modal | logic: paraconsistent | logic: relevance | type theory: constructive