New font stuff, just plain ol' letters, no new punctuation yet:

posed a neat puzzle over dinner: show that the linear exponential ! is not definable using any of the other linear connectives, including unrestricted implication. I think I have a proof now, after one wrong attempt. It goes like this. Suppose we have a propositional expression ψ(A) (not mentioning !) such that ψ(A) |- !A and !A |- ψ(A) for all A. Consider the case where A is an atomic proposition, and look at the proof of ψ(A) |- !A.

We claim that it will never involve the ! right rule. Why? Because the proof will never toss anything into the unrestricted context in any branch where !A is still the goal, so using !-right will always leave us with |- A, which is unprovable. For an illustrative almost-counterexample, ψ(A) might be something like (D ⊃ B) ⊃ C so that after applying ⊃L and the ⊃R we wind up with (among other goals) the goal D; . |- C, but notice that in order to get D in the unrestricted context we had to clobber !A with C. This sequent has no banged subformulae at all, so we certainly can't use !-right.

Now since the proof never decomposes !A on the right at all — indeed the only way it can finish, if you think about it, is by liberal use of the 0-left rule — there is a proof of precisely the same structure that establishes ψ(A) |- 0. By cut admissibility, using the assumption that !A |- ψ(A), we obtain !A |- 0, which quickly leads to a contradiction by inversion on the !-left and (lack of) 0-right rules.
Tags:
• #### (no subject)

After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

• #### (no subject)

Thai curry leftovers for dinner. Got a copy of Hennessy and Patterson's textbook on Architecture, and I am enjoying catching up on all the low-level…

• #### (no subject)

Finally the end is in sight for unpacking my books. Heartstrings are pulled over the desire to slim down and get rid of some of them, but so many are…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic

Your reply will be screened

Your IP address will be recorded

• 11 comments
• #### (no subject)

After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

• #### (no subject)

Thai curry leftovers for dinner. Got a copy of Hennessy and Patterson's textbook on Architecture, and I am enjoying catching up on all the low-level…

• #### (no subject)

Finally the end is in sight for unpacking my books. Heartstrings are pulled over the desire to slim down and get rid of some of them, but so many are…