Explosion and Cut Required - Inference Systems
Joseph Vidal-Rosset
joseph at vidal-rosset.net
Sat Jun 18 02:10:44 EDT 2022
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
>
More information about the FOM
mailing list