What the Metalanguage for First-Order Logic Assumes

When we prove things about first-order logic — define structures and satisfaction, prove soundness, completeness, compactness — we work in a metatheory. A natural question (sharpened in Set Theory and First-Order Logic and The Metalanguage Hierarchy) is: what does that metatheory actually have to assume? The loose slogan "the metatheory is ZFC" badly over-states it. This remark gives the precise ledger, calibrated by reverse mathematics, and records two subtleties that are routinely misremembered: the role of the axiom of choice, and the (non-)role of $\mathrm{Con}(\mathrm{ZFC})$.

Two separate commitments

"Doing FOL in the metalanguage" bundles two distinct things that should be kept apart.

1. A meta-logic — the reasoning apparatus you argue with. This is itself logic, normally classical first-order logic, usually deployed informally. So first-order logic appears in the metalanguage too: you reason with logic in order to reason about the object logic. The meta-logic need not match the object logic — one can study classical logic through a constructive metalogic (constructive reverse mathematics) or study a nonclassical object logic classically.
2. A meta-mathematics — the background set theory or arithmetic that supplies domains, interpretations, satisfaction, and the inductions used in proofs. How much of this is needed is the substantive question, and the answer is: only as much as the particular theorem requires.

The reverse-mathematics ledger

Calibrating commitment (2) theorem-by-theorem:

Two precise equivalences underpin the table:

• Over the base system ${\mathrm{RCA}}_0$, completeness for countable theories is equivalent to WKL₀ — a weak fragment of second-order arithmetic, with no choice.
• Over ZF, completeness $\equiv$ compactness $\equiv$ BPI (the Boolean prime ideal / ultrafilter lemma).

The choice subtlety: BPI, not full AC

It is often half-remembered that "completeness of FOL needs the axiom of choice." The precise position:

• Soundness needs no choice — it is a plain induction on derivations.
• Countable completeness needs no choice. Gödel's original 1929 theorem was for countable languages; the only choice-looking step, Lindenbaum's lemma (extend a consistent set to a maximal consistent one), is carried out by explicitly enumerating the countably many formulas and deciding them one at a time.
• Uncountable completeness needs weak choice. With no enumeration to lean on, Lindenbaum's lemma needs Zorn/AC-style strength. The sharp result is the equivalence

$$\text{completeness (arbitrary language)}{\equiv }_{\mathrm{ZF}}\text{compactness}{\equiv }_{\mathrm{ZF}}\text{BPI}.$$

Crucially, BPI is strictly weaker than full AC:

$$\text{full AC}⟹\text{BPI}⟹\text{(ultrafilters exist, compactness, …)},$$

and neither arrow reverses — there are models of ZF satisfying BPI where full AC fails. BPI is nonetheless independent of ZF (unprovable there), so the general completeness theorem genuinely needs something beyond ZF — just a weak choice fragment, not the whole of AC. (The compactness ⟺ BPI framing is due to Henkin and Łoś–Ryll-Nardzewski.)

$\mathrm{Con}(\mathrm{ZFC})$ is not assumed

The metatheory of FOL does not assume the consistency of its own ambient theory.

• Model theory of arbitrary first-order theories needs only WKL₀ / ZF + BPI — never $\mathrm{Con}(\mathrm{ZFC})$.
• $\mathrm{Con}(\mathrm{ZFC})$ enters in exactly one place: when the object theory is ZFC itself and one wants the specific claim "ZFC has a model." By completeness, "ZFC has a model" $⟺\mathrm{Con}(\mathrm{ZFC})$, and that requires a strictly stronger metatheory (e.g. ZFC + an inaccessible), as the German-analysing-English discussion explains.

A final distinction worth stating crisply: using a theory is not the same as adding its consistency as an axiom. Even when one does loosely take "the metatheory = ZFC," one is assuming ZFC, not ZFC + $\mathrm{Con}(\mathrm{ZFC})$. The consistency statement is an additional, strictly stronger commitment that the lower levels cannot supply for themselves (Gödel's second incompleteness theorem).

Take-aways

• The metalanguage for FOL assumes (i) a meta-logic — itself (classical) first-order logic, used informally — and (ii) just enough meta-mathematics for the theorem at hand, calibrated by reverse mathematics.
• Soundness is choice-free and cheap; countable completeness is choice-free (= WKL₀); uncountable completeness/compactness is equivalent to BPI, a weak choice fragment strictly below full AC and independent of ZF.
• $\mathrm{Con}(\mathrm{ZFC})$ is not a general assumption — it is forced only by the specific semantic claim that the object theory ZFC itself has a model.

Related discussions: Set Theory and First-Order Logic (object/metatheory and foundational ordering), The Metalanguage Hierarchy and Semantics in Mathematics (the tower of levels and the German/English analogy), and What Justifies Con(ZFC)? (the one assumption that is strictly stronger).