Is lambda calculus a sub-system of first-order logic and set theory?

Question

I have been reading lambda calculus for a while, and I have always had the question: is lambda calculus a subsystem under first-order logic and set theory? For instance, in many textbooks, we assume there exists a set of variables $V$, and if $x \in V$, then $x \in \Lambda$ ($x$ is a lambda term). So it seems that $x$ is not primitive to lambda calculus but is primitive to set theory, and $x$ is a variable (in lambda calculus) if and only if $x \in V$, under the sense of $\in$. Further, to specify Church encoding, inevitably we have to assume that existence of $\mathbb{N}$, the set of natural numbers, which has to be constructed under a first-order system with relations $\in$ and $=$ and axioms like ZFC. The abstraction and application operations in lambda calculus, in my understanding, can be viewed as two function symbols in FOL, e.g., for any $x \in V$ and $M \in \Lambda$, $\left(\lambda x. M\right) \in \Lambda$. So to conclude, it makes me feel that lambda calculus is not a new language, but a sub-system of an existing language.

Answer 1

For theories $T_0$ and $T_1$ over the same language, we say $T_0$ is a subtheory of $T_1$ when every theorem of $T_0$ is also provable in $T_1$. If we require theories are closed under deductions, then it means $T_0\subseteq T_1$. For example, $\mathsf{ZF}$ is a subtheory of $\mathsf{ZFC}$, and $\mathsf{RCA_0}$ is a subtheory of $\mathsf{ACA_0}$.

However, how can we compare theories with different syntaxes? Even in a simple case when both $T_0$ and $T_1$ are theories over the first-order logic does not allow comparing them directly unless $T_0$ and $T_1$ have the same language (that is, the same set of the predicate, function, and constant symbols.) For example, how can we say $\mathsf{PA}$ is a subtheory of $\mathsf{ZFC}$?

In the above case, you may claim that $\mathsf{PA}$ can be "embedded" into $\mathsf{ZFC}$ because we can define the natural number structure over $\mathsf{ZFC}$, and we can show this structure satisfies $\mathsf{PA}$. That is right. However, there are more examples whose "comparison" is less trivial in this manner. For example, how can we "compare" $\mathsf{KP}$ and $\mathsf{ATR_0}$? We cannot compare these two directly by comparing their theorems. Can we extend the notion of being a subtheory to theories with different languages?

Fortunately, there is a known way to compare apples and oranges: interpretations. Informally, an interpretation from $T_0$ to $T_1$ is a way to "simulate" $T_0$ within $T_1$. Its formal definition is a bit tedious, so I recommend a relevant question and answers on this website. (To answer the comparison between $\mathsf{KP}$ and $\mathsf{ATR_0}$, the former can interpret the latter but not vice versa.)

Going back to comparing $\mathsf{PA}$ and $\mathsf{ZFC}$, the standard construction of the set of natural numbers over a set theory gives a way to interpret $\mathsf{PA}$ within $\mathsf{ZFC}$. In this sense, we might think $\mathsf{PA}$ is a subtheory of $\mathsf{ZFC}$.

---

However, interpretability is sometimes very very far from being a subtheory. Let me give some examples:

• Heyting arithmetic $\mathsf{HA}$ is a first-order intuitionistic arithmetic. $\mathsf{HA}$ is obtained from $\mathsf{PA}$ by dropping the law of excluded middle. Clearly, $\mathsf{HA}$ is a subtheory of $\mathsf{PA}$.

  By Gödel-Gentzen double-negation translation, $\mathsf{PA}$ is interpretable within $\mathsf{HA}$. Then can we say $\mathsf{PA}$ is a subtheory of $\mathsf{HA}$?

• Various forcing constructions are also examples. We can view forcing syntactically, and we may view it as a way to interpret some extensions of $\mathsf{ZFC}$ within $\mathsf{ZFC}$.

  As an example, forcing by adding $\aleph_2$ Cohen reals provides a way to interpret $\mathsf{ZFC+\lnot CH}$ within $\mathsf{ZFC}$. On the other hand, collapsing $2^{\aleph_0}$ to $\aleph_1$ without adding reals provides a way to interpret $\mathsf{ZFC+ CH}$ within $\mathsf{ZFC}$. Can we say that both $\mathsf{ZFC+ CH}$ and $\mathsf{ZFC+\lnot CH}$ are subtheories of $\mathsf{ZFC}$?

These examples should illustrate claiming a given theory is a subtheory of another is often unnatural if we only rely on interpretations. In your case, lambda calculus and set theory even have different syntaxes: The rules of lambda calculus form a standalone formal theory that is irrelevant to first-order logic. Thus comparing these two as subtheories would be more elusive, although what Thomas Andrews pointed out shows lambda calculus is interpretable within $\mathsf{ZFC}$.

Answer 2

You are misunderstanding how language is used in mathematical texts. It's clear that "a set of variables" refers to sets in their informal sense that was understood well enough for such purposes centuries before ZFC emerged. Similarly, the claim that the natural numbers can be coded in the λ-calculus requires nothing more than the idea of counting numbers (including zero) as understood by the ancients. That sets and natural numbers could be defined precisely within ZFC and first-order logic does not imply that they presuppose ZFC and first-order logic; rather the opposite is true, that mathematical conceptions including sets, numbers and many more advanced concepts were understood (and used mostly correctly) before they were made precise.

ZFC can model both the syntax and the semantics of the λ-calculus, but nevertheless the λ-calculus is a free-standing formal calculus that is absolutely independent of ZFC or any other specific foundation of mathematics.