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.

  • 1
    $\begingroup$ Have you heard of system T? $\endgroup$
    – Trebor
    Commented Sep 12, 2022 at 3:11
  • $\begingroup$ I believe things become problematic when you start quantifying over propositions $\endgroup$
    – Couchy
    Commented Sep 12, 2022 at 4:21
  • $\begingroup$ @Trebor so STLC plus booleans and primitive recursive arithmetic right? I know there has to be stuff investigating its strength but I'm not familiar with the details $\endgroup$ Commented Sep 12, 2022 at 18:58
  • 1
    $\begingroup$ It is not clear what your formalism is, and the answer depends on that. You say it is first-order logic. Is it multi-sorted? What are the sorts, does "STLC" indicate you're implementing STLC with first-order logic on top? Is there a sort of truth values? Your examples indicate that you can define $\{f(z) \mid z \in x\}$, so perhaps you're in set theory (in which case the question is moot anyhow). $\endgroup$ Commented Sep 13, 2022 at 14:04
  • 1
    $\begingroup$ Naive, possibly massively open-ended question: Why is first order logic impractical? $\endgroup$
    – user1168
    Commented Sep 16, 2022 at 9:47

2 Answers 2


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}$.

  • $\begingroup$ I'm trying to follow along here; is there a concise reference (for an interested newbie) for the shorthand being used (STLC, HA, AC...), or is the best reference an Internet search? Thanks! $\endgroup$
    – user1168
    Commented Sep 14, 2022 at 16:20
  • 3
    $\begingroup$ @DanielMGessel Simply Typed Lambda Calculus, (higher order) Heyting Arithmetic, Axiom of Choice, Direct Choice, and (second/higher order) Peano Arithmetic $\endgroup$
    – Couchy
    Commented Sep 14, 2022 at 18:06
  • $\begingroup$ This is really interesting but gets into model theory beyond me. It seems fragile. I'm not sure how this might extend if I play with say linear logic or modal logic. $\endgroup$ Commented Sep 18, 2022 at 1:45

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).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.