I am trying to understand why $\forall n \in \mathbb{N} \vdash P(n)$ doesn't imply $\forall n \in \mathbb{N}P(n)$ by studying the concepts in this answer, and had 2 questions about the difference between $\forall n \in \mathbb{N} \vdash P(n)$ and $\forall n \in \mathbb{N}P(n)$:

  1. Why does $\forall n \in \mathbb{N} \vdash P(n)$ only make sense in the metatheory? I don't understand why the object theory is not capable of talking about whether or not $P(n)$ can be proven given any explicit $n$, especially because the linked answer says that $\vdash \forall n \in \mathbb{N} P(n)$ is a statement made within the object theory. Semantically, why does the quantification in $\forall n \in \mathbb{N} \vdash P(n)$ happen outside of the theory, but the quantification for $\vdash \forall n \in \mathbb{N} P(n)$ happens inside of the theory?
  2. Why is the model of the naturals referred to by a statement in the metatheory not necessarily the same as the model of the naturals referred to by a statement in the theory? In this case, both of the statements referring to $\mathbb{N}$, and I thought that $\mathbb{N}$ is a specific model of the naturals, namely $0,1,2,\ldots$; so because we are referring to this set both times, it seems that we are referring to the same model of the naturals regardless of whether we are outside or inside the theory.

For additional context, I am trying to understand why $\forall n \in \mathbb{N} \vdash P(n)$ doesn't imply $\forall n \in \mathbb{N}P(n)$ in order to better understand answers to my question here.

  • $\begingroup$ If the "object theory" were talking about whether or not P(n) could be proven for various n, then it would be acting as a metatheory. $\endgroup$ Commented Jun 22 at 22:17
  • $\begingroup$ @spaceisdarkgreen why can we talk about $\vdash \forall n P(n)$ though without operating as a metatheory? $\endgroup$ Commented Jun 22 at 22:18
  • 3
    $\begingroup$ $\vdash \forall n P(n)$ is a statement in the metatheory. $\forall n P(n)$ is a statement in the object theory. $\endgroup$ Commented Jun 22 at 22:19
  • 5
    $\begingroup$ I think the notation is obscuring something important here. This "quantifying in the metatheory" only makes sense because for each natural number, there is a corresponding term (written SSSSSS0, or whatever). Let $\mathbf n$ be the term in the object language standing for $n$. What we're differentiating between is "for each $n\in \mathbb N,$ $\vdash P(\mathbf n)$" and "$\vdash \forall n P(n).$" $\endgroup$ Commented Jun 22 at 22:25
  • $\begingroup$ Perhaps this is easier in Peano Arithmetic $\mathbf{PA}$. Even if it is ω-consistent, it can be extended using the negation of Godel's sentence. The resulting system is no longer ω-consistent. Even though there are no easy models, one can think of them as having all natural numbers and some infinite numbers that are not numerals. Intuitively one cannot discard the existence of these infinite numbers, and so one cannot insert the quantifiers into the theory. $\endgroup$
    – Keplerto
    Commented Jun 22 at 22:29

2 Answers 2


One way of explaining this could be in terms of non-standard models, as in Lumsdaine's comment, which goes as follows:

"if Con(PA) fails in a non-standard model, it means it contains a “proof of non-standard length” of a contradiction from PA. With a little work, one can externalise that to some non-well-founded “proof tree”, which has at each node a possibly-non-standard formula (which in turn externalises to some not-necessarily-well-founded syntax tree), where each step will genuinely follow from earlier steps by some standard rule of proof, but the whole tree will be non-well-founded, and hence not an actual proof."

Thus the proof of negation of Con(PA) can be understood in terms of proofs of nonstandard length and failure of well-foundedness.

Inside a model of $PA + \neg Con(PA)$ one can give a proof of a contradiction from PA; this model and this proof (whether a sequence or a tree of formulas satisfying the deduction rules at each step) are necessarily non-well-founded.

