Connexive Logic

First published Fri Jan 6, 2006; substantive revision Fri Aug 8, 2014

Connexive logic is a comparatively little-known and to some extent neglected branch of non-classical 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 (see the entries on conditionals 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 57b14, where it is explained that:

It is impossible that if A, then not-A.

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, Nasti De Vincentis 2002, and McCall 2012, where McCall refers to ~((A →B) ∧ (~A →B)) as Aristotle's Second Thesis and, following Martin 2004, to ~((A →B) ∧ (A →~B)) as Abelard's First Principle. Aristotle's Second Thesis and Abelard's First Principle are interderivable with BT and with BT′ using intuitionistic principles only.

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. Kapsner (2012) refers to a logic that satisfies AT, AT′, BT, and BT′ and, moreover, satisfies the requirement that (a) in no model A→~A is satisfiable (for any A) and (b) in no model A→B and A→~B are simultaneoulsy satisfiable (for any A and B), as strongly connexive, whereas if the conditions (a) and (b) are not both satisfied, the system is only called weakly connexive.

1. Motivation

1.1 Connexivity and relevance

Routley (1978) suggested another 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), cf. also Serenac and Jennings 2003. 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, Woods 1968 and 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 2.4 and 2.5. The availablity of such connexive systems may be appreciated in view of the fact that Zermelo-Fraenkel set theory based on a system of connexive logic with Simplification is inconsistent, see Wiredu 1974.

The relation between connexive logic and relevance logic can also be seen as follows. Let A and B be contingent formulas of classical propositional logic, i.e., formulas that are neither constantly false nor constantly true. It is well-known that then the following holds:

  1. Not: ~A ⊢ A
  2. If A ⊢ B, then not: A ⊢ ~B
  3. If A ⊢ B, then A and B share some propositional variable (sentence letter)

If property (iii) is generalized to arbitrary formulas A and B, it is called the variable sharing property or variable sharing principle, which is generally seen as a necessary condition on a logic to count as a relevance logic (see the entry logic: relevance). So-called containment logics (also called Parry systems or systems of analytic implication, see Parry 1933, Anderson and Belnap 1975, Fine 1986, Ferguson 2014), satisfy the strong relevance requirement that if ⊢ A → B, then every propositional variable of B is also a propositional variable of A.

The variable sharing property indicates a content connection between A and B if B is derivable from A (or, semantically, A entails B). The properties (i) and (ii) may be viewed to express a content connection requirement on the derivability relation in a negative way. If one wants to express these constraints in terms of the provability of object language formulas, one naturally arrives at Aristotle's and Boethius' Theses.

1.2 Other Motivation

Motivation for systems of connexive logic not only comes from considerations about a content connection between antecedent and succedent in valid inferences or implications, but also from more instrumental considerations. In McCall 1967, connexive implication is motivated by reproducing in a first-order language all valid moods of Aristotle's syllogistic (see the entry on Aristotle's logic). 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 (see the entry on typelogical grammar). Consider, for example, the syntactic category (type) (n → s) of intransitive verbs, i.e., of expressions that in combination with a name (an expression of type n) result in a sentence (an expression of type s). The idea is that an expression is of type ~(n → s) iff in combination with a name it does not result in a sentence. In other words, an expression belongs to type ~(n → s) iff it is of type (n → ~s).

According to McCall (1975, p. 451), “[o]ne of the most natural interpretations of connexive implication is as a species of physical or “causal” implication,” and in McCall (2014) he argues that “[t]he logic of causal and subjunctive conditionals is … connexive, since ‘If X is dropped, it will hit the floor’ contradicts ‘If X is dropped, it will not hit the floor’.” Boethius' Thesis indeed appears on a list of principles every “precausal” connective should satisfy, see Urchs 1994. McCall (2012, p. 437), however, concedes that “causal logic is still very much an ongoing project, and no agreed-on formulation of it has yet been achieved.” Principles of connexive logic have been discussed in conditional logic (see the entry logic: conditional), beginning with Ramsey's (1929) comments on what is now called the Ramsey Test, as pointed out, e.g., in Ferguson 2012 and McCall 2012:

If two people are arguing “If p will q?” and are both in doubt as to p, they are adding p hypothetically to their stock of knowledge and arguing on that basis about q; so that in a sense “If p, q” and “If p, ~q” are contradictories“ (notation adjusted).

