The simply-typed $\lambda$-calculus has:
- product types $A \times B$, with corresponding term formers (pairing and projections)
- function types $A \to B$, with corresponding term formers (abstraction and application)
- equations governing the term formers and subtitution
The simply-typed $\lambda$-calculus does not postulate the existence of any types (sometimes we postulate the unit type $1$, and often we postulate the existe of a type, but without any assumptions about it). We typically work with schemata, i.e., we use meta-level symbols for types. This is akin to using propositional symbols in the propositional calculus.
Simple type theory is simply-typed $\lambda$-calculus and additionally at least:
- the type of truth values $o$, with the corresponding term formers (constants $\bot$ and $\top$, connectives, quantifiers at every type)
- the type of natural numbers $\iota$, with the corresponding term formers (zero, succcesor, primitive recursion into arbitrary types)
- equations governing the term formers and substitution
There are several variations:
- we may postulate excluded middle for truth values
- we may include a definite description operator
- we may include the axiom of choice
- we may vary the extensionality principles
We quickly obtain a formal system that expresses Heyting (or Peano) arithmetic and more, which suffices for incompleteness phenomena to kick in.
What I think is confusing you is the fact that there are two ways to relate logic to type theory:
The Curry-Howard correspondence relates the propositional calculus to the simply-typed $\lambda$-calculus by an interpreation of propositional formulas as types.
Higher-order logic embeds into simple type theory by an interpretation of logical formulas as terms of the type $o$ of truth values.
There is a difference of levels, which makes all the difference. To illustrate, consider the propositional formula $p \land q \Rightarrow (r \Rightarrow p \land r)$. In the simply typed $\lambda$-calculus it is interpreted as the type $P \times Q \to (R \to P \times R)$, whereas in simple type theory it is interpreted as the term $p \land q \Rightarrow (r \Rightarrow p \land r)$ of type $o$, i.e., it is a particular term parameterized by variables $p, q, r$. A higher-order formula, such as $(\forall r : \mathsf{Prop} . r \Rightarrow p) \Rightarrow p$ cannot be encoded in the simply-typed $\lambda$-calculus, whereas in the simple type theory it is again just a term of type $o$ (just replace the sort of propositions $\mathsf{Prop}$ with the type $o$).
Also note that the pure simply-typed $\lambda$-calculus does not postulate the natural numbers. If we add the natural numbers to the simply-typed $\lambda$-calculus we get a fragment of simple type theory known as Gödel's System T (or a version of it, depending on minutiae of how equality is treated), which suffers from – or enjoys, depending on your point of view – the incompleteness phenomena already.