Explosion and Cut Required

[Mario Carneiro]

On Wed, Jun 15, 2022 at 7:07 PM Joseph Vidal-Rosset <joseph at vidal-rosset.net>
wrote:

> If you talk about this substitution in my paper online  (
>
> https://www.vidal-rosset.net/paraconsistent_tennants_logic_is_inconsistent.html
> ), where A is interpreted by this sequent
>
> X, A |- B
>
> and B by this one:
>
> X, (A -> B) -> B |- B
>
> then I repeat that it is provable in minimal logic that these sequents
> are interderivable. I have called this rule DNS for "Double Deduction à
> la Slaney" (that is in fact the reducibility of triple negation to one
> negation, B being most often the absurdity constant):
>
>               X, A |- B
> ====================== DNS
> X, (A -> B) -> B  |- B
>
> because it was implemented by Jonh Slaney for his prover for minimal
> logic. Derivable in minimal logic, it is not surprising at all that it
> is also derivable in Tennant's Core logic.
>

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.

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