# Explosion and Cut Required

Joseph Vidal-Rosset joseph.vidal.rosset at gmail.com
Mon Jun 13 03:14:04 EDT 2022

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

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