[Math] Platonic Truth and 1st Order Predicate Logic

lo.logicmodel-theory

Consider the following simple example as motivation for my question. If it were the case that, say, the Riemann hypothesis turned out to be independent of ZFC, I have no doubt it would be accepted by many as a new axiom (or some stronger principle which implied it). This is because we intuitively think that if we cannot find a zero off of the half-line, then there is no zero off the half-line. It just doesn't "really" exist.

Similarly, if Goldbach's conjecture is independent of ZFC, we would accept it as true as well, because we could never find any counter-examples.

However, is there any reason we should suppose that adding these two independent statements as axioms leads to a consistent system? Yes, because we have the "standard model" of the natural numbers (assuming sufficient consistency).

But can this Platonic line of thinking work in a first-order way, for any theory? Or is it specific to the natural numbers, and its second-order model?

In other words, let $T$ be a (countable, effectively enumerable) theory of first-order predicate logic. Define ${\rm Plato}(T)$ to be the theory obtained from $T$ by adjoining statements $p$ such that: $p:=\forall x\ \varphi(x)$ where $\varphi(x)$ is a sentence with $x$ a free-variable (and the only one) and $\forall x\ \varphi(x)$ is independent of $T$. Does ${\rm Plato}(T)$ have a model? Is it consistent?

The motivation for my question is that, as an algebraist, I have a very strong intuition that if you cannot construct a counter-example then there is no counter-example and the corresponding universal statement is "true" (for the given universe of discourse). In particular, I'm thinking of the Whitehead problem, which was shown by Shelah to be independent of ZFC. From an algebraic point of view, this seems to suggest that Whitehead's problem has a positive solution, since you cannot really find a counter-example to the claim. But does adding the axiom "there is no counter-example to the Whitehead problem" disallow similar new axioms for other independent statements? Or can this all be done in a consistent way, as if there really is a Platonic reality out there (even if we cannot completely touch it, or describe it)?

Best Answer

The phenomenon accords more strongly with your philosophical explanation if you ask also that the sentences have complexity $\Pi^0_1$. That is, the universal statement $\forall x\ \varphi(x)$ should have $\varphi(x)$ involving only bounded quantifiers, so that we can check $\varphi(x)$ for any particular $x$ in finite time. If you drop that requirement, there are some easy counterexamples, hinted at or given already in the comments and other answers.

But meanwhile, even in the case you require $\varphi(x)$ to have only bounded quantifiers, there is still a counterexample.

Theorem. If $\newcommand\PA{\text{PA}}\newcommand\Con{\text{Con}}\PA$ is consistent, then there is a consistent theory $T$ extending $\PA$ with two $\Pi^0_1$ sentences $$\forall x\ \varphi(x)$$ $$\forall x\ \psi(x)$$ both of which are consistent with and independent of $T$, but which are not jointly consistent with $T$.

Proof. Let $T$ be the theory $\PA+\neg\Con(\PA)$, which is consistent if $\PA$ is consistent. Let $\rho$ be the Rosser sentence of this theory, which asserts that the first proof in $T$ of $\rho$ comes only after the first proof of $\neg\rho$ (see also my discussion of the Rosser tree). Our two $\Pi^0_1$ sentences are:

  • every proof of $\rho$ from $T$ has a smaller proof of $\neg\rho$.
  • every proof of $\neg\rho$ from $T$ has a smaller proof in $T$ of $\rho$.

The first statement is equivalent to $\rho$, and the second is equivalent over $T$ to $\neg\rho$, since $T$ proves that every statement is provable; the only question is which proof comes first. So both statements are consistent with $T$.

But the sentences are not jointly consistent with $T$, since in any model of $T$, both $\rho$ and $\neg\rho$ are provable from $T$, and so one of the proofs has to come first. QED

Related Question