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

CC BY-SA 4.0
2020-10-25T18:10:59.457Z
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.
D.W.
CC BY-SA 4.0
2020-10-25T19:33:12.920Z
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.
David Lehnherr
<curry-howard>
Curry Howard Isomorphism and cut elimination
David Lehnherr
# Curry Howard Isomorphism and cut elimination

(Asked by: username_0 on 2020-10-25)

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?

Best,

David

**Tags:** curry-howard
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  

---

## 0 answers

