# Simple Lambda Calculus Question

For any 2 strongly normalizing terms in the simply typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong normalization and the typable lambda calculus, but I have not been able to show that this is the case. Any help would be much appreciated.

• In the untyped λ-calculus, this is is of course not the case. The self-application term λx.xx is SN but applied to itself this gives the canonical non-terminating term. But given what you write, I wonder whether you ask about this property for the simply typed λ-calculus? It has the property but this is not how the proof of SN for it proceeds. Could you clarify? Commented Jan 5, 2023 at 14:11
• Yes actually, that is correct - for typable Lambda Calculus terms, how do you prove application preserves the strongly normalizing property? Commented Jan 5, 2023 at 15:45
• Proving that application preserves SN is the hard part. Given the exact correspondence between type theories and logics know as Curry-Howard correspondence, this must be hard by Gödel's 2nd incompleteness theorem. The standard technique used in SN proofs is called reducibility candidates. Maybe people.mpi-sws.org/~dg/teaching/pt2012/gallier.pdf is a place to look? Commented Jan 5, 2023 at 18:56
• – D.W.
Commented Jan 5, 2023 at 22:01
• Oh hey I wrote something on this almost 8 years ago! mathoverflow.net/a/206529/36103
– cody
Commented Jan 23, 2023 at 18:19