<ol>
<li><p>How “standard” is it? A <a href="https://prooftheory.blog/2020/09/07/simple-proofs-of-cut-elimination-ii-intuitionistic-logic/" rel="nofollow noreferrer">post by Anupam Das on the proof theory blog</a> attacks the folklore by comparing the following two results:</p>
<blockquote>
<p>Proposition 1 (Folklore). For any theorem A of IPL, we can compute a cut-free LJ proof of A in exponential time and polynomial space in |A|.</p>
</blockquote>
<blockquote>
<p>Theorem 3 (Statman ’79). Deciding whether two simply typed <span class="math-container">$\lambda$</span>-terms reduce to the same normal form is not elementary recursive.</p>
</blockquote>
<p>He then remarks:</p>
<blockquote>
<p>[...] Statman’s result does not imply any lower bounds on the complexity of cut-elimination for LJ, since normalisation of <span class="math-container">$\lambda$</span>-terms constitutes just one particular strategy for cut-elimination. Note in particular, that both Proposition 1 and Theorem 3 are perfectly consistent with each other.</p>
</blockquote>
</li>
<li><p>Nevertheless, let me mention two works in this direction that help clarify the link. Consistently with the previous remark, they assume a strategy corresponding to the negative polarisation of logic (corresponding to call-by-name reduction in the λ-calculus). But even with this assumption the result is deeper than it looks, relating global transformations (substitution) with local ones (from cut-elimination).</p>
<ul>
<li>Hugo Herbelin. 1994. <em>A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure</em>. <a href="https://doi.org/10.1007/BFb0022247" rel="nofollow noreferrer">https://doi.org/10.1007/BFb0022247</a> / <a href="https://pauillac.inria.fr/%7Eherbelin/articles/csl-Her94-lambda-bar.ps.gz" rel="nofollow noreferrer">https://pauillac.inria.fr/~herbelin/articles/csl-Her94-lambda-bar.ps.gz</a></li>
<li>Daniel Murfet, William Troiani. 2020. <em>Gentzen-Mints-Zucker duality</em>. <a href="https://arxiv.org/abs/2008.10131" rel="nofollow noreferrer">https://arxiv.org/abs/2008.10131</a></li>
</ul>
<p>Additional references can be found in their bibliography. Some discussion about this correspondence is also found at the end of Chapter 6 in the following textbook:</p>
<ul>
<li>Troelstra and Schwichtenberg. 1996. <em>Basic Proof Theory.</em> <a href="https://doi.org/10.1017/CBO9781139168717" rel="nofollow noreferrer">https://doi.org/10.1017/CBO9781139168717</a></li>
</ul>
</li>
</ol>

