Core Logic is not paraconsistent: one proof, six certifications

`DNS’ being an acronym for `Double Negation à la Slaney’ [3], I call `DNS.1’ and `DNS.2’ the rules listed in Table 2 below, together with their respective derivations in \(\mathcal{F}\), which prove that they are derivable in \(\mathbb{C}\). (By definition, a rule is derivable in a given system of rules if its conclusion is derivable from its premisses within the system [4, p. 47].)

A rule is invertible when, from the derivability of a sequent of the form of its conclusion, the derivability of all its premisses follows [5, p. 93]. By inspection of the derivation of DNS.1 in Table 2 above, it is provable in \(\mathcal{F}_{\mathbf{M}}\) that DNS.1 is invertible.

Indeed, from root to top, this derivation starts from an application of rule \(L\to\), whose right premiss is an axiom, so that invertibility on that side is trivial. On the left of this derivation, there is an application of rule \(R\to\). Consequently, DNS.1’s invertibility depends on \(R\to\)’s, which is itself provable. Note that in his discussion of the converse of the Deduction theorem, Tennant himself acknowledged the invertibility of \(R\to\) [2, p. 46] and, because the context of \(R\to\) is assumed as consistent, the application of Cut i.e.

is \(\mathbb{C}\)-admissible in this case [2, p. 154] and therefore impossible to deny. Note also that DNS.1, provably valid in M and containing no negation, cannot have its invertibility invalidated in \(\mathbb{C}\); but, for the most skeptical reader, an invertibility proof for DNS.1 is done by structural induction on derivation trees in \(\mathcal{F}_{\mathbf{M}}\), both in [6] and in mechanised proofs whose links are given at the end of this note. The \(\mathbb{C}\)-admissibility of Cut makes this proof of invertibility easy, by contrast with the structural induction, which is longer and harder but appeals to no Cut at all. Either way, DNS.1 is derivable in \(\mathbb{C}\), and its invertibility is a metatheorem of \(\mathcal{F}_{\mathbf{M}}\). That this invertibility also governs \(\mathbb{C}\)’s own rejection assertions is the one commitment that the final certified theorem displays as a named hypothesis (anti_DNS1_rule_for_ℂ; named conservativity_at_DNS1 in the Version 4 files) — precisely the overlap commitment of [2, p. 35].

The invertibility of DNS.1 means that whenever the conclusion is derivable, the premiss is derivable too. By contraposition, whenever the premiss is not derivable, the conclusion is not derivable either. This is precisely rule \(\overline{DNS.1}\):

In the terminology of refutation systems — the deductive systems for rejected statements initiated by Łukasiewicz [7] and developed for sequents by Tiomkin [8] and by Goranko [9]; for a survey, see [10] — \(\overline{DNS.1}\) is a refutation rule, and its licence is exactly Goranko’s correctness discipline for antisequent calculi: a refutation rule is correct when its converse is a correct rule, and the converse of \(\overline{DNS.1}\) is the invertibility of DNS.1, established above. \(\overline{DNS.1}\) is therefore not a meta-rule imported into the kernel from outside: it is a rule derivable from the kernel’s own invertibility, latent in the shadow of the system.

This point is the conclusion of the proof: as premiss of \(\overline{DNS.1}\), \eqref{claim1} entails an antisequent which is in contradiction with a consequence of DNS.2:

Therefore, \eqref{claim1} cannot be maintained in \(\mathbb{C}\) without contradiction: if Core logic is consistent, it cannot be paraconsistent. \(\blacksquare\)

Every step of the proof just read is machine-checked.

• Step 1: DNS.1 and DNS.2 are derivable — DNS.1 uniformly in the two readings of \(\mathcal{F}\), since its derivation uses only the four shared rules, and DNS.2 in \(\mathcal{F}_{\mathbb{C}}\) through \(R\to_{\mathbb{C}}\).
• Step 2: DNS.1 is invertible in \(\mathcal{F}_{\mathbf{M}}\), by one structural induction on derivations, without Cut.
• Step 3: \(\overline{DNS.1}\) is a metatheorem of \(\mathcal{F}_{\mathbf{M}}\), the contrapositive of that invertibility — Goranko’s converse-correctness licence [9], mechanised — and the refutation system whose only rejection axiom is \eqref{claim1} and whose only refutation rule is \(\overline{DNS.1}\) is Ł-correct for \(\mathcal{F}_{\mathbf{M}}\).
• Step 4: the contradiction, in two forms — the Ł-incorrectness of that same system for \(\mathcal{F}_{\mathbb{C}}\), which rejects a sequent that \(\mathcal{F}_{\mathbb{C}}\) derives, and the conditional theorem claim1_false, whose two hypotheses are displayed rather than hidden.

