Explosion and Cut Required - Inference Systems
Mario Carneiro
di.gama at gmail.com
Fri Jun 17 04:25:25 EDT 2022
On Fri, Jun 17, 2022 at 2:57 AM Joseph Vidal-Rosset <joseph at vidal-rosset.net>
wrote:
>
> Now, I had only time this morning to check via Minlog that DNS.1 is
> provably invertible in minimal logic and here is a proof *without
> detour* i.e. a normal proof that is, of course, a proof in Core logic:
>
> SEQUENT 1: (((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b)) & (((x &
> a) -> b) -> ((x & ((a -> b) -> b)) -> b))
>
> |- (((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b)) & (((x & a) -> b)
> -> ((x & ((a -> b) -> b)) -> b))
>
> | | (x & ((a -> b) -> b)) -> b ASSUMPTION
> | | | x & a ASSUMPTION
> | | | x &E
> | | | a &E
> | | |
> | | | | | a -> b ASSUMPTION
> | | | | | b arrow_E
> | | | | (a -> b) -> b arrow_I
> | | | x & ((a -> b) -> b) &I
> | | | b arrow_E
> | | (x & a) -> b arrow_I
> | ((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b) arrow_I
>
> | | (x & a) -> b ASSUMPTION
> | | | x & ((a -> b) -> b) ASSUMPTION
> | | | x &E
> | | | (a -> b) -> b &E
> | | | a Double_Negation
> | | |
> | | | x & a &I
> | | | b arrow_E
> | | (x & ((a -> b) -> b)) -> b arrow_I
> | ((x & a) -> b) -> ((x & ((a -> b) -> b)) -> b) arrow_I
> (((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b)) & (((x & a) -> b) ->
> ((x & ((a -> b) -> b)) -> b)) &I
>
> I do not translate this proof in Core logic's style i.e. in Gentzen's
> style with parallel elimination rules. I do not have time, but there
> must be no problem for such a translation.
>
Okay, challenge accepted. I'll focus on the first conjunct there, which is
reverse-DNS.1, since I do not contest the second part being provable in
core logic.
[Proof 1]
(x & ((a -> b) -> b)) -> b ASSUMPTION
| x & a ASSUMPTION
| x &E
| a &E
|
| | | a -> b ASSUMPTION
| | | b arrow_E
| | (a -> b) -> b arrow_I
| x & ((a -> b) -> b) &I
| b arrow_E
(x & a) -> b arrow_I
Removing a bit more of the "spurious" operators used to reflect the
turnstile:
[Proof 2]
1. (x & ((a -> b) -> b)) -> b ASSUMPTION
2. x ASSUMPTION
3. a ASSUMPTION
4. | | a -> b ASSUMPTION
5. | | b arrow_E 3, 4
6. | (a -> b) -> b arrow_I 4-5
7. x & ((a -> b) -> b) &I 2, 6
8. b arrow_E 1, 7
Adding in the hypotheses using Gentzen-style |- instead of fitch-style |
brackets:
[Proof 3]
1. |- (x & ((a -> b) -> b)) -> b ASSUMPTION
2. x, a |- x hyp
3. x, a |- a hyp
4. x, a, a -> b |- a -> b hyp
5. x, a, a -> b |- b arrow_E 3, 4
6. x, a |- (a -> b) -> b arrow_I 5
7. x, a |- x & ((a -> b) -> b) &I 2, 6
8. x, a |- b arrow_E 1, 7
and minimize hypotheses to only those used in the step:
[Proof 4]
1. |- (x & ((a -> b) -> b)) -> b ASSUMPTION
2. x |- x hyp
3. a |- a hyp
4. a -> b |- a -> b hyp
5. a, a -> b |- b arrow_E 3, 4
6. a |- (a -> b) -> b arrow_I 5
7. x, a |- x & ((a -> b) -> b) &I 2, 6
8. x, a |- b arrow_E 1, 7
We're starting to have a problem here since step 1 doesn't quite look right
- the assumption should actually be x, ((a -> b) -> b) |- b, but making
that modification is going to mess up the last few steps. First we can
eliminate the "spurious" -> in the assumption:
[Proof 5]
1. x & ((a -> b) -> b) |- b ASSUMPTION
2. x |- x hyp
3. a |- a hyp
4. a -> b |- a -> b hyp
5. a, a -> b |- b arrow_E 3, 4
6. a |- (a -> b) -> b arrow_I 5
7. x, a |- x & ((a -> b) -> b) &I 2, 6
8. x, a |- b cut 1, 7 <- !!!!
then the '&':
[Proof 6]
1. x, ((a -> b) -> b) |- b ASSUMPTION
2. x |- x hyp
3. a |- a hyp
4. a -> b |- a -> b hyp
5. a, a -> b |- b arrow_E 3, 4
6. a |- (a -> b) -> b arrow_I 5
8. x, a |- b cut 1, 2&6
we actually don't need to cut with 2 here because it just gets carried
along, so we get:
[Proof 7]
1. x, ((a -> b) -> b) |- b ASSUMPTION
3. a |- a hyp
4. a -> b |- a -> b hyp
5. a, a -> b |- b arrow_E 3, 4
6. a |- (a -> b) -> b arrow_I 5
8. x, a |- b cut 1, 6
and this is exactly the proof that I wrote in my previous message. The
proofs 5-7 here involve cut, and when you use the cut' rule with consequent
b or #, they would all degenerate to being a proof of # instead of b when
step 1 is the natural proof of ~a, ((a -> b) -> b) |- b.
In fact, the issue appears even earlier than that: all the way back to
proof 3 (which is where we distinguish between step 1 being a "deduction
hypothesis" representing an arbitrary derivation, and steps 2 and 3 which
are regular hypotheses which appear before the turnstile), we have an
invalid use of the arrow_E rule, because in core logic the major premise of
an MP application must be a hypothesis, not a subproof (and step 1
represents a subproof). That is, proofs 3-4 would work to prove
(x & ((a -> b) -> b)) -> b, x, a |- b
but not
x, ((a -> b) -> b) |- b
-----------------------
x, a |- b
In the end, what we actually deduce is that:
x, ((a -> b) -> b) |- b
-----------------------
x, a |- b/#
which is to say, if x, ((a -> b) -> b) |- b is derivable in core logic for
some x,a,b, then either "x, a |- b" or "x, a |- #" is derivable in core
logic. This is actually pretty close to the original minimal logic theorem,
and useful enough for proving theorems like "core logic proves all closed
theorems from intuitionistic logic", but it is different enough to what you
are after as to break your proof, because the "or 'x, a |- #'" part cannot
be ignored here.
I disagree, because for the Core logician, B is not # (i.e. the falsity
> or absurdity constant, bot, F, etc.)
>
Right, B and # are different and this makes all the difference in this
case. You are trying to find a way to prove ~A, A |- B but you only got a
proof of ~A, A |- #.
The only difference between Core
> logic and minimal logic (except, of course, the relaxed rule VE and rule
> -> I that replaces bot E, rules that are not in minimal logic) is that
> in Core logic, there is no vacuous discharge, i.e. no Weakening on the
> left when there is a contradiction on the left of the turnstile.
As mentioned above, another important difference is the fact that the
arrow_E rule only works on hypotheses, not on subproofs. You have to use
the cut' rule to "apply arrow_E to subproofs" but this has a possibility of
"upgrading" your consequent from B to # which is what you are trying to
avoid in this case.
> 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. If you have a proof of X |- B then you can deduce X
|- A -> B (although X might lose an occurrence of A if it has one). This is
still true in the case X |- bot ==> X |- A -> bot. For example:
B, (B -> bot) |- bot
is derivable, so
B, (B -> bot) |- A -> bot
is also derivable. Here's a proof:
1. B |- B hyp
2. bot |- bot hyp
3. B, (B -> bot) |- bot arrow_E 1, 2
4. B, (B -> bot) |- A -> bot arrow_I 3
> This ban allows the Core logician to
> claim that the following sequent
>
> bot |- ~B
>
> is unprovable in Core logic, by contrast with minimal logic.
I think the reason you can't prove the latter is that if you apply not_I
then you are left with the goal of proving "B, bot |- #" and there is no
obvious way to involve B in the proof here, since if we use bot to deduce
the unsatisfiability of the hypotheses then this yields a proof only of
"bot |- #" with no extra B hanging off.
> The only claim of the
> "minimal logician" is that if you accept a contradiction in the premises
> of your theory, you can prove that any sentence is false. Such a claim
> does not sound so "irrelevant".
>
The core logician would counter that it would be nice to be told (by the
logic or otherwise) that the hypotheses are inconsistent, and not waste
time writing down random sentences that have nothing to do with the
refutation. You ask the logic "does X |- A?" and it responds "X |- #" and
you say "...that's not what I asked, but I guess I don't need to do the
next step of the proof after this (use A to deduce something else) then".
Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220617/7f04ff9d/attachment-0001.html>
More information about the FOM
mailing list