Timeline for Is there a consistent, unsound, $\omega$-inconsistent, effective theory that doesn't prove its own inconsistency?
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 10, 2023 at 16:30 | history | rollback | Noah Schweber |
Rollback to Revision 2
|
|
| Sep 10, 2023 at 16:24 | comment | added | Noah Schweber | @ZuhairAl-Johar Sure, use $\mathsf{KP}+\neg Con(\mathsf{ZFC})$ instead, where $Con$ is phrased set-theoretically instead of arithmetically. | |
| Sep 10, 2023 at 13:45 | comment | added | Zuhair Al-Johar | @NoahSchweber, is there an example where $T$ is not formalized in the language of arithmetic? | |
| Sep 10, 2023 at 12:15 | vote | accept | Zuhair Al-Johar | ||
| Sep 10, 2023 at 12:14 | history | edited | Zuhair Al-Johar | CC BY-SA 4.0 |
deleted 1 character in body
|
| Sep 10, 2023 at 3:49 | comment | added | Pace Nielsen | Thanks, that clarifies things. If I'm understanding correctly, we just need a theory strong enough where Godel's 2nd incompleteness theorem can be internalized. So we could take $T=Q + \neg Con (Q+Con(Q))$, where $Q$ is Robinson arithmetic. (And note, neither $PA+Con(PA)$ nor $Q+Con(Q)$ proves its own inconsistency, so optimizing for system-strength doesn't lead us to a bad place.) | |
| Sep 10, 2023 at 3:32 | comment | added | Noah Schweber | 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. | |
| Sep 10, 2023 at 3:30 | comment | added | Noah Schweber | @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]$." | |
| Sep 10, 2023 at 3:29 | comment | added | Pace Nielsen | I think my question boils down to what "reasoning in $ZFC$" means, in this context. For my purposes, let's use $ZFC'$ instead. What does it mean to "reason in $ZFC'$"? For example, $ZFC'$ thinks of itself as inconsistent, so should we take it for granted that $1=0$, since we are reasoning in $ZFC'$? | |
| Sep 10, 2023 at 3:20 | comment | added | Noah Schweber | @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. | |
| Sep 10, 2023 at 3:18 | comment | added | Pace Nielsen | My question is regarding your last sentence. I don't see how $ZFC$ proving $Con(PA)$ implies that it also proves $Con(T)$. My use of $ZFC'$ and $T'$ was only meant to peel away a lot of irrelevancies. I don't understand how $ZFC'\vdash Con(PA)$ would imply $ZFC'\vdash Con(T')$. | |
| Sep 10, 2023 at 3:08 | comment | added | Noah Schweber | 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. | |
| Sep 10, 2023 at 3:07 | comment | added | Noah Schweber | @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) | |
| Sep 10, 2023 at 2:57 | comment | added | Pace Nielsen | I'm still not following your argument. Try the following. Replace $ZFC$ everywhere with $ZFC':=PA+Con(PA)+\neg Con(PA+Con(PA))$, and let $T'=PA+\neg Con(ZFC')$. Your same argument seems to apply. | |
| Sep 10, 2023 at 2:35 | history | edited | Noah Schweber | CC BY-SA 4.0 |
added 254 characters in body
|
| Sep 10, 2023 at 2:16 | comment | added | Pace Nielsen | If you replace $ZFC$ with $PA+Con(PA)$ everywhere, then you can greatly weaken your consistency/soundness assumptions. | |
| Sep 10, 2023 at 1:43 | history | answered | Noah Schweber | CC BY-SA 4.0 |