Nothing is postulated in support of the argument: in Coq, every Print Assumptions reports Closed under the global context, and in Lean 4 the proof depends on propext alone — an axiom of the ambient logic, not a premiss of the argument; the two principles granted to Tennant are antecedents of the final theorem. Whoever wishes to resist the conclusion must reject one of them — at the price, for the second, of giving up the refutation discipline of the very kernel that grounds the overlap of \(\mathbb{C}\) with \(\mathbf{M}\). These two horns are precisely the two points recalled in the introduction: the paraconsistency of \(\mathbb{C}\), and its overlap with \(\mathbf{M}\).

Table 1 fixes five rules, and a formal encoding must settle two things that their notation leaves open: whether an initial sequent may carry side formulæ, and whether \(L\to\) shares one context or splits it. The twelve statements are certified under both settlements, in three proof languages with distinct foundations — Coq and Lean 4 (dependent type theory), Athena (a denotational proof language over many-sorted first-order logic). Table 3 begins with the two clauses that differ and, beneath each, its three certifications. Each of the other three clauses, that is to say \(L\neg\), \(R\to\), \(R\to_{\mathbb{C}}\), is exactly the same on both sides.

The right-hand column is Table 1 read literally: reflexivity at the singleton, contexts split between the premisses, and no monotonicity lemma declared or used anywhere. This literalism comes at a price: with the axiom no longer diluted, \(R\to\) no longer involves an optional discharge but only a mandatory one, so that the following sequent, where \(A\) and \(B\) are distinct atoms, valid both in M and in \(\mathbb{C}\) [2, p. 35]:

is certified as being no longer derivable. One qualification is worth making here, since the cell above reads atomic: the encoded axiom quantifies over formulæ, not over atoms, and is therefore more generous than Table 1 on that point. The generosity runs in the safe direction. It can only enlarge the set of derivations, and the negative results — claim1_general, DNS1_inversion_lemma, atomic_relevance — are proved by induction over the enlarged system, hence hold a fortiori of the atomically restricted one. These files therefore certify a strict subsystem of \(\mathcal{F}_{\mathbb{C}}\), weakening-free by theorem rather than by inspection: atomic_relevance and no_dilution establish that no side formula can enter a context at all.

The left-hand column departs from Table 1 at those two clauses only, and the two are not independent. The diluted axiom is precisely what restores, in the textbook form of \(R\to\) (see syecond remark), the optional discharge that Table 1 writes \(\Delta \backslash \{A\}\): from \(B, A \vdash A\) by Ax., \eqref{eq:6} follows by \(R\to\). This is why Weakening on the left, though not a rule of \(\mathbb{C}\), must be admissible in it on consistent contexts. And context_monotonicity performs, as a lemma proved by structural induction, the merging of contexts that the multiplicative \(L\to\) effects notationally; it is certified inert and adds no theorem. The additive presentation is thus \(\mathbb{C}\)’s fragment \(\mathcal{F}\) as faithfully as additive-\(\mathbf{LJ}\) is \(\mathbf{LJ}\), with at most the latitude that \(\mathbb{C}\) itself admits. It is taken as the reference for the same reason that additive contraction-free calculi are standard throughout structural proof theory [11]: determinism in backward search, principal formulæ located by membership, no context split to guess.

The reader will see that, in the Comments section, an anonymous reader granted the theorem but doubted the system:

I’m extremely confident that you’ve proved the theorem in your challenge […] but I’m now quite certain that the system you’ve proven something about isn’t Core Logic.

The doubt bore on \(L\to\), read as a covert Weakening on the left. The two columns of Table 3 bracket the fragment, \[\text{multiplicative} \subsetneq \mathcal{F}_{\mathbb{C}} \subseteq \text{additive}\] and each half of the proof is certified at the bound where the inclusion carries it. The derivable half — absurdity_core, DNS1_in_ℱ, DNS2_instantiated, hence the sequent that collides — is certified at the lower bound: what a subsystem derives, \(\mathbb{C}\) derives a fortiori. The underivable half — claim1_holds_in_ℱ_ℂ, DNS1_conclusion_underivable_in_ℱ_M — is certified at the upper bound: what a system with more derivations still refuses to derive, \(\mathbb{C}\) refuses a fortiori. And claim1_false needs neither concession: it receives \eqref{claim1} from Tennant as a hypothesis and consumes only the derivable half, so it is certified at both bounds. The contradiction is therefore not an artefact of the structural settlement: it arises on every reading of \(\mathcal{F}\) that lies between the two bounds.