Abelard's First Principle, ~((A →B) ∧ (A →~B)), is considered as a principle of conditional non-contradiction and as such is endorsed by some philosophers, e.g., Gibbard (1981, p. 231), Lowe (1995, p. 47), and Bennett (2003, p. 84), without making any reference to connexive logic. Conditional non-contradiction fails, however, to be a valid principle in the semantics suggested by Stalnaker (1968) and Lewis (1973), cf. the discussion in Unterhuber 2013.

Another motivation for connexive logic has been presented by John Cantwell (2008) without noting that the introduced propositional logic is a system of connexive logic. Cantwell considers the denial of indicative conditionals in natural language and argues that the denial of, say, the conditional ‘If Oswald didn't kill Kennedy, Jack Ruby did.’ amounts to the assertion that if Oswald didn't shoot Kennedy then neither did Jack Ruby. This suggests that (A→~B) is semantically equivalent with ~(A→B).

Motivation taking up the idea of negation as cancellation and negation as falsity (cf. the entry on negation) is presented in Sections 2.3 and 2.4.

2. Systems of connexive logic

2.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), see also Rahman and Redmond 2008. The basic idea of connexive implication was spelled out also by E. Nelson (1930), and a 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. Meyer (1977) showed that the first-degree fragment of the normal modal logic S5 (and in fact every normal modal logic between KT and S5, cf. the entry logic: modal) and CFL are equivalent in the following sense: all theorems of CFL are provable in S5 if the connexive implication A→B is defined as □(A ⊃ B) ∧ (A ≡ B), where ⊃ and ≡ are classical implication and equivalence, respectively, and every first-degree theorem of S5 is provable in CFL if □A (“it is necessary that A”) is defined as (~p ∨ p)→A. 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.

More recently, Cantwell (2008) presented a truth table semantics for a system of connexive logic together with a proof-theoretical characterization. The truth tables for negation and implication are taken from Belnap 1970. Cantwell considers a language containing the constantly false proposition ⊥ and the following three-valued truth tables for negation, conjunction, disjunction, and implication with designated values T and − (where ‘T’ stands for truth and ‘F’ for falsity):

~
T F
F T
− −
∧ T F −
T T F −
F F F F
− − F −
∨ T F −
T T T T
F T F −
− T − −
→ T F −
T T F −
F − − −
− T F −

In this system, (A→~B) and ~(A→B) have the same value under every assignment of truth values to atomic formulas. Kaspner (2012) noticed that Cantwell's system, although it is weakly connexive, fails to be strongly connexive, whereas CC1 is strongly connexive.

McCall (2014) presents a cut-free sequent calculus for a system of connexive logic that he calls “connexive Gentzen.” The calculus has the non-standard feature of using pairs of axioms that are not logical truths. An annotation with subscripts is used to enable the elimination of dependencies on such non-standard axioms in the course of a derivation. The resulting system differs from CC1 in that p →(p ∧ p) and (p ∧ p)→ p are provable, and it is shown to be sound with respect to certain four-valued matrices. Sound and complete cut-free sequent calculi for certain constructive and modal connexive logics have been presented in Kamide and Wansing 2011, see Sections 2.4–2.6.

2.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.

2.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 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 iff 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, cf. the entry logic: modal. 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)).

Ferguson (2014) observes that the intersection of the semantical consequence relations of variant (a) of Priest's logic and the negation, conjuncton, disjunction fragment of Bochvar's 3-valued logic (cf. the entry logic: many-valued) results in a known system of containment logic, namely the system RC presented in Johnson 1976.

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.

2.4 Four-valued constructive connexive logic

A system of connexive logic with an intuitively plausible possible worlds semantics using a binary relation between worlds 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 2008, Routley 1974, Thomason 1969, Wansing 2001, Kamide and Wansing 2012.

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 (cf. the entry logic: paraconsistent). 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. Kamide and Wansing (2011) present a sound and complete sequent calculus for C and show the cut-rule to be admissible, which means that it can be dispensed with.

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) but pointed out in the online version of this paper).

The system C is a conservative extension of positive intuitionistic logic. In C, strong negation is interpreted in such a way that the intuitionistic implication of its negation-free sublanguage is a connexive implication. Analogously, strong negation may be added to positive dual intuitionistic logic to obtain a system with a connexive co-implication, and to bi-intuitionistic logic to obtain a system with both a connexive implication and a connexive co-implications, see Wansing 2008.

