Explosion and Cut Required - Inference Systems

[Mario Carneiro]

On Fri, Jun 17, 2022 at 11:15 AM Joseph Vidal-Rosset <
joseph at vidal-rosset.net> wrote:

>
> Le 17/06/2022 à 10:25, Mario Carneiro a écrit :
>
> >>     In ND
> >>    for Core logic
> >>
> >>        B
> >>    ------ -> I
> >>    A -> B
> >>
> >>     is allowed, by contrast with
> >>
> >>        bot
> >>    --------- -> I
> >>     A -> bot
> >>
> >>    which is not allowed in Core logic.
>
> > Those are both allowed.
>
> No, they are not both allowed, you are wrong!
>
> See for example "Autologic", p. 189, where  Tennant repeats that IR
> “requires non-vacuous discharge of assumptions,” but he adds in footnote
> 6 on the same page, “except, crucially, in one half of the rule of
> implication introduction!” This means that it is only for the other half
> of implication introduction (i.e. for the conditional introduction rule
> that allows the derivation of
> ~A |- A->B ) that vacuous discharge (i.e. weakening) is forbidden.
>

The one half that Tennant is talking about in that footnote is exactly the
half being used here. In core logic there is no special behavior that
associates to particular substitutions of a formula: a generic description
of a derivation like X |- B ==> X\{A} |- A -> B is true for any
substitution to the formulas A and B, including bot. That is, it is
possible to have core logic proofs that manipulate "bot" (which I will
write as "F") in the consequent position, as distinct from proofs that end
in # (which is not a formula and cannot appear in implications). The two
forms of the conditional implication rule are:

->Ra: X, A |- # ==> X |- A -> B
->Rb: X |- B ==> X\{A} |- A -> B

These rules are never simultaneously applicable, because the first one only
applies to a sequent of the form X |- # (and remember, # is not a formula)
and the second one only applies to a sequent of the form X |- B with a
formula on the right. If B happens to be F, you would still need to use the
second form, because "F" is a formula. The ->Rb rule allows for vacuous
discharge, as evidenced by the way the hypotheses are written in the rule:
it removes A from the hypotheses if present, but if it's not present then
the rule still applies. Only the ->Ra rule forbids vacuous discharge.

You talk about the conditional introduction rule that allows the derivation
of ~A |- A -> B, and this is ->Ra which indeed forbids vacuous discharge.
But I don't see how this matches the ->I scheme you presented, which has
the form F ==> A -> F (you omitted the context for some reason? I guess it
would be X |- F ==> X\{A} |- A -> F) which clearly matches ->Rb, not ->Ra,
since the hypothesis "X |- F" ends in F and not #. If when you wrote "bot"
you actually meant #, then A -> # is not well formed in the consequent of
the rule (# isn't a formula).

When you wrote
>
> x, ((a -> b) -> b) |- b
> -----------------------
> x, a |- b/#
>
> to contest that the invertibility of DNS.1 is provable in Core logic, I
> am afraid you show that the Core logician falls into formal sophistry. I
> understand that this means that if {x,a} is inconsistent, then # instead
> of b,


No, that's not what I meant. The determination of whether the Cut algorithm
returns a derivation of "x, a |- b" or "x, a |- #" does not depend on
semantic properties like the consistency of {x, a} but rather on the Cut
algorithm itself. There is no simpler way to determine it other than to run
the algorithm on the derivations and find out which one you get. For the
particular case of your derivations, you get a proof of "~A, A |- #".

in other words, the conclusion is  x, a |- b if and only if
> x, a |/- # .


No, it's not an if and only if. Clearly if x, a |- # then {x, a} is
inconsistent (since we can easily read a classical proof of ((x & a) -> F)
from the core proof), but x, a |- b does not imply that {x, a} is
consistent, or that x, a |/- #. For example:

1. a |- a   (Ax.)
2. a & ~b |- a   (L/\ 1)
3. b |- b   (Ax.)
4. a & ~b, a -> b |- b   (L-> 2, 3)

Here we have a core proof of "a & ~b, a -> b |- b" such that the
assumptions are unsatisfiable but nevertheless does not end in #. Here's
another proof from the same set of hypotheses that does end in #:

1. a |- a   (Ax.)
2. b |- b   (Ax.)
3. ~b, b |- #   (L~ 2)
4. a, ~b, a -> b |- #   (L-> 1,3)
5. a & ~b, a -> b |- #   (L/\ 4)

I prefer to stop this discussion now, because we are in a dead end, like
> if  you persisted in denying  that 1 + 1 = 2.


It is tiresome for me as well, but I'm not sure how else to resolve the
situation. This is why you should do your proofs formally; so many of these
issues seem to simply be type errors that a bit of formalization would
solve.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220617/31b3c7df/attachment.html>