Simply type lambda calculus and simple type theory are not equivalent. The former only has rules for alpha- and beta-reduction, the latter also has rules for Modus Ponens, extensionality and the Introduction of the quantification constant $\Pi$. The normalization results for lambda calculus only refer to rewriting modulo alpha- and beta reduction (there are also variants including eta, an extensionality rule for lambda terms). I will give a common set of rules below (following: Benzmüller, Miller: Automation of Higher-order Logic).
What is a little confusing is that lambda calculus can encode proofs in simple type theory. This is usually done via the Curry-Howard isomorphism but Farmer uses a different encoding. In both cases, we can verify a proof term by normalization but we can not find these terms by reduction.
Simply typed LC (Church style)
The types $o$ and $\iota$ are basic types. Every basic type is a (complex) type. Let $\tau_1, \tau_2$ be (complex) types, then the type application $\tau_1 \rightarrow \tau_2$ is a complex type.
Terms are inductively defined:
- A variable $x$ of type $\tau$ is a term of type $\tau$
- Let $s$ be a term of type $\tau_1 \rightarrow \tau_2$ and $t$ be a term of type $\tau_1$. Then the application $s t$ is a term of type $\tau_2$
- Let $x$ be variable of type $\tau_1$ and $t$ be a term of type $\tau_2$, then $\lambda x.t$ is a term of type $\tau_1 \rightarrow \tau_2$.
We define the following inferences on lambda terms:
- $\alpha$-equivalence: $(\lambda x.t[x]) = (\lambda y.t[y])$ when $x,y$ do not appear in t otherwise.
- $\beta$-equivalence: $(\lambda x.s[x])t = s[t]$ when $x$ does not appear in $t$. Rewriting the equation left to right is called a $\beta$-reduction; rewriting right to left is called $\beta$-expansion.
Remark: I made the containment requirements stricter than necessary to simplify the presentation. The main issue to overbinding, iotw. that $(\lambda x \lambda y.f x y) y$ $\beta$-reduces to $\lambda z.f y z$ but not to $\lambda y. f y y$.
The decidability result you mentioned is that continued $\beta$-reduction of a term modulo $\alpha$-equivalence terminates and results in a normal form. There is also an upper bound ($O(2\uparrow\uparrow$n) to the growth in size during this process such that we cannot express any function that grows faster than that.
Elementary type theory: We assume the existence of variables for the logical connectives ($¬,∨,\Pi)$ of types $o\rightarrow o$, $o\rightarrow o \rightarrow o$ and $(\alpha \rightarrow o) \rightarrow o$. The connectives $\land,⊃$ can be derived the same way as in FOL. $\Pi$ represents universal quantification; $\forall x.f$ is defined as $\Pi \lambda x.f$ and $\exists x.f = \neg \forall x.\neg f$.
We also add the following inference rules to typed LC:
- Substitution: given the term $f x$ where $x$ is not free (*), infer the term $f a$ (under the condition that $x$ and $a$ have the same type)
- Modus Ponens: from $f$ and $f ⊃ g$ infer $g$
- Generalization: from $f x$ infer $\Pi f$ if $x$ is not free in $f$
We also assume some Hilbert-style axioms describing the logical connectives.
Simple type theory: We add even more axioms to elementary type theory: extensionality, Leibniz equality, number theory, description and choice.
It should be intuitive that applying inferences cannot terminate even for elementary type theory: after all, it allows to derive logical consequences for which $\beta$-reduction is not sufficient. LC is still a quite expressive language which even allows to encode proofs - it's just not strong enough to express the proof search.
Remark: the logical connectives can be defined in multiple ways, e.g. Andrews builds up the whole theory based on an equality predicate.
(*) a variable $x$ is bound in a term if it occurs inside an abstraction $\lambda x.t$ over $x$. All occurrences of a variable that are not bound are free occurrences.