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.
-
$\begingroup$ What do you mean by a new language? Does the existence of a semantics, however ad hoc, built using set theory preclude a language from being new? $\endgroup$– Greg NisbetJan 1 at 20:12
-
$\begingroup$ @GregNisbet "new language" means a separate set of symbols with a separate set of rules, syntactically. $\endgroup$– Ziqi FanJan 1 at 20:16
-
3$\begingroup$ Scott, etal., proved that, in set theory, there is a set $X$ and a function $X\to X^X$ which models lambda calculus. It's hard to be sure, however, if that means lambda calculus is a subset of set theory, because lambda calculus could have other models in other theories. It is best to treat lambda calculus as its own thing. $\endgroup$– Thomas AndrewsJan 1 at 20:57
-
1$\begingroup$ It sounds like your concern is with the use of set-theoretic terminology and notation to describe lambda calculus, but these are just tools to help make the description precise. Would anything be gained by avoiding this and trying to use "purely natural language"? $\endgroup$– KarlJan 1 at 21:14
2 Answers
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}$.
-
2$\begingroup$ There is another issue in your question that you conflate an object language and a metalanguage, as Karl commented. You referred to the set of variables, but it is a notion over a metatheory (here, set theory) and not a notion formalizable over an object theory (here, lambda calculus.) $\endgroup$ Jan 1 at 21:45
-
$\begingroup$ Then I guess more precisely, I am trying to "interpret" lambda calculus using FOL/set theory, and in this case, lambda calculus constitute the semantics of FOL (just like Tarski's world)? $\endgroup$– Ziqi FanJan 1 at 23:00
-
$\begingroup$ @ZiqiFan I do not fully understand what you precisely tried, so I could answer what you said under more clarification. However, my impression tells what you did is defining the syntax lambda calculus over $\mathsf{ZFC}$, and if my impression is correct, it says nothing about interpretability. $\endgroup$ Jan 2 at 3:48
-
$\begingroup$ To repeat, as Thomas Andrews mentioned, Dana Scott constructed a model of untyped lambda calculus using domain theory, and this is a way how to interpret lambda calculus over a set theory (say, $\mathsf{ZFC}$.) $\endgroup$ Jan 2 at 3:49
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.