Explosion and Cut Required

[Joseph Vidal-Rosset]

Le 13/06/2022 à 00:36, Mario Carneiro a écrit :

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

Hello Mario, hello everyone

I made no "insinuation", Mario. Please, read carefully what you quote. I 
meant public objection, that is to say objection either published via 
isso, the comment engine of my blog, or on this list, for example. So, 
many thanks to you for this objection on the list.

I insist on the point that it is the consistency assumption that leads 
to assert anti-DNS.1 via DNS.1. I already replied to you, Mario,  in our 
private correspondence, that this way of deduction is *perfectly legal* 
in proof theory and I quoted as an example this post sent by Rob Arthan 
to prove that is Sigma is consistent and Sigma |- A, then Sigma Union 
{A} is also consistent:

https://math.stackexchange.com/questions/2732615/prove-that-if-%CE%A3-is-consistent-and-%CE%A3-vdash-a-then-%CE%A3-%E2%88%AA-a-is-consisten

I pointed out to you that this argument is valid in minimal logic, 
because it is provable in minimal logic as in Core logic that

A -> B, B -> A |- (~B -> ~A) & (~A -> ~B)

A and B being interpreted by the sequents of DNS.1, the deduction of 
anti-DNS.1 is involved in Core logic, if Core logic is consistent with 
it own propositional calculus and if it is consistent "tout court".

Semantically, the above sequent is transparent: it says, if A is true if 
and only if B is also true (that is to say, A and B are equivalent), 
therefore B is false if and only if A is false. Let us replace A and B 
respectively by top (the truth constant) and ~bot (the negation of the 
absurdity constant), we have:

top -> ~bot,  ~bot -> top |- (~ ~bot -> ~top) & (~top -> ~ ~ bot)

It is trivial to prove that the negation of this last sequent is an 
inconsistency, and even *is* the definition of inconcistency, because it 
is reducible to

top |- bot

i.e.

|- bot

that is to say an absurdity.

Therefore, if Core logic avoids this absurdity, that is to say if it is 
a consistent system, because DNS.1 is derivable and invertible, 
anti-DNS.1 must be valid in Core logic too.

Last, I do not understand the "derivation" that you wrote:

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

That make no sense: antisequent rules are about antisequents and not 
sequents , the label anti-DNS.1 is probably a mistake and you meant DNS.1:

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


A derivation that is indeed valid in minimal logic (a paraconsistent 
logic) and it shows only that if DNS.3 is derivable (and it is derivable 
via the "new" rule for conditional introduction that replaces the 
intuitionistic absurdity rule) then this last sequent is also derivable 
(because DNS.1 is invertible)  "in contradiction to Tennant's theorem on 
the relevance-preservation properties of Core logic". Therefore the 
contradiction is indeed in the paraconsistency that the Core logician 
claims for his system. But your deduction goes further than my own 
argument, Mario, and it is very interesting. Again, many thanks to you.

All the best,

Jo.