Draft:Abelian logic

Abelian logic (also called the logic of Abelian ℓ-groups or Abelian Group Logic, abbreviated AGL) is a substructural, relevance logic whose algebraic semantics is given by lattice-ordered abelian groups (abelian ℓ-groups). Its specifically unusual among well-studied non-classical logics in being contra-classical: rather than being a sublogic of classical logic, it proves formulas that are not classical tautologies while failing to prove some formulas that are. It was discovered independently, and for different reasons, by Robert K. Meyer and John K. Slaney as a logic of relevance, and by Ettore Casari as a formal logic of comparison.

History of it

Meyer and Slaney presented the system at a 1979 meeting of the Australasian Association for Logic, although their results were not published until a decade later, as Abelian Logic in the anthology Paraconsistent Logic: Essays on the Inconsistent. same year, Ettore Casari independently published a description of the same logic, arrived on a different direction: he was formalizing comparative constructions in natural language (an example would be taller than or as heavy as), and called the resulting system comparative logic. Casari's original comparative logic is built on the slightly more general algebraic base of lattice-ordered pregroups which is restricted to genuine (abelian) groups it coincides with Meyer and Slaney's system. Meyer and Slaney returned to the system in a 2002 follow-up, "A, Still Adorable", proving (among other things) that Abelian logic is rejection-complete such that every formula is either a theorem or refutable in a Łukasiewicz-style sense. The logic has cases under an active research topic for example. recent work has produced new relational semantics for its negation, new proof theory, and a systematic algebraic study of its extensions.

Language and the axiomatization.

Abelian logic can be presented as an extension of BCI, the implicational fragment of linear logic. Where BCI has the axioms

${\text{B}}:\quad (A\to B)\to ((C\to A)\to (C\to B))$

${\text{C}}:\quad (A\to (B\to C))\to (B\to (A\to C))$

${\text{I}}:\quad A\to A$

and modus ponens as its rule, Abelian logic adds a schema which is the axiom of relativity:

${\text{A}}:\quad ((A\to B)\to B)\to A$

That generalizes double-negation elimination by letting any formula B stand in for falsity. Equivalently, Abelian logic is obtained from Anderson and Belnap's relevance logic R by adding a contraction schema $(A\to (A\to B))\to (A\to B)$ and generalizing R's negation axiom $((A\to \mathrm {f} )\to \mathrm {f} )\to A$ to the relativity schema above. Full Abelian logic extends this implication with conjunction, disjunction, and a truth constant $\mathrm {t}$. Dropping contraction (and, with it, weakening, $A\to (B\to A)$) is what keeps the logic relevant and stops it from collapsing into classical logic, even though the added relativity axiom is not itself a classical validity.

Notation.

