Abelian Logic

Origin. Robert K. Meyer and John K. Slaney, "Abelian Logic (from A to Z)" (in Graham Priest, Richard Routley, and Jean Norman, eds., Paraconsistent Logic: Essays on the Inconsistent, Philosophia Verlag, Munich 1989, 245–288), with a sequel, "A, Still Adorable" (in Carnielli, Coniglio, and D'Ottaviano, eds., Paraconsistency: The Logical Way to the Inconsistent, 2002). Ettore Casari arrived at the same logic independently, as a logic of comparison formalizing the majority, minority, and equality constructions of natural language, ideas he traced to Aristotle: "Comparative Logics and Abelian ℓ-groups" (in Ferro, Bonotto, Valentini, and Zanardo, eds., Logic Colloquium '88, North-Holland 1989, 161–190). George Metcalfe, Nicola Olivetti, and Dov Gabbay, "Sequent and Hypersequent Calculi for Abelian and Łukasiewicz Logics" (ACM Transactions on Computational Logic 6(3), 2005, 578–613), supplied the analytic proof theory.

Models. The logic of lattice-ordered abelian groups. Meyer and Slaney reached it from Anderson and Belnap's R by dropping contraction and liberalizing the double-negation axiom ((A → ⊥) → ⊥) → A to relativity, ((A → B) → B) → A; Casari reached it from comparatives; the two constructions determine the same variety, and ℤ generates that variety. In ℤ the implication measures a difference — v(A → B) = v(B) − v(A) — and a theorem is a formula whose value is non-negative under every assignment. A is contraclassical: relativity is classically refutable and weakening fails in A, so neither logic contains the other. Like RM3, A lies on the boundary between the relevant family and this division — it descends from R (see Relevance Logic) and sits here because a single totally ordered matrix characterizes it.

Formalism.

Language: →, +, ∧, ∨, t primitive. ¬A := A → t. A ↔ B := (A → B) ∧ (B → A).

Axioms (Meyer–Slaney): A1. ((A ∨ B) → C) ↔ ((A → C) ∧ (B → C)) A2. ((A + B) → C) ↔ (A → (B → C)) A3. (A → B) → ((B → C) → (A → C)) A4. ((A → B) ∧ (A → C)) → (A → (B ∧ C)) A5. (A ∧ (B ∨ C)) → ((A ∧ B) ∨ (A ∧ C)) A6. A ↔ (t → A) A7. (A ∧ B) → A A8. (A ∧ B) → B A9. A → ((A → B) → B) A10. ((A → B) → B) → A — the axiom of relativity Rules: modus ponens; adjunction.

Algebraic semantics: Abelian ℓ-groups ⟨G, +, ∨, ¬, t⟩: abelian group, lattice, + distributing over ∨. a ∧ b := ¬(¬a ∨ ¬b), a → b := ¬a + b. Validity: v(φ) ≥ t under every valuation. In A, a + b = ¬(¬a + ¬b) — intensional conjunction and intensional disjunction are the same connective — and t = ¬t.

Characteristic matrix: ℤ = ⟨ℤ, +, max, −, 0⟩, designated: the positive cone {a : a ≥ 0}. v(A → B) = v(B) − v(A); ¬ is minus; ∧ is min, ∨ is max, + is addition; t = 0. ℚ and ℝ serve equally (Characterisation Theorem below).

Checked in ℤ: Relativity: a − (b − (b − a)) = 0. Identically zero, not merely non-negative. Excluded middle A ∨ ¬A: max(a, −a) = |a| ≥ 0. Valid. Prelinearity (A → B) ∨ (B → A): |b − a| ≥ 0. Valid. Weakening A → (B → A): −b. Fails. Contraction (A → (A → B)) → (A → B): a. Fails. A → (B → B): −a. Fails — the relevant inheritance. Explosion (A ∧ ¬A) → B: b − min(a, −a); a = 0, b = −1 refutes. Paraconsistent. Variable sharing nonetheless fails: (p ∧ ¬p) → (q ∨ ¬q) evaluates to |a| + |b| ≥ 0, a theorem with no shared variable.

