Are there existential theorems of ZFC, or PA say, with no witnesses?

Ie does there exist a formula $\phi$ such that ZFC $\vdash\exists x \phi(x)$, but for all numerals $\underline{n}$, ZFC $\nvdash \phi(\underline{n})$?

Can you give an example of such a formula?

  • $\begingroup$ I meant an arithmetic statement, so ZFC $\vdash \exists x \in \omega \phi(x)$ $\endgroup$
    – McDuffin
    Dec 14 '14 at 15:22
  • $\begingroup$ I believe Goedel was the first to give such an example. (His construction works for any sufficiently expressive system, in particular for ZFC.) $\endgroup$ Dec 14 '14 at 17:41
  • 4
    $\begingroup$ "Shape without form, shade without colour, Paralysed force, gesture without motion" -- T.S. Eliot, The Hollow Men. $\endgroup$
    – Asaf Karagila
    Dec 14 '14 at 18:06
  • $\begingroup$ Goodstiein's Theorem (Kirby-Paris-Theorem) is an example for PA. $\endgroup$ Dec 15 '14 at 23:18
  • $\begingroup$ @Christoph-SimonSenjak: Not really. Goodstein’s theorem is $\Pi^0_2$, so it does not even start with an existential quantifier. And if you substitute a number for the outer universal quantifier to obtain an existential ($\Sigma^0_1$) statement, it will have a witness provable already in Robinson’s $Q$. $\endgroup$ Dec 16 '14 at 17:22

The answer is yes, provided these theories are consistent. For example, PA proves that there is a number $n$, such that if there is no proof of a contradiction in PA of size at most $n$, then there is no proof of a contradiction in PA at all. This is trivial if you think about it, since either there is a proof of a contradiction in PA, in which case you can let $n$ be any number larger than that proof, or else there isn't such a proof of a contradiction, in which case any $n$ has the desired property. But PA does not prove that any particular number $n$ has this property, since then PA would prove its own consistency, which violates the incompleteness theorem.

Here is another kind of example: Let $\sigma$ be any statement that is independent of PA, and let $\phi(n)$ assert that $(n=0\wedge\sigma)\vee(n=1\wedge\neg\sigma)$. So PA proves $\phi(0)\vee \phi(1)$, and in particular it proves $\exists x\ \phi(x)$, but PA doesn't prove either case separately, because $\sigma$ is independent.

If you strengthen the conclusion of your question, however, to say that the theory should actually prove $\neg\phi(n)$ for every numeral $n$, then you would be asking whether these theories are $\omega$-inconsistent. Of course, we all think that our theories are $\omega$-consistent, because we want and expect that the natural numbers referred to inside the theory are somehow the same as those in the meta theory. But of course, because of the incompleteness theorem, we cannot prove this within the theory itself. Notice that a theory must be $\omega$-consistent in the case that it has an $\omega$-model, a model in which the natural numbers of the model are the same as the natural numbers of the meta-theory. For this reason, our stronger theories can often prove that our weaker theories are $\omega$-consistent. For example, ZFC proves that PA is $\omega$-consistent, and ZFC+large cardinals proves that ZFC is $\omega$-consistent. My own view is the assertion that a theory is $\omega$-consistent is just one stop along a continuum, from assuming consistency up to iterated consistency up to having a well-founded model up to large cardinals and so on, moving up in consistency strength at each step.

Meanwhile, if these theories are consistent, then it is easy to make examples of $\omega$-inconsistent theories extending them. For example, the theories PA+$\neg$Con(PA) and ZFC+$\neg$Con(ZFC) are consistent by the incompleteness theorem, but not $\omega$-consistent, because each of them asserts that there is a certain proof of a contradiction, which is provably not instantiated by any actual natural number witness.

  • 1
    $\begingroup$ The existence of an $\omega$-model is equivalent to consistency in $\omega$-logic, which is a much stronger property than just $\omega$-consistency. $\endgroup$ Dec 14 '14 at 15:58
  • $\begingroup$ Yes, you are right. I have edited. $\endgroup$ Dec 14 '14 at 16:07
  • $\begingroup$ One might add, however, that in the large cardinal realm this difference doesn't actually count as very much stronger. Typically, a stronger large cardinal provides a full transitive model of the weaker cardinals. $\endgroup$ Dec 14 '14 at 20:17
  • $\begingroup$ I agree with the sentiment, though I'd prefer to say that the existence of a transitive model is (in the realm of set theory) much stronger than the existence of an $\omega$-model, which is in turn much stronger than $\omega$-consistency. $\endgroup$ Dec 14 '14 at 23:07
  • $\begingroup$ Yes, of course I agree completely with that. $\endgroup$ Dec 14 '14 at 23:08

$\def\epn{\mathrm{EP}_\mathbb N}\def\dp{\mathrm{DP}}$When a theory $T$ (with a distinguished definable set of “natural numbers” satisfying a suitable minimal arithmetic) has the property in the question, viz.

$$\tag{$\epn$}T\vdash\exists x\in\mathbb N\,\phi(x)\text{ implies }T\vdash\phi(\underline n)\text{ for some $n\in\mathbb N$,}$$

$T$ is said to have the numerical existence property. As explained in Joel’s answer, classical theories can have the numerical existence property only if inconsistent or complete, which prevents any interesting examples by virtue of Gödel’s incompleteness theorem.

However, the situation is quite different for theories over intuitionistic logic. Indeed, most natural constructive theories (e.g., Heyting arithmetic) do have $\epn$.

Since $\phi\lor\psi$ is equivalent to $\exists n\,((n=0\land\phi)\lor(n=1\land\psi))$, $\epn$ implies the seemingly weaker disjunction property

$$\tag{$\dp$}T\vdash\phi\lor\psi\implies T\vdash\phi\text{ or }T\vdash\psi.$$

By a result of Harvey Friedman, $\dp$ is in fact equivalent to $\epn$ if $T$ is recursively axiomatizable.

We may stratify the definition by restricting the complexity of the formulas. A consistent recursively axiomatizable classical theory never has $\epn$ for $\Pi^0_1$ formulas, or $\dp$ for $\Pi^0_1$ sentences, or $\dp$ for $\phi\in\Sigma^0_1$ and $\psi\in\Pi^0_1$. This leaves $\Sigma^0_1$ as the only realistic possibility. Friedman’s argument shows that for recursively axiomatized $T$, the following are equivalent:

  1. $T$ has $\epn$ for $\Sigma^0_1$ formulas,

  2. $T$ has $\dp$ for $\Sigma^0_1$ sentences,

  3. $T$ is $\Sigma^0_1$-sound or inconsistent.

Naturally occurring theories are $\Sigma^0_1$-sound (e.g., PA) or assumed to be $\Sigma^0_1$-sound (e.g. ZFC).

See also Visser (§7) for an interesting connection of Friedman’s characterization to (non)interpretability of inconsistency.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.