p
e
r
s
o
n
a
l |
FALSE! (2)
(15 Oct 2003 at 12:49) |
A ha, well, after fixing the logic and getting 13 pages into a new proof, I found another counter-example. The following sequent has no derivation:
*; *; { []A } ==> A
However,
*; *; { [] A } ==> [] A
and
*; []A; { [] A } ==> A.
I have a fix for the logic, but it may totally ruin the proof. Argh!
google search for 'cut admissibility is false rules': 5940 results (10 fewer than last time, though now my page is listed as the first hit!)
google search for 'cut admissibility is false sucks': 36 results (3 more than last time, with my page again as the first hit)
The trend is definitely towards this sucking more than ruling... |  |
|
|
|
|