CC BY-SA 4.0
2023-11-17T21:44:53.870Z
OK, this is probably stupid, but: if we take a $\lambda$-term, interpret it as a natural deduction proof, convert the latter to a sequent proof, eliminate cuts in the latter, and convert it back to a natural deduction proof and then $\lambda$-term… what goes wrong? From the difference in complexity we can't expect to get a normal form so easily, so what *do* we get?
Gro-Tsen
CC BY-SA 4.0
2023-11-18T14:26:11.420Z
Cut-elimination being stated in terms of proving the same sequent, there is no requirement of preserving any notion of meaning of proofs. For instance, a cut-elimination procedure returning $K_*=\lambda x\lambda yy$ when the input is βη-equivalent to $K=\lambda x\lambda yx$ would be allowed. (The blog post mentions more subtle cut-elimination procedures, which are "local" in a certain sense.)
gadmm
CC BY-SA 4.0
2023-11-17T19:44:42.017Z
2023-11-19T02:06:08.953Z
2023-11-19T02:06:08.953Z
gadmm
<p>What is the precise connection between:</p>
<ul>
<li><p>strong normalization of the simply typed <span class="math-container">$\lambda$</span>-calculus, and</p>
</li>
<li><p>cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent calculus” form?</p>
</li>
</ul>
<p>Does either follow from the other?  Does each follow from the other?  (Do they have the same computational complexity and/or arithmetic strength?)</p>
<p>I can vaguely see that, under the Curry-Howard correspondence, a redex <span class="math-container">$(\lambda (v:\sigma).E)T$</span> will translate to a natural deduction style proof with <span class="math-container">$\rightarrow$</span> introduction immediately followed by <span class="math-container">$\rightarrow$</span> elimination, which becomes a cut proof in sequent calculus, whose immediate elimination should correspond to the reduct <span class="math-container">$E[v := T]$</span>.  So certainly there should be <em>some</em> connection.  The precise details escape me, however, in particular because terms in the s.t.<span class="math-container">$\lambda$</span>.c. correspond to natural deduction proofs whereas cut elimination takes place at the sequent calculus level (there are three things in correspondence: a <span class="math-container">$\lambda$</span>-term, a natural deduction proof and a sequent calculus proof, and I'm not sure what the correct statement at the “natural deduction” level should be that corresponds to the two bullet points at the “<span class="math-container">$\lambda$</span>-calculs” and “sequent calculus” levels).</p>
<p>I'm sure this is very standard: is there a textbook that explains this, hopefully in a pleasant way?</p>

CC BY-SA 4.0
2023-11-16T22:37:41.980Z
Maybe sections 3.4, 3.5 and 3.6 of Proofs and Types (http://www.paultaylor.eu/stable/prot.pdf) can help. It takes place in a slightly broader setting, where there are three kinds of redexes.
sparusaurata
CC BY-SA 4.0
2023-11-17T09:34:11.847Z
Concerning "what the correct statement at the “natural deduction” level should be that corresponds to the two bullet points", the usual keyword is "detour elimination".
Lê Thành Dũng 'Tito' Nguyễn
<lo.logic><lambda-calculus><curry-howard>
Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic
Gro-Tsen
# Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic

(Asked by: username_0 on 2023-11-16)

What is the precise connection between:

* strong normalization of the simply typed $\lambda$-calculus, and
* cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent calculus” form?

Does either follow from the other? Does each follow from the other? (Do they have the same computational complexity and/or arithmetic strength?)

I can vaguely see that, under the Curry-Howard correspondence, a redex $(\lambda (v:\sigma).E)T$ will translate to a natural deduction style proof with $\rightarrow$ introduction immediately followed by $\rightarrow$ elimination, which becomes a cut proof in sequent calculus, whose immediate elimination should correspond to the reduct $E[v := T]$. So certainly there should be *some* connection. The precise details escape me, however, in particular because terms in the s.t.$\lambda$.c. correspond to natural deduction proofs whereas cut elimination takes place at the sequent calculus level (there are three things in correspondence: a $\lambda$-term, a natural deduction proof and a sequent calculus proof, and I'm not sure what the correct statement at the “natural deduction” level should be that corresponds to the two bullet points at the “$\lambda$-calculs” and “sequent calculus” levels).

I'm sure this is very standard: is there a textbook that explains this, hopefully in a pleasant way?

**Tags:** lo.logic, lambda-calculus, curry-howard

> **Comments:**
> **username_1**: Maybe sections 3.4, 3.5 and 3.6 of Proofs and Types (http://www.paultaylor.eu/stable/prot.pdf) can help. It takes place in a slightly broader setting, where there are three kinds of redexes.  
> **username_2**: Concerning "what the correct statement at the “natural deduction” level should be that corresponds to the two bullet points", the usual keyword is "detour elimination".  

---

## 1 answers

### Answer by username_3 on 2023-11-17. Score: 3

1. How “standard” is it? A [post by Anupam Das on the proof theory blog](https://prooftheory.blog/2020/09/07/simple-proofs-of-cut-elimination-ii-intuitionistic-logic/) attacks the folklore by comparing the following two results:

   > Proposition 1 (Folklore). For any theorem A of IPL, we can compute a cut-free LJ proof of A in exponential time and polynomial space in |A|.

   > Theorem 3 (Statman ’79). Deciding whether two simply typed $\lambda$-terms reduce to the same normal form is not elementary recursive.

   He then remarks:

   > [...] Statman’s result does not imply any lower bounds on the complexity of cut-elimination for LJ, since normalisation of $\lambda$-terms constitutes just one particular strategy for cut-elimination. Note in particular, that both Proposition 1 and Theorem 3 are perfectly consistent with each other.
2. Nevertheless, let me mention two works in this direction that help clarify the link. Consistently with the previous remark, they assume a strategy corresponding to the negative polarisation of logic (corresponding to call-by-name reduction in the λ-calculus). But even with this assumption the result is deeper than it looks, relating global transformations (substitution) with local ones (from cut-elimination).

   * Hugo Herbelin. 1994. *A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure*. <https://doi.org/10.1007/BFb0022247> / [https://pauillac.inria.fr/~herbelin/articles/csl-Her94-lambda-bar.ps.gz](https://pauillac.inria.fr/%7Eherbelin/articles/csl-Her94-lambda-bar.ps.gz)
   * Daniel Murfet, William Troiani. 2020. *Gentzen-Mints-Zucker duality*. <https://arxiv.org/abs/2008.10131>

   Additional references can be found in their bibliography. Some discussion about this correspondence is also found at the end of Chapter 6 in the following textbook:

   * Troelstra and Schwichtenberg. 1996. *Basic Proof Theory.* <https://doi.org/10.1017/CBO9781139168717>

> **Comments:**
> **username_0**: OK, this is probably stupid, but: if we take a $\lambda$-term, interpret it as a natural deduction proof, convert the latter to a sequent proof, eliminate cuts in the latter, and convert it back to a natural deduction proof and then $\lambda$-term… what goes wrong? From the difference in complexity we can't expect to get a normal form so easily, so what *do* we get?  
> **username_3**: Cut-elimination being stated in terms of proving the same sequent, there is no requirement of preserving any notion of meaning of proofs. For instance, a cut-elimination procedure returning $K_*=\lambda x\lambda yy$ when the input is βη-equivalent to $K=\lambda x\lambda yx$ would be allowed. (The blog post mentions more subtle cut-elimination procedures, which are "local" in a certain sense.)  

---

