[ back to Tom 7 Radar ]

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...
p
o
s
t

a

c
o
m
m
e
n
t
[ Tom 7 Radar  •  Tom 7 on Google+  •  on Twitter  •  on Facebook ]