I am currently reading about the proof for the isomorphism between Gentzen's sequent calculus $G$ and the simply typed lambda calculus $\lambda(\rightarrow,\times)$. The proof assumes the cut-free representation of proofs in $G$. I fail to see the necessity for this assumption (besides that it may shorten the proof). What am I missing?



  • 1
    $\begingroup$ The standard way to figure that kind of thing out is to understand the proof and check where that assumption is used and whether each step would be valid in the absence of that assumption. I suggest you go through that exercise and use it to elaborate on your question. $\endgroup$
    – D.W.
    Oct 25, 2020 at 18:10
  • $\begingroup$ Thanks for the suggestion. I tried to do that, but I couldn't find a flaw. I think that it has to do with the normalization property (i.e. proofs as programms). However, I fail to formalize an argument. $\endgroup$ Oct 25, 2020 at 19:33


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.