The systems C and QC are only weakly connexive, but this is not surprising because these logics are paraconsistent and allow formulas A and ~A to be simultaneously satisfiable in the sense that a state and all its possible expansions may support the truth of both A and ~A. As a result, A → ~A and ~A → A are satisfiable. If A → ~A and ~A → A are unsatisfiable, strong connexivity is in conflict with at the same time satisfying the deduction theorem and defining semantical consequence as preservation of support of truth: A → ~A would entail ~(A → ~A), ~A → A would entail ~(A → A), and the formulas (A → ~A) → ~(A → ~A) and (~A → A) → ~(~A →A) would be valid.

2.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.6 Connexive modal logics

In Wansing 2005, the language of the connexive logic C is extended by modal operators □ and ◊ (“it is possible that”) to define a connexive and constructive analogue CK of the smallest normal modal logic K. The system CK is shown to be faithfully embeddable into QC, to be decidable, and to enjoy the disjunction property and the constructible falsity property.

It is well-known that intuitionistic propositional logic can be faithfully embedded into the normal modal logic S4, which, like K, is based on classical propositional logic (cf. the entries logic: intuitionistic and logic: modal). There exists a translation γ, due to Gödel, such that a formula A of intuitionistic logic is intuitionistically valid iff A 's γ-translation is valid in S4. In particular, intuitionistic implication is understaood as strict material implication: γ(A → B) = □(γ(A) ⊃ γ(B)). Kamide and Wansing (2011) define a sequent calculus for connexive S4 based on MC. This system, CS4, is shown to be complete with respect to a relational possible worlds semantics. The proof uses a faithful embedding of CS4 into positive, negation-free S4. Moreover, it is shown that the cut-rule is an admissible rule in CS4 and that the constructive connexive logic C stand to CS4 as intuitionistic logic stands to S4. In the faithful embedding, the modal translation of negated implications is as expected: γ(~(A → B)) = □(γ(A) ⊃ γ(~B)). A similar translation is used in Odintsov and Wansing 2010 to embed C into a modal extension BS4 of Belnap and Dunn's four-valued logic.

In CS4 the modal operators □ and ◊ are syntactic duals of each other: the equivalence between □A and ~◊~A and between ◊A and ~□~A is provable. Kamide and Wansing (2011) also present a cut-free sequent calculus for a connexive constructive version CS4d– of S4 without syntactic duality between □ and ◊. The relational possible worlds semantics for CS4d– is not fully compositional, cf. Odintsov and Wansing 2004. CS4d– is faithfully embedabble into positive S4 and decidable. Moreover C is faithfully embeddable into CS4d–.

3. 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, 2004, Pizzi and Williamson 2005. 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 formulas and is closed under certain rules. 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, p. 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. The construction of Aristotelian squares of opposition and their combination to Aristotelian cubes in systems of consequential implication is considered in Pizzi 2008.

4. 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 or gimmick. 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 and the study of causal implications. A monograph developing a system of connexive logic in the context of solving a broad range of paradoxes is Angell 2002.

