Connexive Logic

Origin. Historical roots in Aristotle's and Boethius's theses. Modern revival by McCall (1960s), Wansing (1990s-present). Non-classical logic where negation and implication interact. ¬(A → ¬A) and (A → B) → ¬(A → ¬B) are valid. Counter to material implication paradoxes.

Models. Connection between antecedent and consequent. Material implication: A → B true when A false. Connexive: rejects this — implication requires connection. Aristotle's thesis: ¬(A → ¬A) (nothing implies its negation). Boethius's thesis: (A → B) → ¬(A → ¬B).

Formalism.

Aristotle's theses: AT: ¬(A → ¬A) — A doesn't imply not-A AT': ¬(¬A → A) — not-A doesn't imply A

Boethius's theses: BT: (A → B) → ¬(A → ¬B) — if A implies B, A doesn't imply not-B BT': (A → ¬B) → ¬(A → B) — if A implies not-B, A doesn't imply B

Failure in classical logic: Classically, (⊥ → ⊥) and (⊥ → ¬⊥) both true. So ¬((⊥ → ⊥) → ¬(⊥ → ¬⊥)) — BT fails.

Connexive semantics: Various approaches:

Worlds with "incompatibility" relation
Belief revision style
Nelson's logic extensions

Wansing's C: Combines features of Nelson's N4 (strong negation) with connexive theses. Four-valued approach.

Conditionals: Connexive logic often uses non-material conditional. A → B: A relevantly implies B.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Rightwards arrow	Connexive implication; non-symmetric
¬	U+00AC	Not sign	Negation, strong rather than material
∧	U+2227	Logical and	Conjunction
∨	U+2228	Logical or	Disjunction
⊥	U+22A5	Up tack	Falsum, used in the classical counterexample to BT
AT	—	Aristotle's thesis	¬(A → ¬A)
AT′	—	Aristotle's thesis, second form	¬(¬A → A)
BT	—	Boethius's thesis	(A → B) → ¬(A → ¬B)
BT′	—	Boethius's thesis, second form	(A → ¬B) → ¬(A → B)
C	—	Wansing's connexive logic	N4 with the altered falsity clause for →
N4	—	Nelson's paraconsistent logic	Constructive logic with strong negation
CC1	—	McCall's connexive system	Four-valued matrix logic (1966)

Metatheory. Connexivity is a constraint on validities rather than one system: a logic counts as connexive when it validates Aristotle's and Boethius's theses in both forms while its conditional stays non-symmetric. Both theses are classically invalid — take A false and A → ¬A is true, so ¬(A → ¬A) fails — which makes connexive logics contra-classical rather than weakenings of classical logic, so none can be obtained by deleting axioms. The structural cost is negation-inconsistency. Simplification gives both (A ∧ ¬A) → A and (A ∧ ¬A) → ¬A, and Boethius's thesis applied to the first yields ¬((A ∧ ¬A) → ¬A), so the system proves a formula and its negation; any connexive logic retaining simplification must therefore be paraconsistent if it is to stay non-trivial. Angell (1962) and McCall (1966) gave the first modern systems as finite matrices, hence decidable. Wansing (2005) obtained C from Nelson's N4 by a single change to the falsity clause — A → B is false at w iff at every w′ ≥ w where A is true, B is false, so ¬(A → B) is equivalent to A → ¬B — which delivers both theses at once, with a Kripke semantics and negation-inconsistency without triviality.

Applies to. Philosophy of logic. Conditional reasoning. Negation theories. Relevance and connection. Non-monotonic reasoning. Legal conditionals. Counterfactual reasoning.

Limitations. Because the theses are contra-classical, a connexive logic cannot be sound for classical semantics and cannot be recovered as a fragment of classical logic; combining it with classical reasoning is not a matter of restriction but of rejection. Negation-inconsistency is not incidental but forced by simplification, so consistency has to be given up and replaced by non-triviality, and the usual reductio and consistency arguments are unavailable. Connexivity does not yield relevance: C contains positive intuitionistic implication, so A → (B → B) is a theorem and the variable-sharing property fails, which is the very defect the theses were meant to address. And connexivity constrains only which formulas are valid, not what they mean — there is no characteristic algebra, no frame condition and no shared semantics for the family, so matrix, Kripke and cancellation-negation systems all qualify while agreeing on little else.