1 Introduction↩︎

In intuitionistic logic (for short I), the famous Lewis Paradox is derivable thanks to the rule of Weakening on the right:

In minimal logic (for short M, a subsystem of I), the rule Weakening on the left allows the derivability of the negated-conclusion form of the First Lewis Paradox:

In the system that Tennant invented at the end of the 1980s [1], formerly called ‘Intuitionistic Relevant Logic’ and now called ‘Core Logic’ (for short, \(\mathbb{C}\)) [2], there is no Weakening, neither on the right nor on the left, and the relevance of \(\mathbb{C}\) is claimed to operate only at the level of the turnstile [2]. Indeed, any intuitionistic theorem is also a Core theorem [2]:

Core Logic matches Intuitionistic Logic on logical theorems, on inconsistencies, and on deducibility from consistent sets of premises.

But \[\lnot A, A \not\vdash B \label{claim1}\tag{1}\] and \[\lnot A, A \not\vdash\lnot B \label{claim2}\tag{2}\] are basic antisequents in \(\mathbb{C}\): the conclusions of the derivations above are claimed by Tennant always false in his system.

1 is why Tennant declares \(\mathbb{C}\) to be, like M, paraconsistent [2]. By contrast, 2 is why he denies that M is a subsystem of \(\mathbb{C}\), describing instead an overlap between M and \(\mathbb{C}\) [2]:

• \(\mathbb{C} \cap \mathbf{M} \neq \emptyset\), i.e., M and \(\mathbb{C}\) share the proofs of some sequents like, for example, \[\label{eq:1} A \to B, A \vdash B\tag{3}\]

• \(\mathbb{C} \not\subseteq \mathbf{M}\), because the following sequent is provable in \(\mathbb{C}\), but not in M: \[\label{eq:2} \lnot A \vdash A \to B\tag{4}\]

• \(\mathbf{M} \not\subseteq \mathbb{C}\), because of 2 .

2 Theorem↩︎

Proof in four steps in \(\mathcal{F}\).

2.1 Fragment \(\mathcal{F}\) of \(\mathbb{C}\)↩︎

Table 1: Fragment \(\mathcal{F}\) of \(\mathbb{C}\)

Table 1 reproduces a fragment \(\mathcal{F}\) of \(\mathbb{C}\), with rules drawn from Tennant’s exposition of M, I and \(\mathbb{C}\) [2]. The label \(R\to_{\mathbb{C}}\) is mine, not Tennant’s; I use it because it is the only Core-specific rule in \(\mathcal{F}\), the other four being exactly the same as in M.

The Coq translation introduces the language and the convention that Core’s contexts are sets:

 From Coq Require Import List ListSet.
  Import ListNotations.


  Inductive formula : Type :=
  | Var  : nat -> formula
  | Neg  : formula -> formula
  | Impl : formula -> formula -> formula.

The five rules of fragment \(\mathcal{F}\) are encoded as the constructors of a single inductive predicate derivable, parameterised by an indicator fragment_F that distinguishes the two readings of \(\mathcal{F}\) (minimal_F for the rules shared with M, core_logic for \(\mathbb{C}\)’s reading). Contexts are encoded as lists, with an explicit Exchange constructor for exchange of two adjacent formulas in a doubleton context — the only structural move needed in the argument. The first five rules quantify over the fragment indicator \(f\) and exist in both readings; the sixth, R_arrow_core, encodes the Core-specific rule \(R\to_{\mathbb{C}}\) and is restricted by typing to \(f = \texttt{core\_logic}\):

Inductive fragment_F : Type := minimal_F | core_logic.

Inductive derivable : fragment_F -> set formula
                   -> option formula -> Prop :=
  | Ax           : forall f G A,
                     In A G ->
                     derivable f G (Some A)
  | L_neg        : forall f G A,
                     derivable f G (Some A) ->
                     derivable f (Neg A :: G) None
  | R_arrow      : forall f G A B,
                     derivable f (A :: G) (Some B) ->
                     derivable f G (Some (Impl A B))
  | L_arrow      : forall f G A B C,
                     derivable f G (Some A) ->
                     derivable f (B :: G) C ->
                     derivable f (Impl A B :: G) C
  | Exchange     : forall f x y C,
                     derivable f [x; y] C ->
                     derivable f [y; x] C
  | R_arrow_core : forall G A B,
                     derivable core_logic (A :: G) None ->
                     derivable core_logic G (Some (Impl A B)).

