-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
    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
    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$ Apr 24, 2022 at 16:51
  • $\begingroup$ @ZuhairAl-Johar I still don't know what these are supposed to signify. $\endgroup$
    – Wojowu
    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$ 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$ Apr 25, 2022 at 1:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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