Explosion and Cut Required - Inference Systems

[Joseph Vidal-Rosset]

Sorry for the html ....

Here what is I pasted:

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

  |  | a -> b   ASSUMPTION
  |  |  | (a -> b) -> b   ASSUMPTION
  |  |  | b   arrow_E
  |  | ((a -> b) -> b) -> b   arrow_I
  | (a -> b) -> (((a -> b) -> b) -> b)   arrow_I

  |  | ((a -> b) -> b) -> b   ASSUMPTION
  |  |  | a   ASSUMPTION
  |  |  | a -> b   Double_Negation
  |  |  | b   arrow_E
  |  | a -> b   arrow_I
  | (((a -> b) -> b) -> b) -> (a -> b)   arrow_I
((a -> b) -> (((a -> b) -> b) -> b)) & ((((a -> b) -> b) -> b) -> (a ->
b))   &I

Le 17/06/2022 à 19:12, Mario Carneiro a écrit :
>
>
> On Fri, Jun 17, 2022 at 11:15 AM Joseph Vidal-Rosset
> <joseph at vidal-rosset.net <mailto: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
>