-2
$\begingroup$

I was thinking about a principle that occurred to me regarding provability in ZFC and truth. The principle outrageously states that: whatever ZFC shows, it is! In other words whatever ZFC can prove then there is nothing more. I personally think that this must be inconsistent, yet I think there might be a possible modification of it that renders it consistent, and the question is about whether this endeavour had been done before.

Formally; let $\phi,\psi$ be formulas in which only symbol $X$ occur free, then:

$$\forall X \big{[} ({\sf ZFC} \vdash \phi(X)) \implies \psi(X) \big{]} \\ \implies \\ \forall X \big{[} \phi(X) \implies \psi(X) \big {]}$$

Some instances of this are very strong (when added to ZFC). For example it proves global failure of the continuum hypothesis (except trivially for $0,1$).

Another instance that I've recently been pondering is about "size-unreachable" sets, which are sets of all strictly smaller subsets of them. It appears that ZFC only manage to prove $0,1,V_\omega$ to be size-unreachable, and limiting size-unreachable sets to only those is also very strong, I think it also implies generalized failure of the continuum hypothesis, and possibly might prove to be even stronger.

What counter-examples are to this principle?

Is there a known consistent version?

$\endgroup$
1
  • 3
    $\begingroup$ "$ZFC\vdash\phi(X)$" doesn't make sense. ZFC can't prove formulas involving parameters. $\endgroup$
    – Wojowu
    Commented Apr 24, 2022 at 11:53

1 Answer 1

2
$\begingroup$

If we drop the dependence on $X$ (see my comment above), your schema is equivalent to $\neg Con(ZFC)$.

Taking $\psi$ to be a false formula, the schema in particular implies $\phi\implies(ZFC\vdash\phi)$. Plugging in $\phi$ to be CH and then negation of CH, we get that your schema implies $ZFC\vdash CH\lor ZFC\vdash\neg CH$, which implies $\neg Con(ZFC)$.

Conversely, if we assume $\neg Con(ZFC)$, then $ZFC\vdash\phi$ holds for all $\phi$, and hence $(ZFC\vdash\phi)\implies\psi$ is equivalent to $\psi$. But obviously $\psi\implies(\phi\implies\psi)$.

$\endgroup$
6
  • $\begingroup$ @ZuhairAl-Johar I'm not entirely sure what this sequence of formulas has to do with your question or my answer. $\endgroup$
    – Wojowu
    Commented Apr 24, 2022 at 15:13
  • $\begingroup$ You are right! I've made a typo, the formula should be: ${\sf ZFC} \vdash \exists x. \psi \land \phi \\ {\sf ZFC} \vdash \forall x. \psi \to \phi \\ {\sf ZFC} \not \vdash \exists x. \neg \psi \land \phi \\ \implies \\ \forall x . \phi \to \psi$ $\endgroup$ Commented Apr 24, 2022 at 16:51
  • $\begingroup$ @ZuhairAl-Johar I still don't know what these are supposed to signify. $\endgroup$
    – Wojowu
    Commented Apr 24, 2022 at 17:14
  • $\begingroup$ it's a formal capture of the posed question. If the first three conditions are met which literally means that ZFC is proving every x satisfying $\psi$ to fulfill $\phi$ and prove existence of at least one x satisfying $\psi$, and if ZFC doesn't prove an object other than those satisfying $\psi$ to fulfill $\phi$; then all objects satisfying $\phi$ must satisfy $\psi$. That is, the inability of ZFC to prove objects outside $\psi$ to satisfy $\phi$ is turned into a truth, i.e. no object outside $\psi$ can satisfy $\phi$ $\endgroup$ Commented Apr 24, 2022 at 18:56
  • 3
    $\begingroup$ @ZuhairAl-Johar Here is an informal variant of your idea that illustrates the basic difficulty. Consider the informal principle that if $\mathsf{ZFC} \not\vdash \phi$, then $\phi$ is false. If $\mathsf{ZFC}$ is consistent, then by incompleteness, there exists $\phi$ such that $\mathsf{ZFC} \not\vdash \phi$ and $\mathsf{ZFC} \not\vdash\neg\phi$. So both $\phi$ and $\neg\phi$ are false; but this is a contradiction. So $\mathsf{ZFC}$ is inconsistent. Now, this argument is sloppy, but it illustrates the kind of difficulty that any attempt at a more precise version is going to run up against. $\endgroup$ Commented Apr 25, 2022 at 1:15

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