Comments on When is proof of provability a proof?
Parent
When is proof of provability a proof?
I am writing some notes on mathematical logic and I hit upon something I never really understood. I am pretty sure my question is elementary; nevertheless, I would appreciate help clearing my confusion.
We start with a bare-bones metatheory, enough to manipulate and reason about finite strings (I read that a weak fragment of arithmetic is sufficient but I don't know the details). In this setting we can study the syntax of first-order logic (FOL) and, in particular, formulate the ZFC axioms.
Using the language of ZFC, we can again develop the syntax of FOL (now everything is a set underneath rather than primitive symbols) and formulate the ZFC axioms. So ZFC can reason about ZFC. Thus far everything is clear to me.
Questions
Let $\varphi$ be a sentence in the language of ZFC. Suppose that
$$\mathrm{ZFC} \vdash (\mathrm{ZFC} \vdash \varphi).$$In other words, ZFC proves that ZFC proves that $\varphi$ is true. Does it follow that $\mathrm{ZFC} \vdash \varphi$? I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
More generally, if $T$ is a first-order theory and $\psi$ a sentence in the language of $T$, it makes sense to ask whether
$$\mathrm{ZFC} \vdash (T \vdash \psi) \quad\text{ implies }\quad T \vdash \psi.$$Is this stronger statement true? What conditions does ZFC satisfy so that this holds?
Motivation
Suppose one wishes to study a first-order theory $T$. The metatheory is too weak to use standard mathematical techniques. However inside ZFC we have semantics (i.e. models which are sets) and we can prove Gödel's completeness and compactness theorems, and thus all of model theory applies to $T$. But I am left wondering whether results about $T$ derived using these methods translate directly to an honest proof in the weak metatheory.
Post
The following users marked this post as Works for me:
| User | Comment | Date |
|---|---|---|
| Hernán Ibarra Mejia | (no comment) | Apr 24, 2026 at 13:32 |
I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
As Gödel showed, provability is a $\Sigma_1^0$-statement[1]. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements [2]. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
Two tangential notes on this question:
-
Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
-
Nonstandard models of arithmetic provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
0 comment threads