Ackermann Logic

Origin. Wilhelm Ackermann, "Begründung einer strengen Implikation" (Journal of Symbolic Logic, 1956), introduced the connective ⥽ of rigorous implication — strenge Implikation — together with the axiomatic systems Π and Π′. The aim was an implication free of the paradoxes of material and strict implication, in which the antecedent must bear on the consequent. Anderson and Belnap took Π′ as their point of departure: their system E of entailment (Entailment, 1975) is Π′ with Ackermann's rule γ removed, and R was then obtained by adding permutation. Ackermann's paper is where the relevant tradition begins as a formal enterprise rather than a complaint.

Models. Implication as a genuine connection rather than a truth-function. The paradoxes Ackermann rejects are exactly those in which the antecedent plays no role: a false antecedent should not license an arbitrary consequent, and a true consequent should not be licensed by an arbitrary antecedent. Disjunctive syllogism is retained but only as a rule on theorems, never as a conditional, so the deductive strength of classical negation is available at the outer level and not inside the arrow.

Formalism.

Rigorous implication: A ⥽ B: A rigorously implies B. Rejects: ¬A ⥽ (A ⥽ B). Rejects: B ⥽ (A ⥽ B). No irrelevant implications.

Key rejections: Not: A ⥽ (B ⥽ A). Not: (A ∧ ¬A) ⥽ B. Not: A ⥽ (B ∨ ¬B). Paradoxes of material/strict implication rejected.

Positive part: Transitivity: (A ⥽ B) ⥽ ((B ⥽ C) ⥽ (A ⥽ C)). Modus ponens: A, A ⥽ B ⊢ B. Conjunction: A ⥽ B, A ⥽ C ⊢ A ⥽ (B ∧ C).

The rule γ: From ⊢ A and ⊢ ¬A ∨ B infer ⊢ B. Disjunctive syllogism as a rule on theorems, not as an axiom. ((A ∨ B) ∧ ¬A) ⥽ B is not a theorem: γ cannot be discharged into the arrow.

Necessity, defined not primitive: In E, □A := (A ⥽ A) ⥽ A. A is necessary when it is entailed by a logical truth. The modal fragment so defined is S4.

Propositional systems: Π and Π′: Ackermann's systems. E = Π′ minus γ (Anderson and Belnap). R = E plus permutation, (A ⥽ (B ⥽ C)) ⥽ (B ⥽ (A ⥽ C)). T ⊊ E ⊊ R.

Relation to R: R systematizes rigorous implication and adds permutation, which the entailment reading of ⥽ is taken to exclude. R has a clean algebraic semantics in De Morgan monoids; Π′ and E do not.

Symbols.

Metatheory. Anderson and Belnap obtained E by deleting Ackermann's rule γ from Π′, and Meyer and Dunn, "E, R, and γ" (Journal of Symbolic Logic, 1969), proved that γ is nevertheless admissible in E and in R: adding it yields no new theorems, so the deletion costs nothing at the level of theoremhood while removing disjunctive syllogism from the object language. Necessity is definable rather than primitive, □A := (A ⥽ A) ⥽ A, and the modal fragment of E so defined is S4, which is why E is read as a logic of entailment and R is not. The three systems are properly ordered, T ⊊ E ⊊ R, and permutation is what separates E from R. Urquhart, "The undecidability of entailment and relevant implication" (1984), proved all three undecidable by a reduction using von Neumann's coordinatization of modular lattices, and Urquhart (1993) showed that Craig interpolation fails for them as well. Variable sharing holds: if A ⥽ B is a theorem then A and B have a propositional variable in common.

Applies to. The origin of relevant entailment as a formal system. Comparison of E and R, where permutation is the dividing axiom. Paraconsistent reasoning, since explosion is not a theorem. The status of disjunctive syllogism, which γ isolates precisely. Modal readings of entailment via the defined necessity.

Limitations. γ is admissible but not derivable, so disjunctive syllogism cannot be discharged into the arrow: ((A ∨ B) ∧ ¬A) ⥽ B is not a theorem, and the inference is unavailable under hypotheses even though it preserves theoremhood. Without permutation, E's fusion is not commutative, and E and Π′ receive no algebraic characterization as economical as the De Morgan monoids that characterize R; the Routley–Meyer ternary semantics likewise fits R far better than it fits Π′ or E. All three systems are undecidable and none has Craig interpolation. Variable sharing is a necessary condition on theorems and not a sufficient one, so it does not characterize the logic. And Ackermann's original axiomatization was superseded: Π′ is studied through E rather than in its own right, and no independent completeness theorem for Π′ matches what R has.

© 2026 Lingenic LLC