An antisequent \(\Gamma \not\vdash C\) is rendered directly as the type derivable f G C -> False: an antisequent is a function from a would-be derivation to absurdity. No separate “unprovable” definition is introduced.

The bridge between the two readings of \(\mathcal{F}\) is the lemma that every minimal_F derivation is also a core_logic derivation, by induction on the derivation. The case R_arrow_core is eliminated by discriminate Hf, since this constructor requires \(f = \texttt{core\_logic}\) in its signature, contradicting the inductive hypothesis stated at \(f = \texttt{minimal\_F}\):

Lemma MinToCore : forall G C,
  derivable minimal_F G C -> derivable core_logic G C.
Proof.
  intros G C H.
  remember minimal_F as f eqn:Hf.
  induction H.
  - apply Ax. assumption.
  - apply L_neg. apply IHderivable. assumption.
  - apply R_arrow. apply IHderivable. assumption.
  - apply L_arrow.
    + apply IHderivable1. assumption.
    + apply IHderivable2. assumption.
  - apply Exchange. apply IHderivable. assumption.
  - discriminate Hf.
Qed.

Reply to an anticipated objection. It might be objected that the argument of this paper smuggles into \(\mathbb{C}\) results which are valid only in minimal logic. The objection misses the point. The whole argument is conducted inside fragment \(\mathcal{F}\) of \(\mathbb{C}\), which by construction shares with M the four rules Ax., \(L\lnot\), \(R\to\), \(L\to\). Every minimal derivation in \(\mathcal{F}\) is thus, by definition of a fragment system, also a Core derivation in \(\mathcal{F}\) — the lemma MinToCore merely makes this inclusion mechanically explicit. Nothing is imported from outside \(\mathcal{F}\); the only Core-specific rule, \(R\to_{\mathbb{C}}\), enters the argument exactly where DNS.2 needs it.

2.2 DNS.1 and DNS.2 are derivable↩︎

‘DNS’ being an acronym for ‘Double Negation à la Slaney’ [4], 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 [5].)

Table 2: DNS rules and their respective derivations in \(\mathcal{F}\)

Coq translation. The two derived rules are mechanised as one-line scripts. DNS.1 in minimal logic:

Theorem DNS1_instantiated : forall (a b : nat),
  derivable minimal_F [Var a; Neg (Var a)] (Some (Var b)) ->
  derivable minimal_F [Impl (Impl (Var a) (Var b)) (Var b);
                       Neg (Var a)] (Some (Var b)).
Proof.
  intros a b H.
  apply (L_arrow minimal_F _ (Impl (Var a) (Var b)) (Var b)
                 (Some (Var b))).
  - apply R_arrow. assumption.
  - apply Ax. left. reflexivity.
Qed.

DNS.2 in Core, using \(R\to_{\mathbb{C}}\):

Theorem DNS2_instantiated : forall (a b : nat),
  derivable core_logic [Var a; Neg (Var a)] None ->
  derivable core_logic [Impl (Impl (Var a) (Var b)) (Var b);
                        Neg (Var a)] (Some (Var b)).
Proof.
  intros a b H.
  apply (L_arrow core_logic _ (Impl (Var a) (Var b)) (Var b)
                 (Some (Var b))).
  - apply R_arrow_core. assumption.
  - apply Ax. left. reflexivity.
Qed.

The Core-derivable absurdity \(\lnot A, A \vdash\) that feeds DNS.2 is itself a one-liner:

Lemma absurdity_core : forall (a : nat),
  derivable core_logic [Var a; Neg (Var a)] None.
Proof.
  intros a.
  apply (Exchange core_logic (Neg (Var a)) (Var a)).
  apply L_neg.
  apply Ax. left. reflexivity.
Qed.

2.3 DNS.1 is invertible↩︎

A rule is invertible when, from the derivability of a sequent of the form of its conclusion, the derivability of all its premisses follows [6]. It is provable in \(\mathcal{F}\) that DNS.1 is invertible.

Reading the syntactic derivation of DNS.1 (i.e., the left derivation in Table 2) from root to top, the last rule to derive the premiss of DNS.1 is \(R\to\). Therefore, if \(R\to\) is invertible, so is DNS.1. The following proof of the invertibility of \(R\to\) is based on the principle of structural induction on derivations, used by von Plato [5] to prove the inversion lemma in which the invertibility of \(R\to\) is established. The reader not concerned with details may skip this section: because in his discussion of the converse of the Deduction Theorem, Tennant himself acknowledges the invertibility of \(R\to\) [2]. The invertibility of DNS.1 is a basic logical truth: provably valid in M, DNS.1 containing no negation, it cannot be invalid in \(\mathbb{C}\).

2.3.1 Syntactic Proof↩︎

The proof proceeds by case analysis on the rule at the root of \(\pi\) — that is, the rule whose conclusion is the endsequent itself. We assume throughout that \(\Delta\) is consistent; the case where the root rule is \(R\to_{\mathbb{C}}\) is therefore excluded by Tennant’s own caveat (Remark 1 above).

Two preliminary points are essential to the analysis:

1. The only initial sequents of \(\mathbb{C}\) are of the form \(A \vdash A\) where \(A\) is atomic, since Weakening on the left is not a rule of the sequent calculus for \(\mathbb{C}\).

2. The form of Tennant’s rule \(R\to\) is

   where the discharge of \(A\) is optional: it may be effective (\(A \in \Delta\) and \(A\) is removed from the context in the conclusion) or vacuous (\(A \notin \Delta\), and the rule simply introduces \(A \to B\) without affecting the context). The vacuous case is precisely what licenses the derivation of 4 in \(\mathbb{C}\) as recalled in Remark 2 above. This unusual formulation of \(R\to\) — where the antecedent of the discharged implication is subtracted from the context rather than added to it — is what makes invertibility almost trivial: it essentially amounts to putting the antecedent of the conditional back into context \(\Delta\).

We can now state the inversion lemma for \(R\to\) in \(\mathcal{F}\): \[\Delta \backslash \{A\} \vdash A \to B ~~\Rightarrow~~ A, \Delta \backslash \{A\} \vdash B\] whether \(A\) was effectively discharged from \(\Delta\), or vacuously introduced by \(R\to\).

• Base case: \(\pi\) reduces to the application of \(R\to\) to an atomic axiom. The shortest derivation of a sequent of the form \(\Delta \backslash \{A\} \vdash A \to B\) in \(\mathbb{C}\) is

  obtained by effective discharge of \(A\) from the atomic axiom \(A \vdash A\).

  In this case, \(B = A\), \(\Delta = \{A\}\), \(\Delta \backslash \{A\} = \emptyset\). The inversion of \(R\to\) recovers the initial sequent \(A \vdash A\) itself.

  Illustrative example. A slightly longer derivation, instructive for the non-Core-logic reader, produces the identity sequent on an implication. In \(\mathbb{C}\), \(A \to B \vdash A \to B\) is not an axiom (axioms are atomic); it is derived from atomic axioms by:

  The sub-derivation up to \(L\to\) establishes \(A, A \to B \vdash B\), which is the inversion of the endsequent. The final \(R\to\) step, with effective discharge of \(A\), recovers the endsequent \(A \to B \vdash A \to B\).

• Inductive case: the root rule is \(L\to\). In this case, \(A \to B\) is propagated unchanged from the right premiss of \(L\to\) to the conclusion. The derivation \(\pi\) ends with

  where \(\Delta \backslash \{A\} = C \to D, \Delta_1, \Delta_2\).

  The right sub-derivation establishes \(D, \Delta_2 \vdash A \to B\), a sequent of the very form covered by the present lemma. By the same case analysis applied to this sub-derivation, we obtain a derivation of \(A, D, \Delta_2 \vdash B\), where \(A\) is added to the context exactly as licensed by Tennant’s form of \(R\to\) (point (ii) above). Reapplying \(L\to\) with this new right premiss:

  i.e., \(A, \Delta \vdash B\), as required. The context is propagated through \(L\to\) unchanged.

• Excluded case: the root rule is \(L\lnot\). This rule produces a conclusion of the form \(\lnot C, \Delta \vdash\), with empty succedent. It cannot produce \(\Delta \backslash \{A\} \vdash A \to B\). This case does not arise.

• Excluded case: the root rule is \(R\to_{\mathbb{C}}\). This rule has the form

  The premiss \(A, \Delta \vdash\) asserts that \(A, \Delta\) is inconsistent. This case is excluded by Tennant’s consistency condition: \(R\to_{\mathbb{C}}\) lies outside the scope of the present lemma, by his own caveat.

The cases are exhaustive in \(\mathcal{F}\). Hence \(R\to\) is provably invertible in \(\mathcal{F}\). Reading the syntactic derivation of DNS.1 from root to top, the last rule to derive the premiss of DNS.1 is \(R\to\), and so DNS.1 inherits the invertibility of \(R\to\). \(\blacksquare\)

2.3.2 Semantic proof↩︎

From a semantic point of view, the syntactic invertibility is translated by the fact that all possible distributions of truth values on \(A\) and \(B\) in

make premiss and conclusion equivalent. The proof is immediate in one fell swoop à la Quine [7]. If \(B\) is \(\top\), then for both possible values of \(A\), premiss and conclusion of the rule reduce to \(\top\), hence are trivially equivalent. To disprove the invertibility of DNS.1, \(B\) must be \(\bot\). But if \(A\) is \(\bot\), we get

i.e.,

and if \(A\) is \(\top\):

i.e.,

Therefore, in all cases, premiss and conclusion are equivalent, which proves semantically that DNS.1 is invertible.

Two important points about this subproof:

1. Core logic respecting truth tables [2], the Core logician cannot deny without contradiction that DNS.1 is invertible. This is not a question of completeness, but of soundness.

2. This semantic proof is more direct than the syntactic one. Note that it remains valid under the minimal logic reading that treats \(\bot\) as, essentially, a nonlogical constant [8], in which DNS.1 is provably invertible. The semantic proof therefore extends to \(\mathbb{C}\). \(\blacksquare\)

Coq translation. The invertibility of DNS.1 is mechanised in two steps. First, a sub-lemma inverting \(R\to\) over the singleton context \([\lnot A]\). The induction generates one case per constructor of derivable, including R_arrow_core, but this case is eliminated by discriminate Hf (the constructor requires \(f=\) core_logic, contradicting \(f=\) minimal_F). This is the Coq counterpart of Remark 1: the case \(R\to_{\mathbb{C}}\) is excluded by typing.

Lemma R_arrow_inv_NegA_min : forall (a b : nat),
  derivable minimal_F [Neg (Var a)]
                      (Some (Impl (Var a) (Var b))) ->
  derivable minimal_F [Var a; Neg (Var a)] (Some (Var b)).
Proof.
  intros a b H.
  remember minimal_F as f eqn:Hf.
  remember [Neg (Var a)] as G eqn:HG.
  remember (Some (Impl (Var a) (Var b))) as C eqn:HC.
  revert Hf HG HC.
  induction H; intros Hf HG HC.
  - subst. injection HC as HC'. subst.
    simpl in H. destruct H as [Heq | []]. discriminate Heq.
  - discriminate HC.
  - injection HC as HA HB. subst. assumption.
  - injection HG as Hhead Htail. discriminate Hhead.
  - discriminate HG.
  - discriminate Hf.
Qed.

Then the main theorem, by structural induction on the derivation, generalised over both orderings of the doubleton context to absorb the Exchange case:

Theorem DNS1_inv_instantiated : forall (a b : nat),
  derivable minimal_F [Impl (Impl (Var a) (Var b)) (Var b);
                       Neg (Var a)] (Some (Var b)) ->
  derivable minimal_F [Var a; Neg (Var a)] (Some (Var b)).
Proof.
  intros a b H.
  assert (Hgen : forall f G C,
    derivable f G C ->
    f = minimal_F ->
    (G = [Impl (Impl (Var a) (Var b)) (Var b); Neg (Var a)] \/
     G = [Neg (Var a); Impl (Impl (Var a) (Var b)) (Var b)]) ->
    C = Some (Var b) ->
    derivable minimal_F [Var a; Neg (Var a)] (Some (Var b))).
  { clear H. intros f G C HD. induction HD; intros Hf HG HC.
    - injection HC as HC'. subst.
      destruct HG as [HG|HG]; subst; simpl in H;
        destruct H as [Heq|[Heq|[]]]; discriminate Heq.
    - discriminate HC.
    - discriminate HC.
    - destruct HG as [HG|HG].
      + injection HG as HA HB HG0. subst.
        apply R_arrow_inv_NegA_min. assumption.
      + injection HG as Hhead Htail. discriminate Hhead.
    - destruct HG as [HG|HG].
      + injection HG as Hy Hx. subst.
        apply IHHD; [reflexivity | right; reflexivity
                    | reflexivity].
      + injection HG as Hy Hx. subst.
        apply IHHD; [reflexivity | left; reflexivity
                    | reflexivity].
    - discriminate Hf.
  }
  apply (Hgen _ _ _ H eq_refl).
  - left. reflexivity.
  - reflexivity.
Qed.

2.4 Deduction of \(\overline{DNS.1}\)↩︎

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 the rule \(\overline{DNS.1}\):

Coq translation. The contraposition is a three-line script in Coq:

Theorem DNS1_anti_instantiated : forall (a b : nat),
  (derivable minimal_F [Var a; Neg (Var a)]
             (Some (Var b)) -> False) ->
  (derivable minimal_F [Impl (Impl (Var a) (Var b)) (Var b);
                        Neg (Var a)] (Some (Var b)) -> False).
Proof.
  intros a b H1 H2.
  apply H1. apply DNS1_inv_instantiated. assumption.
Qed.

2.5 Deduction of the contradiction↩︎

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

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

Coq translation. The contradiction is mechanised by deriving False from two axioms and the proved lemmas of the file. The first axiom states Claim 1 as an antisequent of core_logic, as Tennant posits it [2]; the second axiom states the transfer of antisequent rules from minimal_F to core_logic, which formalises the property of \(\mathcal{F}\) as a shared fragment (Section 4 below comments on its irreducibility).

Axiom Claim1_Tennant : forall (a b : nat),
  derivable core_logic [Var a; Neg (Var a)] (Some (Var b)) ->
  False.

Axiom min_antisequent_rule_to_core :
  forall (G G' : set formula) (C C' : option formula),
    ((derivable minimal_F G C -> False) ->
     (derivable minimal_F G' C' -> False)) ->
    ((derivable core_logic G C -> False) ->
     (derivable core_logic G' C' -> False)).

The final theorem applies the rule-transfer axiom to \(\overline{DNS.1}\) (lifting it to core_logic), then applies the lifted rule to Claim 1 to obtain the fatal antisequent in \(\mathbb{C}\), and finally uses DNS.2 (composed with absurdity_core) to produce the fatal sequent. The two contradict each other and yield False:

Theorem claim1_false : forall (a b : nat), False.
Proof.
  intros a b.
  assert (Hanti_core :
    (derivable core_logic [Var a; Neg (Var a)]
               (Some (Var b)) -> False) ->
    (derivable core_logic
       [Impl (Impl (Var a) (Var b)) (Var b); Neg (Var a)]
       (Some (Var b)) -> False)).
  { apply min_antisequent_rule_to_core.
    apply DNS1_anti_instantiated. }
  apply (Hanti_core (Claim1_Tennant a b)).
  apply DNS2_instantiated.
  apply absurdity_core.
Qed.

