Does quantification over functions (STLC) increase strength beyond first order logic?

Question

Does quantification over functions (STLC) increase strength beyond first order logic?

I want to add support for binders in my little constructive first order logic formalism I'm working on but I'm worried allowing functions might make things too powerful.

I want to be able to do stuff like axiomize a more constructive version of the image of a set

$$ \forall x f y. y \in \{ f(z) \mid z \in x \} \iff \exists z. z \in x \wedge y = f(z) $$

Or axiomize folding over Peano arithmetic

$$ \forall x f. \mu(x, f, \text{O}) = x$$ $$ \forall x f y. \mu(x, f, \text{S}(y)) = f(\mu(x, f, y))$$

I'm not sure how I want to handle extensionality.

Just assume for now

$$ (x\colon \Box) \cong y \iff x = y $$ $$ (f\colon \tau_1 \rightarrow \tau_2) \cong g \iff \forall x. f(x) \cong g(x) $$

Now clearly it's possible to encode quantification over functions in second order logic in a non constructive way using total functional relations.

But I'm not sure what it means to encode predicates in terms of the image of a function (defined in terms of the STLC.)

I'm not sure what happens if you add an axiom schema for the principle of unique choice either.

$$ (\forall x. \exists! y. P(x, y)) \rightarrow \exists! f\colon \tau_1 \rightarrow \tau_2. \forall x. P(x, f(x))$$

I have heard there are nice systems in between first order logic and second order logic such as monadic second order logic. Maybe a system like monadic second order logic wouldn't be too bad.

Answer 1

The answer depends on the logic considered.

Goodman's theorem states that $\mathsf{HA}^\omega+\mathsf{AC}+\mathsf{DC}$ is conservative over $\mathsf{HA}$. In particular, adding higher-order functions is innocuous.

With classical logic and $\mathsf{AC}$ this is not true anymore, because you can now encode arbitrary second-order predicates as functions. Notably you can embed $\mathsf{PA}_2$ inside $\mathsf{PA}^\omega+\mathsf{AC}$, and the former is much stronger than $\mathsf{PA}$.

Answer 2

Quantifying over predicates introduces impredicativity, which significantly increases the strength of the logic.

If you only allow quantification over non predicates, I believe you are still in the first order domain because you can interpret the function type set-theoretically as the set of terms of that function type. This is no longer true once you quantify over propositions, because you cannot model an impredicative type by the set of its terms (as observed by Reynolds).