The Curry-Howard isomorphism tells us that propositional logic and lambda calculus are isomorphic, meaning that there is a correspondence:
We call Type assignment the action of giving a type to a term, meanwhile Type Inhabitation the action of finding a term with a certain type.
If you find a term with that type, meaning you perform type inhabitation, then the corresponding formulae of first order logic is a theorem (tautology).
Remember that not all terms can be given a simple type, in the context of simple-typed lambda calculus. An example of un-typable term is , and self-applications in general.
Every typable term is strongly normalizing, meaning that every normalizing strategy can reduce the term into a normal form. Note that weakly normalizing means that it exists at least a strategy that reduces the term into a normal form.
A term composed of only linear terms is always strongly normalizing. This is because a linear term can never be applied to itself, so it can never get stuck in an infinite loop.
In contrast, a term that contains non-linear terms can potentially be weakly normalizing. This is because a non-linear term can be applied to itself, which can create an infinite loop.
For example, the term (λx. x) x is weakly normalizing because it can be applied to itself infinitely many times. However, the term (λx. x y) is strongly normalizing because it can never be applied to itself.
In general, a term is strongly normalizing if and only if it does not contain any non-linear terms.
tags: lambda-calculus