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:

1. The Curry-Howard correspondence relates the propositional calculus to the simply-typed $\lambda$-calculus by an interpreation of propositional formulas as  *types*.

2. 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).$$
To prove the formula amounts to giving a term of the type.
In constrast, in simple type theory it is interpreted as the *term*
$$p : o, q : o, r : o \vdash p \land q \Rightarrow (r \Rightarrow p \land r) : o,$$
Now proving the formula amounts to proving the equation $p \land q \Rightarrow (r \Rightarrow p \land r) = \top$ in the simple type theory.

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.