Explosion and Cut Required

[Mario Carneiro]

Hi all,

I have had a long discussion in private correspondence with Joseph about
this particular proof of his, and since he is posting a version of the same
argument on FOM I shall also share my conclusions for the broader
consumption.

On Sun, Jun 12, 2022 at 6:05 PM Joseph Vidal-Rosset <
joseph.vidal.rosset at gmail.com> wrote:

> - 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
>

>From what I can tell, these deductions are correct.

- 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
>

This deduction, however, is not correct. It is the contrapositive of the
following rule:


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

and there is no way to make this deduction in Core logic. Or at least,
Joseph was not able to provide a direct proof of this (the reasoning below
about equivalence has to be taken to talk about the metalogic in which Core
logic is being discussed, and in any case it does not help since it
presupposes this deduction to be valid), and moreover it is in
contradiction to Tennant's theorem on the relevance-preservation properties
of core logic, by exactly the deduction that Joseph uses later:

     ------------ not-elim
       ~A, A |-
---------------------- DNS.3
~A, (A -> B) -> B |- B
---------------------- anti-DNS.1
        ~A, A |- B

Since the final line of the proof is not derivable but DNS.3 and not-elim
clearly are, we conclude that there is no way to prove anti-DNS.1 in Core
logic. Joseph buries the lede by referring to DNS.1 as an *invertible* rule
and so implying the derivability of anti-DNS.1 without showing it.

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...
>

The insinuation that no objections have been raised to the proof is false,
as Joseph well knows.

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220612/fdbbb5f6/attachment-0001.html>