Sources vary in how they render some of these ideas. Negation is most often written $\neg A$, defined as $A\to \mathrm {f}$ for a falsehood constant $\mathrm {f}$ (Meyer and Slaney's own truth and falsehood constants, $\mathrm {t}$ and $\mathrm {f}$, were stipulated to coincide). Other treatments — including Eric Schechter's textbook Classical and Nonclassical Logics, §26 — instead write negation with an overline, ${\overline {A}}$, and abbreviate any formula of the shape $A\to A$ or ${\overline {A\to A}}$ as $\bot$. Provability — "is a theorem of the logic" — is written with the turnstile, $\vdash A$, throughout the literature and below.

Semantics.

The Algebraic semantics

Abelian logic is sound and done with respect to the class of abelian ℓ-groups: structures

$\langle A,\,+,\,-,\,\vee ,\,\wedge ,\,0\rangle$

$\langle A,+,-,0\rangle$ is an abelian group and $\langle A,\vee ,\wedge \rangle$ is a lattice compatible with the group operation which also translations are order automorphisms, the Implication is interpreted as $A\to B:=-A+B$, the conjunction and disjunction as the lattice meet and join, and the designated referencing theorem-producing, the values of a model are the elements of its positive cone.

The real number comparative interpretation

The simplest and most-cited model is the additive group of the real numbers under their usual order, with the non-negative reals as designated values — this is Casari's comparative reading, on which a formula's "truth value" is a real number and truth amounts to being $\geq 0$. Meyer and Slaney showed that the model formats the logic of which a formula is a theorem of Abelian logic if and only if it is valid on the reals, so validity over the whole class of abelian ℓ-groups coincides with validity in this one comparative model.

A more of an understanding of one to make the claim off a reading like this to be natural, consider Schechter's illustration: writing M, T, C for the temperatures of milk, tea and coffee, the intuitively valid inference "if 'the coffee is hotter than the milk' is more true than 'the tea is hotter than the milk', then the coffee is hotter than the tea" formalizes as

$[(M\to T)\to (M\to C)]\to (T\to C)$,

unlike its classical, truth-table reading — is a theorem, since under the real-number semantics both sides reduce to the single value $C-T$.

The Meta theoretic features.

• we'll now establish the parts/features. Contra-classicality. More so, abelian logic proves the relativity axiom, which fails classically, while failing to prove classically valid principles such as weakening; it is therefore not a sublogic of classical logic, in either direction.
• Excluded middle and totality, it would hold. Even though an abelian ℓ-group need not be totally ordered, both $\vdash A\vee \neg A$ and $\vdash (A\to B)\vee (B\to A)$ are theorems. Algebraically this follows from a basic fact about lattice-ordered groups: the "absolute value" $A\vee (-A)$ of any element is always $\geq 0$, whether or not the group's order happens to be total.
• Negation-inconsistency, specifically isn't triviality/ in this case is not trivial under this instance. Because weakening itself fails, a model can satisfy both $A$ and $\neg A$ without every formula becoming provable; Abelian logic is accordingly classed as paraconsistent, and has been cited as an example of a genuinely dialetheic (non-trivially inconsistent) logic. This has turned into a debatable thing of whether $\neg$ deserves to be called "negation" at all, a question recent work has revisited using relational (Kripke-style) semantics.
• Relevance. As a descendant of BCI/R, Abelian logic retains the variable-sharing property characteristic of relevance logics: if $\vdash A\to B$ then A and B share a propositional variable.

The Proof theory.

Meyer and Slaney's original presentation was simply a Hilbert-style. Analytic proof systems that were later given by Metcalfe, Olivetti and Gabbay, who produced hypersequent calculi for Abelian logic — and, via a proof-theoretic embedding, for infinite-valued Łukasiewicz logic — together with terminating variants and labelled single-sequent calculi whose proof search runs in co-NP.

Relation to other logics.

• Łukasiewicz logic and MV-algebras. A categorical equivalence relates (pointed) abelian ℓ-groups to MV-algebras, the algebraic semantics of infinite-valued Łukasiewicz logic and more so. "pointed Abelian logic" has been used to axiomatize Łukasiewicz's unbounded logics relative to this base.
• Linear logic. Implication of Abelian logic properly extends BCI, the implicational fragmentation of linear logic.
• Modal extensions. Diaconescu, Metcalfe and Schnüriger built a real-valued modal logic on Abelian logic's group-and-lattice connectives combined with Kripke frames, giving a labelled tableau calculus and a coNEXPTIME upper bound for validity.
• Connexive logics. 2025 work combined Abelian logic with connexive logic, developing sequent-style proof theory for the resulting "Abelian connexive logics".
• Argumentation and equilibrium. Following Casari's original comparative motivation, the logic has also been re-derived as a logic of equilibrium for competing arguments.

See also.

• Relevance logic
• Linear logic
• Łukasiewicz logic
• Lattice-ordered group
• MV-algebra
• Substructural logic
• Paraconsistent logic
• Contra-classical logic

External links.

• Eric Schechter's page for Classical and Nonclassical Logics — includes a free excerpt (front matter) and errata for the textbook whose Chapter 26 covers Abelian logic. P 436-439.
• John Slaney's abstracts of the original Meyer–Slaney papers on Abelian logic, including "Abelian Logic (from A to Z)" and "A, Still Adorable".