Correspondence of the Fragment F rules: LaTeX, Coq, Lean, Athena, Prolog

Three points fix what is, and what is not, being encoded.

1. There is only one “minimal logic”. The term denotes Johansson’s Minimalkalkül [1937] — intuitionistic logic without ex falso quodlibet — and nothing else. No rival system competes for the name.
2. \(\mathcal{F}_{\mathbf{M}}\) is a proper fragment of it, not the whole. The minimal reading uses four rules only — Ax, \(L\lnot\), \(R\to\), \(L\to\) — which is why every underivability established in \(\mathcal{F}_{\mathbf{M}}\) is a statement about that small fragment, not a borrowed theorem of full minimal logic. The Core reading \(\mathcal{F}_{\mathbb{C}}\) adds exactly one further rule, \(R\to_{\mathbb{C}}\), the sole Core-specific rule in the argument.
3. The four rules are Tennant’s own. They are transcribed in the sequent-calculus format Tennant himself adopts in Core Logic; the label \(R\to_{\mathbb{C}}\) is the only piece of notation that is mine. So the encodings below do not import a foreign presentation of minimal logic: they restate, in four proof languages, rules the Core logician already accepts.

Table 1 of the paper presents fragment F in the usual sequent-rule form. The three certifications encode the same derivability relation, up to three presentation differences, which are encoding conventions and not additional rules:

1. Contexts are sets (pools), treated extensionally. Ax is not encoded in the literal form A ⊢ A but in its membership form: A ∈ Γ ⟹ Γ ⊢ A. The form A ⊢ A of Table 1 is the instance Γ = {A}. Likewise L¬ locates ¬A in Γ by membership (rather than adjoining it notationally), and L→ shares a single context Γ instead of the junction ∆, Γ. This is the “contexts as available assumptions” convention of §2.1.
2. R→ is encoded “backwards”. Table 1 writes ∆ ⊢ B / ∆\{A} ⊢ A→B (A subtracted in the conclusion); the encoding adds A to the premiss context (A :: G) and leaves G in the conclusion. It is the same relation read the other way round — “putting A back into the context”, §2.3.
3. In Athena, derivations are reified. Where Coq and Lean define an inductive Prop with five constructors, Athena declares a datatype Deriv (the proof trees) plus a predicate well-formed defined by biconditionals, and sets derivable f G S ⟺ ∃ d . well-formed d f G S. Each “rule” is thus a clause of well-formed on a constructor of Deriv.

Reading: premisses ⟹ conclusion. Universal binders (forall f G A B / ∀ {f G A B}) are left implicit. In the Athena column, d : f G S abbreviates (well-formed d f G S); each row is the well-formed clause of the indicated constructor of Deriv.

The first four rules (Ax, L¬, R→, L→) are parametric in the fragment f: they hold identically under the minimal reading F_M and under the Core reading F_C. Only R→C is restricted to core_logic: it is the sole C-specific rule, and it is the one that breaks the symmetry between M and C on the fatal sequent.

The correspondence extends to core_logic_is_not_paraconsistent.pl. The five rules recur one by one (ax, lneg, rcond, lcond, rcond_core), up to notational conventions: ~A for ¬A, A=>B for A→B, Gamma:A for the sequent.

Since the recent cleanup, ax/1 has a single clause, the membership axiom shown above; it is therefore exactly Coq’s In A G -> derivable f G (Some A), Lean’s A ∈ G → … and Athena’s mem A G. (An earlier, unreachable second clause — which fired only on a context literally holding a sequent-term, something the calculus never builds — has been removed; every verdict is unchanged.)

• Does the correspondence also hold for the Prolog file? Yes, at the level of the five rules: ax, lneg, rcond, lcond, rcond_core correspond one to one to Ax, L¬, R→, L→, R→C, under the two caveats above (the bot constant; corroboration by bounded search).
• Does any of this require modifying the Coq file? No. This document only reads the existing sources; the three frozen certifications (.v, .lean, .ath) are unchanged and their SHA256 hashes remain identical.