So a metalanguage proof cannot be devised for such a contradiction, but the object (formal) language admits such a proof.

  • 1
    $\begingroup$ Would the downvoter please stand up? $\endgroup$ Commented Jun 23 at 15:15
  • 1
    $\begingroup$ Here is an upvote to fight the resistance of downvoters. $\endgroup$
    – Jii
    Commented Jun 23 at 15:23
  • $\begingroup$ Thanks I'm still trying to understand the concepts in your answer and was wondering what the relevance of there not being a proof of $\forall n P(n)$ has when considering the truth of $\forall n P(n)$ given $\forall n \in \mathbb{N} \vdash P(n)$, as truth doesn't imply provability. Also, am I understanding your answer correctly so far when it seems like you are showing the converse doesn't hold (you are showing that $\forall n P(n)$ doesn't necessarily imply $\forall n \in \mathbb{N} \vdash P(n)$ rather than vice versa)? $\endgroup$ Commented Jun 23 at 18:20
  • 1
    $\begingroup$ If $P(n)$ is the sentence "there is no proof of length $n$ of $\neg Con(PA)$", then establishing $P(n)$ for each metanatural $n$ does not yet establish the object-language formula $(\forall n) P(n)$ as it may fail for a nonstandard $n$. $\endgroup$ Commented Jun 24 at 7:36
  • $\begingroup$ Incidentally, part of the difficulty could be that you seem to think that writing down the string $1,2,3,\ldots$ pins down a specific mathematical entity in a fully determined way. It's a little more complicated than that :-) $\endgroup$ Commented Jun 24 at 7:46

(1) Let's use $\mathbf{n}$ as our numeral for the number $n$. Let $\varphi(x)$ be an open sentence of formal arithmetic. Then of course, if each instance of $\varphi(\mathbf{n})$ is true in the standard model of arithmetic, then $\forall x\varphi(x)$ is true in that model -- since in that model, all the numbers have a corresponding numeral name.

So the crucial first point is this. The claim you are alluding to, about a lack of implication between having available all instances of $\varphi(\mathbf{n})$ and getting $\forall x\varphi(x)$ is a claim about provability, not a claim about truth.

(2) To expand just a little on @spaceisdarkgreen's comment, which makes exactly the key point:

Here's a standard definition:

An arithmetic theory $T$ is $\omega$-incomplete iff, for some open wff $\varphi(x)$, $T$ can prove each wff of the form $\varphi(\textbf{n})$ (where $\textsf{n}$ is $T$'s formal numeral for the number $n$) but $T$ can't go on to prove $\forall x\varphi(x)$.

Look hard at the definition. Certainly there are two different ideas here. Fix on a particular $\varphi(x)$. Then compare claim (A):

$T$ has the deductive power to prove each and every wff of the from $\varphi(\textbf{n}).$

with claim (B):

$T$ has the deductive power to prove the quantified wff $\forall x \varphi(x)$.

And we can very easily imagine an impoverished formal theory $B$ ('Baby Arithmetic') that e.g. proves each wff of the form $\mathbf{2n} = \mathbf{n} + \mathbf{n}$ but can't prove $\forall x(2x = x + x)$ for the boring reason that the formal theory $B$ doesn't know about quantifiers!

(3) OK, but suppose we are dealing with a theory $T$ like Peano Arithmetic which can handle quantified statements. Then, yes, it would of course be nice if whenever (A) is true, then (B) is true. Our guess, pre-1931, might very well be that PA, first-order Peano Arithemtic, is $\omega$-complete.

However, bad news, it follows immediately from the proof of (the syntactic version of) Gödel's first incompleteness theorem that e.g. PA is $\omega$-incomplete. (But to repeat, that's a claim about PA's deductive weakness: of course, for a particular $\varphi$, if each instance of $\varphi(\mathbf{n})$ is true on the standard model, then $\forall x\varphi(x)$ will be true on that model too.)

If you want a proof of that, you'll find an accessible one e.g. on pp. 90-92 of my Gödel Without Too Many Tears which you can download freely from https://www.logicmatters.net/igt. That book will also tell you why we can't beef up PA and make it $\omega$-complete without making it either inconsistent or not computably axiomatizable.

  • $\begingroup$ There are ways of interpreting logic so that truth acts ω-inconsistently. For instance, in the effective topos, if $\mathsf{Halts}(n)$ is the predicate that means that the $n$th Turing machine halts on empty input, then $\mathsf{Halts}(\mathbf{n}) ∨ ¬\mathsf{Halts}(\mathbf{n})$ is true for every numeral $\mathbf{n}$, but $∀n. \mathsf{Halts}(n) ∨ ¬ \mathsf{Halts}(n)$ is false. $\endgroup$
    – Dan Doel
    Commented Jun 23 at 17:22
  • $\begingroup$ There are "ways of interpreting logic" where all kinds of whacky things happen -- ask the dialetheists. But I doubt that thinking about Eff is relevant the OP's concerns addressed here. $\endgroup$ Commented Jun 23 at 20:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .