Explosion and Cut Required

[Joseph Vidal-Rosset]

Hello Vaughan, hello everyone

(I met a problem with my email client, I hope that this email will not 
be sent twice. If it is the case,  I apologize.)

Le   mer.   06/08/22   juin   2022  à   11:04:01   ,   "Vaughan   Pratt"
<pratt at cs.stanford.edu> a envoyé ce message:
 > But if it is, then it would be nice to have a short proof showing that
 > while CA --> can arise in Core  Logic, CA |-- cannot.  Or however Core
 > Logic distinguishes them.

The Core logician's slogan is "relevance  at the level of the turnstile"
(it is  repeated many  times in  Tennant's book  on Core  logic).  The
*unprovability* of sequent


¬ A, A |-  B           (1)


i.e.  the *antisequent*

¬ A, A |/- B           (2)

is undoubtedly the main claim  of Core logic i.e.  the "intuitionistic
relevant logic"  i.e.  *IR*,  where all intuitionistic  *theorems* are
provable,  but  where  no  irrelevant  logical  *sequent*  like  (1)  is
deducible.  In Tennant's book on Core logic, p. 195, formula


¬ A, A |/= B

is  claimed from  the Core  logic's point  of view.  Therefore (2)  is
certainly also  claimed by  the Core logician  (because Core  logic is
claimed to be sound and complete).

Now,  here is  my argument  against  the claim  of (2)  from the  Core
logic's point  of view: the claim  of (2) leads Tennant's  theory to a
contradiction  and   therefore  it  is   false  that  Core   logic  is
paraconsistent, contrarily to  what Tennant wrote (p. 156  of his book
on Core logic).

Proof:

- First, it is provable that these *invertible* rules that I call
   "DNS1"  and "DNS.3"  are *derivable*  in sequent  calculus for  Core
   logic and  therefore these  rules belong  to Core  logic. (I  do not
   reproduce the Core-derivations of these rules in this email.)


             X, A |- B
---------------------- DNS.1
X, (A -> B) -> B |- B



             X, A |-
---------------------- DNS.3
X, (A -> B) -> B |- B


- Second, *if Core logic is consistent*, this rule for antisequents must
   also be accepted as *valid* in Core logic:

             X, A |/- B
---------------------- anti-DNS.1
X, (A -> B) -> B |/- B

Reason:  the following  sequent is provable in Core logic

A ->  B, B -> A |- (¬B ->  ¬A) & (¬A -> ¬B)         (3)


Let us interpret A  and B as the premise and  conclusion of rule DNS.1
(which are provably *interderivable*), then the logical consequence of 
DNS.1 must be the  invertible rule for antisequents  ¬A and ¬B hat  I 
have called "anti-DNS.1".

Note that the  Core logician cannot reject such  a consequence without
making Core logic inconsistent, as it  is provable via  the trees
method for intuitionistic logic. Indeed, once the left part of sequent
(3) is asserted ( and in our interpretation, rule DNS.1), the Core 
logician cannot  without contradiction  refuse  to assert  the  formula 
on  the right, included our interpretation i.e. anti-DNS.1.  If sequent 
(3) is valid for Core logic, then, by  definition, *no interpretation* 
of A and B is supposed to falsify this sequent,  and if it were the 
case, the sequent  calculus for  propositional  Core logic  could 
logically  prove inferences that can be false; that's clearly not an option.

3. Last, the following  deduction proves that antisequent  (2) cannot be
    claimed by the Core logician without contradiction, because, if (2)
    is claimed in Core logic, we can deduce from this theory the 
following  contradiction:

            X, A |/- B                            X, A |-
--------------------- anti-DNS.1 ----------------------- DNS.3
X,(A -> B) -> B |/-B                 X, (A -> B) -> B |- B
------------------------------------------------------------
                          #


Replacing set of formulas X by ¬A, we get:


            ¬A, A |/- B                            ¬A,A |-
---------------------- anti-DNS.1    ----------------------- DNS.3
¬A,(A -> B) -> B |/-B                ¬A, (A -> B) -> B |- B
------------------------------------------------------------
                          #


      Therefore, antisequent (2) cannot be  claimed in Core logic without
      making  Core logic  inconsistent,  and if  Core  is consistent,  it
      cannot be paraconsistent, contrarily to what Tennant claims.

     Q.E.D.

     (Remark :  in minimal logic, only  the premise on the  left in the
    deduction above is accepted, rule DNS.3 is *not* valid only in
    minimal logic. By contrast, in  intuitionistic logic, DNS.3 is valid,
    and that's why antisequent (2) is rejected as false.  The Core logician
    both claim  (2) and allows the  derivation of rule DNS.3. It can't
    work  unless my  argument is  incorrect  for some  plain and  simple
    reason that I do not see.)

For       more      details,      see       my      paper       online

https://www.vidal-rosset.net/paraconsistent_tennants_logic_is_inconsistent.html

Best wishes,

Jo.

PS:  I  would certainly have  been  happy  to publish  this  argument
elsewhere,  but it  was brutally  rejected by  a referee  of a  famous
international  review  whose name  I  will  keep silent,  without  the
slightest  start  of discussion  and  with  the following  conclusion  :
"Author appears  not to understand just  how exigent the notion  of Core
Proof is."  A very harsh conclusion  for a not very  exigent report. Too
bad...  But since my university career is  coming to an end, I no longer
need to  publish in prestigious  journals and I  don't care.  I  am more
interested in open and free discussions  online.  Many thanks to the FOM
list editors.  Is my argument flawless  or not? Surprisingly, I have not
received at the moment the least  objection via the comment engine of my
blog...