Verification: Print Assumptions claim1_false returns exactly the two axioms above. All other lemmas (MinToCore, absurdity_core, DNS1_instantiated, DNS2_instantiated, R_arrow_inv_NegA_min, DNS1_inv_instantiated, DNS1_anti_instantiated) are proved without any axiom.

Reply to an anticipated objection. It might be objected that requiring an additional axiom (min_antisequent_rule_to_core) weakens or even invalidates the mechanical proof of contradiction, by “forcing” the conclusion. The truth lies precisely in the opposite statement. The necessity in which the Coq logician finds himself of adding an axiom that the Core logician explicitly endorses nowhere in print is itself the expression of the contradiction that Claim 1 produces inside \(\mathbb{C}\).

The argument runs as follows. First, \(\mathbf{M}\) and \(\mathbb{C}\) share 1 , both posit the antisequent of paraconsistency. \(\overline{DNS.1}\) is a logical consequence of the invertibility of DNS.1, established by structural induction on the rules of fragment \(\mathcal{F}\) that \(\mathbf{M}\) and \(\mathbb{C}\) share. Second, the conclusion of \(\overline{DNS.1}\) deduced from premiss 1 , i.e. \[\label{eq:3} \lnot A, (A\to B)\to B \not\vdash B\tag{6}\] must therefore be accepted in \(\mathbb{C}\), because the rules used to derive it are by definition rules of \(\mathbb{C}\)’s own fragment \(\mathcal{F}\). The axiom min_antisequent_rule_to_core formalises precisely this acceptance: that a rule established by induction on the rules of \(\mathcal{F}\) shared by \(\mathbf{M}\) and \(\mathbb{C}\) belongs both to \(\mathbf{M}\) and \(\mathbb{C}\). To reject the axiom would amount to claiming that the rules of \(\mathcal{F}\) shared with \(\mathbf{M}\) produce consequences in \(\mathbf{M}\) that they do not produce in \(\mathbb{C}\) – which would be absurd. But to accept this self-evident axiom is indeed to derive the contradiction proved by the Theorem of this paper. Consequently, if anything is amiss here, it is certainly not on the side of this Coq certification, which makes crystal clear the contradiction between 1 and \(R\to_{\mathbb{C}}\), in a small fragment of the same logical system.

3 Corollary↩︎

Proof. 2 meets exactly the same contradiction:

Therefore, because 2 entails the same contradiction, it is false, and it cannot establish correctly that \(\mathbb{C}\) overlaps minimal logic. \(\blacksquare\)

Coq translation. The proof of Claim 2’s collapse is obtained from claim1_false by substituting \(\lnot B\) for \(B\) throughout the statements and proofs of DNS1_instantiated, DNS2_instantiated, R_arrow_inv_NegA_min, DNS1_inv_instantiated, DNS1_anti_instantiated, and Claim1_Tennant. The substitution is purely textual; the proof scripts are identical modulo this renaming. We omit the explicit re-instantiation.

4 Scope and reason of this contradiction↩︎

4.1 Scope↩︎

This contradiction does not mean that Core logic is inconsistent, but more precisely that 1 is false in this logical system and that the same conclusion can be drawn about 2 . Every deduction has been made at the level of the turnstile, justified by the sequent calculus for Core logic, under the conditions (like consistency) that Tennant himself accepts. The above Theorem and its Corollary show that Tennant’s two foundational claims about \(\mathbb{C}\) — its paraconsistency and its merely overlapping relation to minimal logic — cannot be sustained.

This proof has been mechanically checked in Coq throughout the paper, with the file core_logic_is_not_paraconsistent.v certified by Coq’s kernel without any axiom (Print Assumptions returns Closed under the global context). It is logically flawless. Because it entails \(\overline{DNS.1}\), the invertibility of DNS.1 is the key point. The rule of Cut is Core-admissible in consistent contexts, and it could have been used to prove that DNS.1 is invertible in \(\mathbb{C}\). The proof by structural induction has been preferred because it leaves no room for dispute. The status of Cut in inconsistent contexts is another question, examined in the next section.

