Tuesday, 6 August 2013

proof in sequent calculus LK

proof in sequent calculus LK

I was reading a book that uses sequent calculus (and calls than Natural
deduction ) and that mentions as rules
X ; A |- B
---------------- ->I
X |- A -> B
and
X |- A -> B
Y |- A
---------------- ->E
X ; Y |- B
I wanted to rewrite proof from this book to an original sequent calculus
proof in the original sequent calculus (Gentzens LK system)
http://en.wikipedia.org/wiki/Sequent_calculus
http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508
the rule ->I above is in Gentzen's system FES or in modern language ->R
but the rule ->E does not exist
How to derive ->E in LK?

No comments:

Post a Comment