Timeline for What is the connection between these proofs of strong normalization in $\lambda^\to$ and LK?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 24, 2021 at 5:58 | comment | added | Noam Zeilberger | as an aside, it is perhaps worth mentioning that Gentzen also gave a direct proof of normalization for first-order intuitionistic natural deduction. Surprisingly, Gentzen's manuscript was only discovered relatively recently by von Plato, who discusses it in this 2008 article: jstor.org/stable/pdf/20059973.pdf | |
| Jun 22, 2021 at 20:27 | comment | added | Noam Zeilberger | I think Loader is just referring loosely to Gentzen's proof of cut-elimination, for which arguably the "main technique" is a nested induction on formulas and derivations. Gentzen actually proved cut-elimination for both LK and LJ in one go: he gave a cut-elimination procedure for LK, then observed that it preserves the property of being an LJ-derivation (i.e., having at most one formula on the RHS of every sequent). | |
| Jun 22, 2021 at 18:37 | comment | added | Mike Shulman | That's a curious comment, since in general I would expect SN of STLC to be most closely connected to cut-elimination for intuitionistic sequent calculus. | |
| Jun 22, 2021 at 14:00 | history | asked | Trebor | CC BY-SA 4.0 |