Bibliography

  • Almukdad A. and Nelson, D., 1984, “Constructible Falsity and Inexact Predicates”, Journal of Symbolic Logic, 49: 231–233.
  • Anderson, A.R. and N.D. Belnap, Jr., 1975, Entailment: The Logic of Relevance and Necessity, Volume I, Princeton: Princeton University Press.
  • Angell, R., 1962, “A Propositional Logic with Subjunctive Conditionals”, Journal of Symbolic Logic, 27: 327–343.
  • –––, 2002, A-Logic, Lanham: University Press of America.
  • Belnap, N.D., 1970, “Conditional Assertion and Restricted Quantification”, Noûs, 4: 1–13.
  • Bennett, J., 2003, A Philosophical Guide to Conditionals, Oxford: Clarendon Press.
  • Brady, R., 1989, “A Routley-Meyer Affixing Style Semantics for Logics Containing Aristotle's Thesis”, Studia Logica, 48: 235–241.
  • Cantwell, J., 2008, “The Logic of Conditional Negation”, Notre Dame Journal of Formal Logic, 49: 245–260.
  • Ferguson, T.M., 2012, “Ramsey's Footnote and Priest's Connexive Logics”, abstrcat, ASL Logic Symposium 2012, to appear in: Bulletin of Symbolic Logic.
  • –––, 2014, “Logics of Nonsense and Parry Systems”, Journal of Philosophical Logic, doi: 10.1007/s10992-014-9321-y, first published online: June 14, 2014.
  • Fine, K., 1986, “Analytic Implication”, Notre Dame Journal of Formal Logic, 27: 169–179.
  • Gibbard, A. 1981, “Two Recent Theories of Conditionals”, in: W.L. Harper, R. Stalnaker, and C.T. Pearce (eds.), Ifs, Dordrecht: Reidel.
  • Gurevich, Y., 1977, “Intuitionistic Logic with Strong Negation”, Studia Logica, 36: 49–59.
  • Johnson, F.A., 1976, “A Three-valued Interpretation for a Relevance Logic”, The Relevance Logic Newsletter, 1: 123–128. [Available online.]
  • Kamide, N. and Wansing, H., 2011, “Connexive Modal Logic Based on Positive S4”, in: J.-Y. Beziau and M. Conigli (eds.), Logic without Frontiers. Festschrift for Walter Alexandre Carnielli on the Occasion of His 60th Birthday, London: College Publications, 389–409.
  • –––, 2012, “ Proof theory of Nelson's Paraconsistent Logic: A Uniform Perspective”, Theoretical Computer Science 415: 1–38.
  • Kapsner, A., 2012, “Strong Connexivity”, Thought, 1: 141–145.
  • Kneale, W. and Kneale, M., 1962, The Development of Logic, London: Duckworth.
  • Lewis, D., 1973, Counterfactuals, Oxford: Basil Blackwell.
  • Lowe, E.J., 1995, “The Truth about Counterfactuals”, The Philosophical Quarterly, 45: 41–59.
  • MacColl, H., 1878, “The Calculus of Equivalent Statements (II)”, Proceedings of the London Mathematical Society 1877–78, 9: 177–186.
  • Martin, C.J., 2004, “Abelard on Logic”, in: J. Brower and K. Guilfoy (eds.), The Cambridge Companoin to Abelard, Cambridge: Cambridge University Press, 158–199.
  • McCall, S., 1966, “Connexive Implication”, Journal of Symbolic Logic, 31: 415–433.
  • –––, 1967, “Connexive Implication and the Syllogism”, Mind, 76: 346–356.
  • –––, 1975, “Connexive Implication”, § 29.8 in: A.R. Anderson and N.D. Belnap, Entailment. The Logic of Relevance and Necessity. Volume 1, Princeton: Princeton University Press, 434–446.
  • –––, 2012, “A History of Connexivity”, in D.M. Gabbay et al. (eds.), Handbook of the History of Logic. Volume 11. Logic: A History of its Central Concepts, Amsterdam: Elsevier, 415–449.
  • –––, 2014, “Connexive Gentzen”, Logic Journal of the IGPL, doi: 10.1093/jigpal/jzu019, first published online: July 4, 2014.
  • Meyer, R.K, 1977, “S5–The Poor Man's Connexive Implication”, The Relevance Logic Newsletter, 2: 117–123. [Available online.]
  • Mortensen, C., 1984, “Aristotle's Thesis in Consistent and Inconsistent Logics”, Studia Logica, 43: 107–116.
  • Nasti De Vincentis, M., 2006, “Conflict and Connectedness: Between Modern Logic and History of Ancient Logic”, in E. Ballo and M. Franchella (eds.), Logic and Philosophy in Italy, Monza: Polimetrica, 229–251.
  • Nelson, D., 1949, “Constructible Falsity”, Journal of Symbolic Logic, 14: 16–26.
  • Nelson, E.J., 1930, “Intensional Relations”, Mind, 39: 440–453.
  • Odintsov, S., 2008, Constructive Negations and Paraconsistency, Dordrecht: Springer-Verlag.
  • Odintsov S. and Wansing, H., 2004, “Constructive Predicate Logic and Constructive Modal Logic. Formal Duality versus Semantical Duality”, in V. Hendricks et al. (eds.), First-Order Logic Revisited, Berlin: Logos Verlag, 269–286.
  • –––, 2010, “Modal Logics with Belnapian Truth Values”, Journal of Applied Non-Classical Logics, 20: 279–301.
  • Parry, W.T., 1933, “Ein Axiomensystem für eine neue Art von Implikation (analytische Implikation)”, Ergebnisse eines mathematischen Kolloquiums, 4: 5–6.
  • Pizzi, C., 1977, “Boethius' Thesis and Conditional Logic”, Journal of Philosophical Logic, 6: 283–302.
  • –––, 1991, “Decision Procedures for Logics of Consequential Implication”, Notre Dame Journal of Formal Logic, 32: 618–636.
  • –––, 1993, “Consequential Implication: A Correction”, Notre Dame Journal of Formal Logic, 34: 621–624.
  • –––, 1996, “Weak vs. Strong Boethius' Thesis: A Problem in the Analysis of Consequential Implication”, in A. Ursini and P. Aglinanó (eds.), Logic and Algebra, New York: Marcel Dekker, 647–654.
  • –––, 2004, “Contenability and the Logic of Consequential Implication”, Logic Journal of the IGPL, 12: 561–579.
  • –––, 2008, “Aristotle's Cubes and Consequential Implication”, Logica Universalis, 2: 143–153.
  • Pizzi, C. and Williamson, T., 1997, “Strong Boethius' Thesis and Consequential Implication”, Journal of Philosophical Logic, 26: 569–588.
  • –––, 2005, “Conditional Excluded Middle in Systems of Consequential Implication”, Journal of Philosophical Logic, 34: 333–362.
  • Priest, G., 1999, “Negation as Cancellation and Connexive Logic”, Topoi, 18: 141–148.
  • Rahman, S. and Rückert, H., 2001, “Dialogical Connexive Logic”, Synthese, 127: 105–139.
  • Rahman, S. and Redmond, J., 2008, “Hugh MacColl and the Birth of Logical Pluralism”, in: D. Gabbay and J. Woods (eds.), Handbook of the History of Logic. Vol. 4: British Logic in the Nineteenth Century, Amsterdam: Elsevier, 533–604.
  • Ramsey, F.P., 1929, “General Propositions and Causality”, in F. Ramsey, Philosophical Papers, ed. H. A. Mellor, Cambridge: Cambridge University Press, 1990.
  • Routley, R., 1974, “Semantical Analyses of Propositional Systems of Fitch and Nelson”, Studia Logica, 33: 283–298.
  • –––, 1978, “Semantics for Connexive Logics. I”, Studia Logica 37: 393–412.
  • Routley, R., Meyer, R., Plumwood, V. and Brady, R., 1982, Relevant Logics and Their Rivals, Atascadero, CA: Ridgeview Publishing Company.
  • Routley, R. and Montgomery, H., 1968, “On Systems Containing Aristotle's Thesis”, Journal of Symbolic Logic, 33: 82–96.
  • Routley, R. and Routley V., 1985, “Negation and Contradiction”, Revista Columbiana de Mathemáticas, 19: 201–231.
  • Serenac, D. and Jennings, R.E., 2003, “The Preservation of Relevance”, Eidos, 17: 23–36.
  • Stalnaker, R. 1968, “A Theory of Conditionals”, in: N. Rescher (ed.), Studies in Logical Theory, American Philosophical Quarterly Monograph Series, 2, Oxford: Blackwell, 98–112.
  • Strawson, P., 1952, Introduction to Logical Theory, Oxford: Oxford University Press.
  • Thomason, R., 1969, “A Semantical Study of Constructive Falsity”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 15: 247–257.
  • Thompson, B., 1991, “Why is Conjunctive Simplification Invalid?”, Notre Dame Journal of Formal Logic, 32: 248–254.
  • Unterhuber, M., 2013, Possible Worlds Semantics for Indicative and Counterfactual Conditionals. A Formal Philosophical Inquiry into Chellas-Segerberg Semantics, Heusenstamm: Ontos Verlag.
  • Urchs, M., 1994, “On the Logic of Event-causation. Jaśkowski-style Systems of Causal Logic”, Studia Logica, 53: 551–578.
  • Wagner, G., 1991, Ex Contradictione Nihil Sequitur, in: Proceedings IJCAI 1991, , San Francisco: Morgan Kaufmann, 538–543.
  • Wansing, H., 2001, “Negation”, in L. Goble (ed.), The Blackwell Guide to Philosophical Logic, Cambridge, MA: Basil Blackwell Publishers, 415–436.
  • –––, 2005, “Connexive Modal Logic”, in R. Schmidt et al. (eds.), Advances in Modal Logic. Volume 5, London: King's College Publications, 367–383. [Available online.]
  • –––, 2007, “A Note on Negation in Categorial Grammar”, Logic Journal of the Interest Group in Pure and Applied Logics, 15: 271–286.
  • –––, 2008, “Constructive Negation, Implication, and Co-implication”, Journal of Applied Non-Classical Logics, 18: 341–364.
  • Wiredu, J.E., 1974, “A Remark on a Certain Consequence of Conexive Logic for Zermelo's Set Theory”, Studia Logica, 33: 127–130.
  • Woods, J., 1968, “ Two Objections to System CC1 of Connexive Implication”, Dialogue, 7: 473–475.

Other Internet Resources

[Please contact the author with other suggestions.]

Copyright © 2014 by
Heinrich Wansing <Heinrich.Wansing@rub.de>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.