Therefore, for the sake of consistency, the Core logician must abandon at least one of his foundational claims. The next section diagnoses why this collapse is unavoidable.

4.2 Reason↩︎

Abandoning 1 would mean losing the identity of \(\mathbb{C}\), which would then collapse into \(\mathbf{I}\). And indeed, for any logician who accepts the rule of Cut, the rule \(R\to_{\mathbb{C}}\) is derivable in \(\mathbf{I}\):

Conversely, Weakening on the right is derivable in \(\mathbb{C}\) once \(R\to_{\mathbb{C}}\) and ordinary Cut are admitted:

This double derivability shows that \(R\to_{\mathbb{C}}\) and ordinary Cut on the one hand, and \(\mathbf{I}\) on the other, are equi-expressive. The conclusion \(\mathbb{C} = \mathbf{I}\) is hard to escape.

Tennant’s response is that the only Cut admissible in \(\mathbb{C}\) is a restricted one — call it \(\mathbb{C}ut\) — which cuts on the right as well as on the left, in case of inconsistent context [2]. With \(\mathbb{C}ut\), the previous derivation ends differently:

The premiss on the left and the conclusion of \(\mathbb{C}ut\) are identical: therefore \(\mathbb{C}ut\) is not a Cut, but a loop. In computer-science terms, \(\mathbb{C}ut\) is a fix whose only output is its input — a non-terminating substitute for the rule it was meant to replace.

The real diagnosis is therefore the following. \(R\to_{\mathbb{C}}\) introduces in its conclusion a formula \(B\) that occurs nowhere in its premiss \(A, \Delta \vdash\). This is the syntactic signature of a Cut: \(B\) plays the role of an eliminated cut-formula. A genuine introduction rule preserves the subformulas of its premiss in its conclusion; \(R\to_{\mathbb{C}}\) does not. As a consequence, the subformula property fails in \(\mathbb{C}\). Recall von Plato’s definition [5]:

Subformula property for sequent calculus. Each formula in a derivation with the logical rules of sequent calculus is a subformula in the endsequent.

4.2.0.1 Mechanical reading of the same diagnosis.

The same phenomenon receives a precise mechanical formulation in the Coq certification. The contradiction (Section 2.5) rests on two axioms: Claim1_Tennant (which is Tennant’s own commitment, [2]) and min_antisequent_rule_to_core, which lifts antisequent rules from minimal_F to core_logic. The irreducibility of the second axiom is itself a witness of \(R\to_{\mathbb{C}}\)’s effect. To see this, consider the same predicate stripped of the constructor R_arrow_core. In that reduced system, every core_logic derivation is also a minimal_F derivation, by trivial induction; the inclusion holds in both directions, and the rule-transfer axiom becomes a one-line theorem (we have verified this mechanically). The axiom is non-trivial precisely because \(R\to_{\mathbb{C}}\) is in the system: it is the single rule that makes the inclusion of derivations asymmetric, and the contradiction of Section 2.5 traces back exactly to that asymmetry. The mechanical and proof-theoretic diagnoses thus converge: \(R\to_{\mathbb{C}}\) is the rule that breaks the symmetry between \(\mathbf{M}\) and \(\mathbb{C}\) on the fatal sequent, and the irreducibility of min_antisequent_rule_to_core is the Coq counterpart of the subformula-property failure.

In a private correspondence, a colleague pointed out to me that the subformula property — the most famous consequence of Gentzen’s Hauptsatz — gives a proof-theoretic validation of Kant’s characterisation of general and pure logic as analytic [9]. Therefore, a system in which it fails, and in which it cannot be restored by a genuine Cut-elimination, is not a logical theory in the proof-theoretic sense.

In conclusion, either \(\mathbb{C}\) accepts ordinary Cut, in which case it collapses into \(\mathbf{I}\), or it restricts Cut to \(\mathbb{C}ut\), in which case \(\mathbb{C}ut\) is a loop and the subformula property fails. Tennant’s logic stands on the horns of this dilemma — between a system that is no longer paraconsistent, and a system that is no longer a logic.

References↩︎