Explosion and Cut Required - Inference Systems

[Mario Carneiro]

I appreciate the summary of the argument as it currently stands. You
misapprehend my objection however: I have no problem at all with step 3,
and (A <-> B) -> (~A <-> ~B) is very obviously derivable. You focus a lot
on this step but give short shrift to the actually flawed step which is
step 2. I have been asking for a direct proof of your claim that
reverse-DNS.1 is derivable but I have received only a reference to a proof
on your website that apparently proves X, A |- B ==> X, A |- B and does not
use Core rules: in particular Cut appears and you have not used it
correctly. If I interpret this proof charitably as a way to show X, (A ->
B) -> B |- B ==> X, A |- B, I get:

1. X, (A -> B) -> B |- B (Hyp)
2. A |- A  (Ax.)
3. B |- B  (Ax.)
4. A, A -> B |- B (L-> 2,3)
5. A |- (A -> B) -> B (R-> 4)
6. X, A |- B (Cut 1,5)

The last step very clearly uses Cut, which is not a rule of Core logic. The
thing that was proven admissible is not exactly this rule but rather

6. X, A |- B/# (Cut' 1,5)

where the determination of whether the consequent is B or # depends on
details of the two derivations 1 and 5 that were used (and since 1 is an
arbitrary hypothetical derivation we cannot evaluate it to say which it
is). In the case of interest, X = ~A and 1. is proved by applying DNS.3 to
the trivial proof of ~A, A |- #, and for this choice of derivation step 6
evaluates to the trivial proof of ~A, A |- #.

PS: You often turn to minimal logic provers in order to make a point about
derivability of this or that, but while doing so you ignore the difference
between A, (B -> C) |- D ==> E |- F and (A -> ((B -> C) -> D)) -> (E -> F).
For core logic specifically, this is not okay: core logic for pure formulas
involving implication looks basically like classical logic, but there are
various effects that appear only "at the level of the turnstile" as you
well know, so you can't argue that just because the latter is derivable the
former must also be derivable.

On Thu, Jun 16, 2022 at 3:43 PM Joseph Vidal-Rosset <joseph at vidal-rosset.net>
wrote:

> 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.
>
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220617/3f8dc690/attachment-0001.html>