Explosion and Cut Required

[Joseph Vidal-Rosset]

Hello Mario, hello everyone,

Le 16/06/2022 à 06:20, Mario Carneiro a écrit :
> You have not established this (specifically, the reverse direction
>
> X, (A -> B) -> B  |- B
> ----------------------------- anti-DNS.1
>            X, A |- B
>
> ). While this may be true in minimal logic, I'm fairly certain the proof
> involves an invalid use of Cut which prevents transferring the proof as
> is. It's obviously suspicious to a Core logician because B "comes out of
> nowhere" in the consequent but it is perfectly well relevant to the
> hypotheses in the antecedent of the rule.
>
> Everything about equivalence and anti-sequents etc is irrelevant to
> establishing this claim, which you have not proved.
>
>     I am sorry to tell you that analogies, suggestions and feelings cannot
>     be considered as rebuttals.
>
>
> I would hope that "this step is false because it uses a rule that isn't
> a rule" is considered as a rebuttal! You have a tendency not to focus on
> that step but it's really the important one and it deserves to be
> treated more explicitly.

Let's go.

Again I guess that you meant DNS.1 (because it makes no sense both to
talk about a rule on anti-sequents and to write only sequents in this
rule). Your point is that I used an *unrestricted Cut* to prove the
invertibility of DNS.1 and therefore this invertibility stays unproved
for the Core logician who would be constrained to recognize only the
derivability of DNS.1, but *not* its invertibility; therefore

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

would be banned from Core logic, because the Core logician aims at
avoiding this catastrophic derivation:

                 ------ Ax.
                 A |- A
             ----------  L~
             ~A, A |-
----------------------- DNS.3
~A, (A -> B) -> B |- B
  ----------------------- reversed-DNS.1
             ~A, A |- B

But note that the so-called restricted Cut for Core logic leads to conclude:

                ------- Ax.
                 A |- A
             ----------  L~
             ~A, A |-
----------------------- DNS.3
~A, (A -> B) -> B |- B
  ----------------------- reversed-DNS.3  (i.e. restricted Cut)
              ~A,A |-



I recall that, explaining the use of the *unrestricted Cut*, Tennant
wrote, in Core logic, p. 152:

> That secures, in the time-honored words of Russell, all the advantages of
> theft over honest toil.

That provides a sum-up of the issue of this discussion: where is really
the fraud? In the use of the *unrestricted* Cut or, on the contrary, in
its replacement by a *restricted* version of Cut? Logicians on this list
should give their judgment.

In fact, the so-called restricted Cut that is admissible in Core logic
is a kind of "If Then Else". In our case, it says to the Core logican:
"if the set of premises in  DNS.1 is consistent, then inversion is
allowed, otherwise reverse DNS.3 " In other words no inversion (i.e.
Cut) is allowed if that leads to the derivation of the terrible First
Lewis's Paradox, the Core logician's nightmare.  But, in my opinion, it
sounds like a situation where a surgeon tells his nursing team: "if the
thermometer shows a patient has no fever, note it in the report,
otherwise change to a thermometer that never shows a fever, that's
better." (A strange "epistemic gain".)

Now, I stress on this last point that concerns DNS.2 i.e.

     X, A |-
-------------- DNS.2
X, ~ ~ A |-

Even the Core logician cannot contest that it is syntactically
equivalent to

                 X, A |- bot
---------------------------  DNS.2
X, (A -> bot) -> bot |- bot

("bot" being provably equivalent to any contradiction of this form
~ ~ B & ~ B )

Everyone knows that DNS.2 is valid because (~ ~ ~ A <-> ~ A) is a
*theorem* in Core logic as well as in minimal logic. It means that, with
DNS.2, even the Core logician does not care about the formulas in set X.
Like the minimal logician, he says that DNS.2 is valid, because it is
provable that

    ~ A |-
==========
  ~ ~ A |-

  i.e.

                 A |- bot
========================
(A -> bot) -> bot |- bot

the double line meaning that this is an invertible derivation and this
absence of X meaning that X can be void : provided that the right of the
turnstile is void or bot, A and (A -> bot) -> bot are interderivable or
equivalent.  But this equivalence suddenly disappears for the Core
logician in the following derivations that are no longer valid in
minimal logic, but that are provable in Core logic:


                 A |- bot
========================
     (A -> B) -> B |- B


                 A |- bot
========================
(A -> bot) -> bot |- B


Slaney's prover can prove these derivations with the -i option to get
the intuitionistic logic system:

  SEQUENT 1:   ~ a -> (((a -> b) -> b) -> b)
  |- ~a -> (((a -> b) -> b) -> b)

  | ~a   ASSUMPTION
  |  | (a -> b) -> b   ASSUMPTION
  |  | a   Double_Negation
  |  | F   arrow_E
  |  | b   Bot_E
  | ((a -> b) -> b) -> b   arrow_I
~a -> (((a -> b) -> b) -> b)   arrow_I


  SEQUENT 2:  ~a -> (((a -> F) -> F) -> b)
  |- ~a -> (~~a -> b)

  | ~a   ASSUMPTION
  |  | ~~a   ASSUMPTION
  |  | F   arrow_E
  |  | b   Bot_E
  | ~~a -> b   arrow_I
~a -> (~~a -> b)   arrow_I

It's easy to get the Core logic version of these proofs: just delete the
line Bot_E, copy and paste the same proofs.

That is why I consider that is a very clear case of use without mention
of the intuitionistic absurdity rule, and the obvious fraud consists in
denying it firmly. Why? Because the only thing that the Core logician
does is to postpone the irrelevant conclusion to the conclusion of the
conditional, and he is happy with it. Contrarily to what we have to do
in minimal logic, he interprets the absurdity constant in this case as a
logical constant that allows the use his "new" rule for conditional on
the right, in replacement of rule Lbot i.e. Weakening on the left.
Contrarily to what Tennant said, the Core logician in this situation
wants all the advantages of theft (that of the intuitionistic absurdity
rule) over honest toil (that consists in recognizing clearly the use of
this tool).

My point in this paper is that, if you do *not* presuppose the
consistency or inconsistency of the set of premises in  DNS.1 rule, like
you do when you're reasoning in minimal logic or in intuitionistic
logic, and if you assume only that your logical system is consistent and
that your propositional calculus is sound, then you have to admit that
this rule is both derivable and invertible and  that it involves an
invertible rule for antisequents, that is anti-DNS.1. If the Core
logician accepts the same conditions (that were accepted by Johansson as
by Heyting as well), he cannot deny that his system cannot be
consistently claimed to be paraconsistent. But the Core logician
persists in  playing another game with his own rules. It is exactly the
way of fraudsters or thieves.

All the best,

Jo.