Gentzen's Cut Elimination theorem: Philosophy Forums

Gentzen's Cut Elimination theorem

Sergei_Trop
Initiate

Usergroup: Members
Joined: Oct 17, 2009

Total Topics: 2
Total Posts: 2

Posted 11/17/09 - 06:43 AM: Subject: Gentzen's Cut Elimination theorem	#1
Hello all! Let me discuss famous Gentzen's Cut Elimination theorem for PURE First Order Logic from his amazing 1934 paper (in which by the way he introduced his Natural Deduction system). Proving this theorem in Constructive Logic Gentzen describe the algorithm transforming every proof with Cut to one without Cut. Therefore the Cut rule (or lemma using) does not bring new theorems of First Order Logic even in Constructive Logic. And even in Constructive Logic our proofs are steel monotone with respect to number of logical symbols and have subformula property. Maybe someone knows some other valuable sides of this pure FOL theorem (motivations, applications, ...)? I am asking that because the motivations/applications of Cut Elimination which I know concern with Gentzen's FREE-Cut Elimination theorem. Thank you for thoughts, Sergei Tropanets

Bourbaki

Usergroup: Members
Joined: May 27, 2009

Total Topics: 1
Total Posts: 19

Posted 11/30/09 - 05:44 PM:	#2
I would suggest reading Gaisi Takeuti's Text entitled Proof Theory and then read S.R. Buss's Handbook of Proof Theory to see some current research related to computer science. I know that in type theory there are some kinds of normal forms (which undoubtedly lend themselves to a handy maniupulation) that require cut elimintation. Takueti's book goes into some of that, though the first result he has is the use of cut elimination in a proof of the consistency of Peano arithmetic (also due to Gentzen, so if you want you could probably read his original papers, though from what I gather Takeuti makes an effort to keep the proof very close to the original).

Sorry, you don't have permission to post. Log in, or register if you haven't yet.