I ran into this question while reading Enderton and Mendelson. Both books pause to introduce enough set theory to define the alphabet, formulas, assignments, and the rest of the machinery of first order logic.
That stopped me. ZFC is itself a theory written in first order logic. The construction seemed to run in both directions: sets were being used to build FOL, while FOL was being used to build set theory.
The usual answer is short: distinguish the object theory from the metatheory. The distinction is correct, but it did not settle the question I was actually asking. This note follows the question one step further, down to the background reasoning that lets any formal system get started.
The apparent circularity
Put the two claims next to each other.
- To define FOL, the book uses sets. It talks about the set of symbols, about functions from variables to terms, about countable languages.
- To define ZFC, the book uses FOL. The axioms are sentences in a formal language.
Read both bullets as foundational dependencies and a circle appears immediately: neither side can be written down first.
Object theory and metatheory
The first move is to separate the two levels.
FOL is described in a metalanguage. From outside the formal system, we talk about finite strings of symbols, recursive definitions, and finite derivations. Only after that machinery is in place do we write ZFC as an object theory inside FOL. The sets mentioned in the syntax chapter belong to the mathematical background in which the formal language is being described; they are not sets whose existence has already been proved from the axioms of ZFC.
Kunen makes this split explicit in Set Theory §I.3. He distinguishes the formal theory from the metatheory and says that, for the elementary syntactic and relative-consistency arguments under discussion, finitistic reasoning provides the intended metatheoretic background. This should not be read as a claim that unrestricted model-theoretic semantics uses only finite objects.
If the distinction still feels like a verbal maneuver, Jacob Neumann's Things to Take With You: 80-310/610 Formal Logic, Fall 2020 is worth reading at this point. He begins with recursive syntax, shows why structural induction follows the shape of that syntax, and then asks the same question directly: if is explained using the English word "and", have we defined anything or merely changed notation? The answer is that "and" belongs to the metalanguage doing the explaining, while belongs to the object language being explained. The later sections put the distinction to work in deduction, soundness, completeness, proof checking, and the Henkin construction.
That resolves how the two levels interact. It still leaves a lower question unanswered: what lets us reason in the metalanguage in the first place?
The answer I still did not believe
The object-theory/metatheory distinction was not my objection. The sentence that often came next was.
Most books say that the set theory used in the metatheory is informal rather than ZFC, so there is no circle. But what is "informal set theory" supposed to mean here? Logic textbooks use countability, cardinal arithmetic, and, for sufficiently general forms of completeness, choice principles. Those are genuine mathematical commitments. Calling them informal does not make them disappear.
The standard answer therefore seemed to move my question back one step and stop. I wanted to know what was actually left at the bottom.
What is left at the bottom?
The useful next step was to identify what the background reasoning actually needs.
To begin formal syntax, you do not need the full set-theoretic apparatus used later in a textbook. You need finite strings and rules for manipulating them.
For an effectively specified language, a formula is a finite string of symbols whose grammar can be checked mechanically. A formal proof is a finite list or tree of formulas. Proof checking is a finite procedure when the axioms and rule instances are decidable, or when axiom instances carry suitable checkable certificates. An arbitrary theory need not have such an effective presentation. At this level we are not appealing to another formal theory underneath the first one. We are carrying out ordinary finitary reasoning about concrete expressions.
Kunen calls this background activity the metatheory. In his 2011 book he explains why he deliberately leaves it unanalyzed:
Our finitistic reasoning in the metatheory is never analyzed formally. In fact, it cannot be, since you could not understand the formal analysis if you did not already understand some basic finitistic reasoning.
"Kunen's informal metatheory" is therefore not the name of a hidden formal system. It is his label for a background competence that he chooses not to axiomatize. Other authors draw the boundary differently, but the general idea is the same: before we can study a formal system, we must already know how to read finite expressions and follow explicit rules.
Describing the background as finitary work on expressions helped me understand the distinction. Concrete examples make its scope clearer.
What finitary reasoning looks like
Here are four examples, mostly Kunen's own.
- Read a string of symbols and say whether it is a formula. Kunen puts it as: the set of formulas of predicate calculus is recursive, because we may program a computer to read a string of symbols and tell us whether or not that string is a formula.
- Read a finite list of formulas and check that each line follows from earlier lines by a rule. That is checking a proof.
- Recognize when a given sentence is an axiom of ZFC. There are infinitely many, but they come from finitely many schemes, so the check is finite.
- Take an inconsistency in and turn it, by an explicit procedure, into an inconsistency in . That is what says, and it is the example Kunen gives of a result in the metatheory.
Each task is carried out on a particular finite string or derivation, even when the theory being discussed has infinitely many theorems or axiom instances.
Kunen makes the stopping point unusually visible in §I.14. He says that a formula is a finite sequence of symbols, asks what a symbol is, and then explicitly sidesteps the question. He lets be the number 1, "whatever that is". The formal definitions stop because the reader's ability to distinguish and manipulate marks has already begun.
These examples answer the question one operation at a time. The diagram below shows how the same answer reorganizes the apparent circle as a dependency chain.
The dependency chain
Read the arrows from top to bottom. ZFC appears well down the picture, as one formal theory among others. The syntax and proof rules above it can be described without first assuming ZFC as an object theory.
The second row contains systems that can be presented directly by rules on finite syntax. Propositional logic is one; FOL extends it with quantifiers and predicates. Type theory is another, which is why Lean need not sit on top of set theory. A logic-free presentation of PRA is a third.
PRA appears twice on purpose. Presented as an equational calculus, it can be specified directly and belongs in the second row. Presented in the usual way as a first order theory, it belongs under FOL beside PA and ZFC. The equational and first-order presentations express the same primitive-recursive arithmetic at the level of the corresponding quantifier-free consequences, although the first-order language can state additional quantified sentences. The difference matters when PRA is proposed as a metatheory, so I return to it below.
Statements about these systems do not add another automatic row. Consistency, incompleteness, and relative strength are metatheoretic claims: they may be argued in the informal background or formalized in a weak theory such as PRA. Once the kind of dependence is kept explicit, the picture is a chain rather than a circle.
Reading the diagram
The arrows show formal or presentational dependence, not historical influence and not a claim that one foundation is uniquely correct. Taking the boxes from top to bottom:
Propositional logic leads to FOL. It supplies the connectives without quantifiers. Both textbooks begin there: Enderton calls it sentential logic, Mendelson calls it the propositional calculus, and both introduce quantification only afterward.
FOL provides the language for first order theories. PA, the usual presentation of PRA, ZFC, and many other theories are obtained by choosing a signature and axioms within that logical framework.
PRA is a leaf in both presentations. It is not shown as the foundation of an ordinary mathematical subject. Its role here is different: it can serve as a formal stand-in for a substantial part of the finitary metatheory, allowing relative consistency and standard incompleteness arguments to be carried out inside a precise system.
PA is also drawn as a leaf. That is a choice of scope for this diagram, not a claim that arithmetic cannot support other mathematics. PA can encode syntax and serve as a formal background for substantial arithmetic reasoning.
ZFC supports the familiar set-theoretic development of ordinary mathematics. Analysis, algebra, topology, and the rest can be reconstructed within it. That downstream role is what makes ZFC a foundation in this diagram.
Type theory offers another route to ordinary mathematics. It reaches the same bottom box by a different foundational branch, rather than passing through ZFC.
Second order logic is omitted deliberately. Its syntax could be placed near FOL, but its standard semantics brings substantial set-theoretic structure with it. Adding it would complicate the picture without changing the answer to the original circularity question.
What do proof checkers rest on?
The top box can still feel philosophical until we look at a proof checker. A running checker has to cross the same boundary between background activity and formal system in completely explicit steps.
Lean checks proofs. Somewhere at the bottom it must decide whether an expression is well formed and whether a term has the claimed type. "Informal set theory" is not an executable specification, so what does the machine actually do?
It works on finite data. Lean's kernel takes a term, checks it against a type, and accepts or rejects it by an algorithm. Lean's object theory is a powerful dependent type theory, represented in the second row of the diagram. But the strength of the propositions that can be expressed in that theory should not be confused with the algorithm that checks a particular proof term. The algorithm's finite implementation does not make the underlying type theory weak. Acceptance is relative to the declared axioms and the trusted implementation; Lean does not establish that every user-added axiom is consistent. See its kernel overview and axiom documentation.
Metamath provides another example. A Metamath database supplies symbol strings and substitution rules; the verifier checks rule applications, the required hypotheses, substitutions, and disjoint-variable conditions. These requirements are specified in the Metamath manual. No particular logic is built into the verifier. The main database, set.mm, declares classical FOL and then ZFC, so the mathematics developed there follows the left branch of the diagram. Those foundational choices live in the database, not in the small program that checks it.
A proof checker is therefore a mechanical version of part of the top box. It does not eliminate the background layer; it turns a carefully isolated piece of that layer into an algorithm we can run.
Is PRA built on FOL?
Once the top box looks algorithmic, it is tempting to replace it with a formal theory. PRA is a common candidate. My first reaction was that this merely moved the circle, because PRA is usually presented as a first order theory.
Two things are true. PRA is commonly presented as a first order theory with quantifier-free induction, and that presentation does use FOL. But PRA also has a logic-free presentation with no connectives and no quantifiers. Its sentences are equations between terms built from primitive recursive functions, and its rules operate by substitution and induction on equations. Logic-free formulations were developed by Curry in 1941 and Goodstein in 1954; this is not a claim that primitive recursive arithmetic itself began in 1941. In that presentation PRA need not presuppose FOL, which is why it also appears in the second row of the diagram.
PRA still does not replace the top box. To understand its terms, equations, and rules, we must already be able to recognize finite expressions and valid applications of a rule. That is the same prior competence again. Kunen puts the point directly in his 2011 book: PRA approximates finitistic reasoning; it does not make that reasoning unnecessary.
Why is there no canonical metatheory?
If PRA can formalize so much of the metatheory, why not choose some system of that kind and declare it the canonical bottom layer? I wanted exactly that answer. The difficulty is that writing down the system cannot replace the competence needed to read what has been written.
- It is elementary enough that ordinary practice does not need a fixed axiomatization of it.
- Formalizing it recreates the problem. To read the axioms and rules of your proposed canonical metatheory, you already have to recognize finite strings and rule applications.
- People disagree on where finitary stops. Tait puts it at PRA. Parsons argues for less. Kreisel argued for more. Kunen says outright that the notion of finitistic is not rigorously defined.
The first point explains why textbooks rarely dwell on the issue. The second explains why no additional formalization can end the regress by itself.
One question was really three
The answers seemed to disagree because I had been treating three questions as one.
- How is FOL defined? By giving recursive rules for its finite syntax, a deductive calculus, and a semantics in a metalanguage.
- Where are theorems about FOL proved? In a metatheory whose strength depends on the theorem. Elementary syntax needs very little; general model theory may use substantial set theory; much proof-theoretic reasoning can be formalized in weak arithmetic such as PRA.
- What must a reader already be able to do before any of those formalizations make sense? Recognize finite expressions, follow definitions, and check explicit rule applications.
The object-language/metalanguage distinction answers the first question. Choosing PRA, ZFC, or another formal background addresses the second. The third is where the chain stops, because any proposed formal answer to it would have to be read and understood using the very competence it was meant to replace.
There is still a philosophical edge here. Recognizing a finite string already seems to involve some grasp of finite collections, so I would not claim that logic is cleanly prior to every notion of collection. But that does not restore the original circle. The starting point is not ZFC secretly proving the syntax of FOL. It is a modest practice of reading and manipulating finite expressions, after which FOL, ZFC, type theory, and their relationships can become objects of precise mathematical study.
Sources
- Kenneth Kunen, Set Theory: An Introduction to Independence Proofs, 1980. §I.3 for the formal theory and metatheory split, §I.14 for coding syntax and for sidestepping what a symbol is.
- Kenneth Kunen, Set Theory, 2011, for the passage on the metatheory never being analyzed formally and for PRA being only an approximation to it. Neither appears in the 1980 edition.
- Haskell Curry, A formalization of recursive arithmetic, 1941, for a logic-free formulation of recursive arithmetic.
- R. L. Goodstein, Logic-free formalisations of recursive arithmetic, 1954, for the refinement.
- William Tait, Finitism, 1981, for the thesis that finitism is PRA.
- Herbert Enderton, A Mathematical Introduction to Logic, and Elliott Mendelson, Introduction to Mathematical Logic, for the textbooks the question came from.
- Jacob Neumann, Things to Take With You: 80-310/610 Formal Logic, Fall 2020, for a concise account of recursive syntax, structural induction, the object-language/metalanguage distinction, soundness and completeness, and the Henkin construction.