Substructural position: The negation-free fragment of FLe plus relativity (Jankovec and Poiger, "Pointed Modal Abelian Logic, Algebraically", EPTCS 447, 2026, 518–531); see Full Lambek Calculus. The intensional (group) fragment: sequent calculus by Paoli (Substructural Logics: A Primer, 2002); Shirahata's compact multiplicative linear logic CMLL is the same multiplicative logic.

Proof systems and complexity: Hypersequent calculus with cut elimination; terminating variants; co-NP labelled sequent calculi (Metcalfe–Olivetti–Gabbay 2005). Weispfenning (1986): the word problem for abelian ℓ-groups is co-NP-complete; hence the tautology problem for A is co-NP-complete.

Symbols.

Metatheory. The Characterisation Theorem: φ is a theorem of A iff φ is valid in all abelian ℓ-groups iff φ is valid in ℤ iff in ℚ iff in ℝ. The equivalence of theoremhood with validity in the variety is Meyer and Slaney's (1989), who also gave a direct proof that ℤ suffices; the equivalence among ℤ, ℚ, ℝ, and the variety is ℓ-group theory, since each of the three generates the variety of abelian ℓ-groups. A is decidable and its tautology problem co-NP-complete, by Weispfenning's co-NP-completeness of the word problem for abelian ℓ-groups (Theoretical Computer Science 48, 1986, 127–132) — the same complexity class as classical and Łukasiewicz validity, against the undecidability of R (Urquhart 1984, recorded in the Relevance Logic entry). Metcalfe, Olivetti, and Gabbay (2005) proved cut elimination for their hypersequent calculus and gave two embeddings of Łukasiewicz logic into A: Meyer and Slaney had shown the enthymematic fragment of A to be Ł⁺, the positive part of Łukasiewicz logic, and Metcalfe–Olivetti–Gabbay extended this to identify the material fragment of A with the whole of Ł. The kinship is the one the Łukasiewicz Logic entry records from the algebraic side — Mundici's Γ equivalence between MV-algebras and abelian ℓ-groups with strong unit — with [0, 1] standing to Ł as ℤ stands to A. Galli, Lewin, and Sagastume derived A as a logic of equilibrium for arguments, and Hirai (2013) proved his Amida calculus, intuitionistic linear logic plus the axiom (φ ⊸ ψ) ⊗ (ψ ⊸ φ), sound and complete for A.

Applies to. Comparative constructions in natural language — Casari's majority, minority, and equality. Proof theory for Łukasiewicz logic, through the embeddings of Ł into A. Paraconsistent reasoning with a detachable implication and a co-NP decision procedure. The study of contraclassical logics, where A is a well-known example. Session-typed concurrency, through Hirai's Amida calculus. The logic of equilibrium (Galli, Lewin, Sagastume).

Limitations. Variable sharing fails — (p ∧ ¬p) → (q ∨ ¬q) is a theorem — so A is not relevant in Anderson and Belnap's sense despite its parentage, the same verdict RM3 receives in this collection. There is no falsum and no verum: t = ¬t identifies the truth constant with its own negation, no formula implies every formula, and no formula is implied by every formula, since a nontrivial ℓ-group has neither greatest nor least element. Added to classical logic, relativity trivializes — instantiating B with any tautology turns ((A → B) → B) → A into A — so A-reasoning does not transfer to a classical context, and classical weakening and explosion do not transfer in. Nontrivial ℓ-groups are torsion-free and hence infinite, so A has no finite characteristic matrix and its decidability comes from Weispfenning's bound rather than from evaluation in a table. And theoremhood as guaranteed non-negative value means a formula and its negation are both theorems exactly when the value is identically zero — A → A and ¬(A → A) included — so the theorem set is negation-inconsistent while remaining nontrivial.

© 2026 Lingenic LLC