Can we have a consistent and effective (fulfilling Godel's criteria) first order theory $T$, that is both arithmetically unsound and $\omega$-inconsistent, and yet doesn't prove its own inconsistency ( i.e. $T \not \vdash \neg \operatorname {Con}(T)$)?
$\begingroup$
$\endgroup$
8
asked Sep 10, 2023 at 0:24
-
1$\begingroup$ "both unsound and $\omega$-inconsistent"? Isn't that redundant? What would be an example of a theory that's sound and $\omega$-inconsistent? Maybe I don't understand what "unsound" means (or what $\omega$-inconsistent means), I'm not a logician. $\endgroup$– bofCommented Sep 10, 2023 at 3:58
-
$\begingroup$ @bof, Not it is not redundant. See: $\omega$-consistent theory $\endgroup$– Zuhair Al-JoharCommented Sep 10, 2023 at 11:58
-
3$\begingroup$ If the theory is expressed in the language of arithmetic, then it is redundant. An $\omega$-inconsistent theory proves every instance $\varphi(n)$ of some formula, but also $\neg\forall x\ \varphi(x)$. This violates soundness, since either some $\varphi(n)$ is not actually true or the universal is true. $\endgroup$– Joel David HamkinsCommented Sep 10, 2023 at 12:53
-
$\begingroup$ @JoelDavidHamkins, so is arithmetically sound and being $\omega$-consistent equivalent if the theory is expressed in the language of arithmetic? $\endgroup$– Zuhair Al-JoharCommented Sep 10, 2023 at 13:43
-
1$\begingroup$ No, because the theory $\text{PA}+\neg\omega\text{-Con}(\text{PA})$ in your link is unsound but $\omega$-consistent. $\endgroup$– Joel David HamkinsCommented Sep 10, 2023 at 13:55
|
Show 3 more comments
2 Answers
$\begingroup$
$\endgroup$
12
Sure. Consider something like $T=\mathsf{PA}+\neg\mathit{Con}(\mathsf{ZFC})$ (assuming $\mathsf{ZFC}$ is actually consistent of course).
$T$ is consistent but not $\omega$-consistent (it proves that each specific natural number fails to be a $\mathsf{ZFC}$-proof of $\perp$, but still proves that some number is a $\mathsf{ZFC}$-proof of $\perp$).
More interestingly, $T\not\vdash\neg \mathit{Con}(T)$. To see this, note that if it did we would have $\mathsf{PA}$-provably that $\neg\mathit{Con}(\mathsf{ZFC})\rightarrow\neg\mathit{Con}(T)$. Taking the contrapositive and shifting to the stronger theory $\mathsf{ZFC}$, we would get $$\mathsf{ZFC}\vdash\mathit{Con}(T)\rightarrow\mathit{Con}(\mathsf{ZFC}),$$ a contradiction since $\mathsf{ZFC}$ already proves the consistency of $T$. (Why does $\mathsf{ZFC}$ prove the consistency of $T$? If $T$ were inconsistent then $\mathsf{PA}$ would prove $\mathit{Con}(\mathsf{ZFC})$ and hence be inconsistent. So since $\mathsf{ZFC}$ proves that $\mathsf{PA}$ is consistent, $\mathsf{ZFC}$ also proves that $T$ is consistent.)
answered Sep 10, 2023 at 1:43
-
1$\begingroup$ @PaceNielsen I'm not sure I see the problem - it doesn't look to me like your $T'$ does prove its own inconsistency. Your $T'$ thinks that $\mathsf{ZFC}'\vdash\perp$, which is to say (via the deduction theorem) that $$\mathsf{PA}+Con(\mathsf{PA})\vdash Con(\mathsf{PA}+Con(\mathsf{PA})).$$ Consequently, your $T'$ thinks that $\mathsf{PA}+Con(\mathsf{PA})$ is inconsistent by the (internalized) second incompleteness theorem. But so? $T'$ doesn't literally contain that theory, it only contains $\mathsf{PA}$. (cont'd) $\endgroup$ Commented Sep 10, 2023 at 3:07
-
1$\begingroup$ And if we replace your $T'$ with $\mathsf{ZFC}'+\neg Con(\mathsf{ZFC}')$ - call the result $T''$ - then we lose the analogue of the step in my argument where $\mathsf{ZFC}\vdash Con(T)$: it is not the case that $\mathsf{ZFC}'$ proves the consistency of $T''$. So I think you've just found another (much more parsimonious but slightly trickier to check) instance of a pair of theories to which my argument applies. $\endgroup$ Commented Sep 10, 2023 at 3:08
-
2$\begingroup$ @PaceNielsen That's what the sentence before it explains, which I'll expand on a bit here for readability: reasoning in $\mathsf{ZFC}$, the only way that $\mathsf{PA}+\neg Con(\mathsf{ZFC})$ could be inconsistent is if $\mathsf{PA}\vdash Con(\mathsf{ZFC})$. But that would a fortiori imply $\mathsf{PA}\vdash Con(\mathsf{PA})$, hence $\mathsf{PA}$ is inconsistent - which $\mathsf{ZFC}$ knows isn't the case. $\endgroup$ Commented Sep 10, 2023 at 3:20
-
2$\begingroup$ @PaceNielsen No. $\mathsf{ZFC}'$ does not believe that $\perp$ (or $0=1$) is true; it does believe that $\mathsf{ZFC}'\vdash\perp$ is true. More precisely (but conflating meta-level sentences with their arithmetizations for simplicity), we have $$\mathsf{ZFC}'\not\vdash\perp\quad\mbox{but}\quad \mathsf{ZFC}'\vdash (\mathsf{ZFC}'\vdash\perp)$$ "Reasoning in $[X]$" just means "everything that follows is provable in $[X]$." $\endgroup$ Commented Sep 10, 2023 at 3:30
-
1$\begingroup$ Incidentally, this is exactly why I phrased my answer with $\mathsf{PA}$ and $\mathsf{ZFC}$; optimizing for system-strength forces us to reason inside theories that prove their own inconsistency, and that's often a stumbling block. $\endgroup$ Commented Sep 10, 2023 at 3:32
$\begingroup$
$\endgroup$
Noah's answer may be the best here. But I'll add this as an additional answer. In particular, the theory in question is not fully formalized in the language of arithmetic.
Let's take theory $\sf PA + \neg \, \omega$-$\sf \operatorname{Con}(PA)$, this is an arithmetically unsound $\omega$-consistent arithmetic theory. Now, to break $\omega$-consistency we can add a primitive constant $c$ to it's language, then add the schema: $$ [\mathcal S_n(0) < c]_{n=0,1,2,..}$$ Where $ \mathcal S_n(0)$ denotes the $n$-iterated successor of $0$, where of course $n$ being concrete natural. This would break $\omega$-consistency at $c$ for the property $(x < c)$.
So, this theory is both arithmetically unsound and $\omega$-inconsistent.
Now, the base theory $\sf PA + \neg \, \omega$-$\sf \operatorname{Con}(PA)$, being $\omega$-consistent, cannot prove its own inconsistency, and since the above theory is obtained through compactness from the base theory then it cannot prove a sentence in the language of the base theory that the base theory itself cannot prove. Hence, $T \not \vdash \neg \operatorname{Con}(T)$.
answered Sep 10, 2023 at 15:09