Two further silences are worth breaking, since faithfulness was the issue. In the derivations of Table 2 the multiplicative \(L\to\) is applied with its right context \(\Gamma\) empty — the right premiss being the axiom \(B \vdash B\) — so the split does no work there, and the additive version reaches the same conclusion by its single context_monotonicity step: two derivations of one sequent, not two logics. And Table 1 gives a left rule for negation and no right rule; the encoding transcribes this exactly, with L_neg and no R_neg. Negation enters the argument at exactly one point, through that one rule. In absurdity_core, the axiom \(A \vdash A\) becomes \(\lnot A, A \vdash\) by \(L\neg\), which introduces the negation on the left and empties the succedent — the sequent without which \(R\to_{\mathbb{C}}\) would have nothing to discharge. Everything after that is implicational: DNS2_instantiated reaches the decisive sequent by \(L\to\), \(R\to_{\mathbb{C}}\) and \(Ax.\). In both DNS steps \(\lnot A\) instantiates \(\Delta\), the context of the DNS rules — the “possible additional assumptions that are not active in a rule”, in Negri and von Plato’s terms [12, p. 15]. There the principal formula is \((A \to B) \to B\); \(\lnot A\) is neither principal nor active, and no rule for negation occurs anywhere in DNS.1, in DNS.2, or in their derivations in Table 2. So the chain turns on the implication rules, \(R\to_{\mathbb{C}}\) above all, and on the single left rule for negation that Table 1 supplies. There is no right rule for negation to tighten, to weaken, or to fault. The encoding of negation is examined on its own in the repository, which pins it between an upper and a lower bound in the same manner, and perturbs it with the very rules an objector would want.

Adequacy itself cannot be the object of a certification — de Bruijn’s criterion: the gap between an informal calculus and its formalisation is not closed by a machine, on pain of regress. But the burden it leaves is precise, because the fragment is small. Each of the five rules stands beside its encoding, clause by clause, in Coq, Lean 4, Athena and Prolog, in the rule-correspondence table; the companion note on the Prolog engine lets the reader generate derivations by the clauses themselves — a corroboration, since proof search exhibits witnesses whereas the six certifications above check proofs. To show the encoding inadequate it suffices to exhibit either a rule of \(\mathcal{F}\) that it fails to derive, or a rule of it not admissible in \(\mathbb{C}\). \(L\to\), the one rule named, is answered twice over in Table 3. A general doubt, unaccompanied by such an example, is not an objection that can be met, because it is not one that can be stated.

The six source files, the Comparator challenges, the config.json for the two-kernel procedure and the SHA256 of every frozen file are in the GitHub repository, whose README documents each check. Beyond the one-click links above, the additive Lean proof has been validated at the gold standard of the Lean reference manual: exported to a serialised proof term in a sandbox and replayed through two independently implemented kernels, Lean’s own and nanoda, written in Rust.

'claim1_false' depends on axioms: [propext]
Build completed successfully (3 jobs).
Running nanoda kernel on solution
Nanoda kernel accepts the solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!

Both kernels accept the proof term, whose only axiom is propext, and the statement they accept is, by construction, exactly that of the trusted challenge (SHA256: 6147a4234a2420a420d2c67eb145ace7b3d9ec14fc1e2dc368c35010e54804cc) — neither a weaker one nor a cleverly disguised one.

Coq and Lean 4 are two kernels of a single family: both implement a calculus of inductive constructions, so a proof that passes both has been checked twice against one foundation. A defect in that foundation — or in the way inductive definitions are elaborated within it — would be invisible to both. Athena is not of that family. It is a denotational proof language over polymorphic many-sorted first-order logic, with an assumption-base semantics in the LCF tradition [13]: there are no dependent types, no inductive definitions and no proof terms. A derivation is a datatype, its well-formedness a first-order predicate, and the twelve statements are re-proved from the free-generation axioms of that datatype alone. Athena can dispatch goals to automated provers; neither of these two files does. Every step is a kernel step — uspec, mp, directed chain rewriting — so verification succeeds or fails independently of any resource limit or prover heuristic.

This is precisely the value of Athena for the certification of this proof. The same twelve statements hold in two dependent type theories and in a framework that shares with them neither kernel, nor elaborator, nor notion of proof term — and, as Table 3 shows, under both structural readings of \(L\to\). Six certifications, three foundations, two presentations of the fragment: the contradiction owes nothing to the idiosyncrasies of a single system, nor to a single reading of the rules. It is the logical consequence of the small fragment \(\mathcal{F}\) of \(\mathbb{C}\) together with \eqref{claim1}. And the Corollary follows by the same reasoning, mutatis mutandis.