Explosion and Cut Required - Inference Systems

[Joseph Vidal-Rosset]

Hello Dennis, hello everyone,

I do not know if all this discussion will be published on FOM, but this
is very probably be my last email on this topic.

Le 16/06/2022 à 18:55, dennis.hamilton at acm.org a écrit :

>   I trust that I am being specific enough now.

Not really, and here is why.

If I have understood correctly what you wrote, you just told me:

(1) The intuitionistic absurdity rule is not welcome in mathematical logic.

(2) I trust Tennant, therefore your argument must be flawed.

Vis-à-vis my paper online, point (1) is irrelevant, because even if I
consider, with many philosophers and logicians,  that the intuitionistic
absurdity rule must be kept on board,  I did not dispute not about
whether Heyting was right against Johansson.

Point (2) is only ad hominem. It is not worth discussing. This kind of
reaction is among the worst in academic discussions.

There is nothing personal in my discussion of Neil's work. I met him
some years ago, and I have very fond memories of that day, and of all of
our private email discussions. I would add that, unlike many colleagues,
I have read many of Neil's books and articles and my discussion should
be seen as a mark of respect and intellectual esteem. But Neil knows
that I was never convinced by IR or Core logic, for good reasons, even
if, of course, Neil and others believe that these reasons are not good.

Now, the discussion with Mario leads me to sum up my argument that I
keep online, because it seems to me flawless, in spite of your opinions,
those of Mario and yours.

1- DNS rules are all derivable in Core logic, under three forms, that I
have called DNS.1, DNS.2 and DNS.3. (Only DNS.3 is invalid in minimal
logic).

2- DNS.1 is provably invertible in Core logic, and I gave a proof of
this fact via an admissible use of the restricted Cut for Core logic.

3- If Core logic is consistent, DNS.1 entails anti-DNS.1, i.e. exactly
the same rule where antisequents replace the sequents of DNS.1. Mario
denies this point, in spite of the fact that it is is provable in
minimal logic that it is *absurd* to hold both the interderivability of
A and B (i.e. the sequents of DNS.1) and to reject the interderivability
of ~A and ~B (i.e. the antisequents). Here the proof of this point in
minimal logic via Slaney's Minlog, a proof that is, of course, *valid in
Core logic*:

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

  | ~(((a -> b) & (b -> a)) -> ((~a -> ~b) & (~b -> ~a)))   ASSUMPTION
  |  | (a -> b) & (b -> a)   ASSUMPTION
  |  | a -> b   &E
  |  | b -> a   &E
  |  |  |  | ~a   ASSUMPTION
  |  |  |  |  | b   ASSUMPTION
  |  |  |  |  | a   arrow_E
  |  |  |  |  | F   arrow_E
  |  |  |  | ~b   arrow_I
  |  |  | ~a -> ~b   arrow_I
  |  |
  |  |  |  | ~b   ASSUMPTION
  |  |  |  |  | a   ASSUMPTION
  |  |  |  |  | b   arrow_E
  |  |  |  |  | a   arrow_E
  |  |  |  |  | F   arrow_E
  |  |  |  | ~a   arrow_I
  |  |  | ~b -> ~a   arrow_I
  |  | (~a -> ~b) & (~b -> ~a)   &I
  | ((a -> b) & (b -> a)) -> ((~a -> ~b) & (~b -> ~a))   arrow_I
  | F   arrow_E

Therefore, because the sequents of DNS.1 are interderivable, there is a
interderivability of antisequents, i.e.  rule anti-DNS.1 that is the
logical consequence of the derivability of DNS.1 in Core logic.

4. The conjunction of anti-DNS.1 and DNS.3 is inconsistent. Therefore
the paraconsistency claim for Core logic i.e. ~A, A |/- B entails an
inconsistency in Core logic.

Q.E.D.

The only possible objection is that, from the Core logician's point of
view, anti-DNS.1 and DNS.3 *cannot have the same context*. The premises
of the former must be considered as consistent, while the latter starts
from a set of premises that is inconsistent. Application of the
restricted Cut for Core logic is legal to prove the interderivability of
premises of DNS.1 only if the premises of this rules are not inconsistent.

Is this objection decisive?

The trouble is that
1- we do not need such a presupposition to prove in minimal logic that
DNS rule is invertible.
2- the claim of antisequent ~A, A |/- B entails not the least difficulty
in minimal logic, by contrast with Core logic, where it is clearly
necessary to presuppose a distinction between consistent set of premises
and inconsistent set of premises to try to avoid such a catastrophe.
Strange "logic", really.

All the best,

Jo.