Timeline for Can different extensions of ZF have contradictory consequences for first-order arithmetic?
Current License: CC BY-SA 3.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 15, 2013 at 2:14 | comment | added | Keshav Srinivasan | @JoelDavidHamkins See my comment to my question, where I give an argument that seems to show that Con(KM + all true Pi_1 statements) is actually Pi_1. | |
| Aug 15, 2013 at 1:42 | comment | added | Joel David Hamkins | Well, I'm finding your question to be a moving target. For your latest version, in the previous comment, it seems that you can use Con(KM+true $\Pi^0_1$), meaning the consistency of the theory of KM with the collection of $\Pi^0_1$ sentences that happen to be true. Note that this consistency assertion is no longer $\Pi^0_1$, since the theory is not computable, but it is $\Pi^0_2$. | |
| Aug 15, 2013 at 1:31 | comment | added | Keshav Srinivasan | (cont'd) So to sum up, I want a statement X such that (1). NBG doesn't prove that "ZF is sound" implies X and NBG doesn't prove that "ZF is sound" implies not X; (2). ZF would not prove either X or not X if X were false; (3). ZF + X proves a statement of arithmetic that ZF by itself doesn't prove. Now admittedly, (2) is a bit vague, but for all practical purposes it means that X shouldn't be a Pi_1 statement. | |
| Aug 15, 2013 at 1:24 | comment | added | Keshav Srinivasan | @TheUser I don't quite understand what you're saying, but we may be having a misunderstanding due to me not phrasing my objection to consistency statements well enough. I think my new edit to my question may clarify things. The problem is that consistency statements are Pi_1, and Pi_1 statements can always be disproven if they're wrong, in both ZF and PA. So a consistency statement is only independent of ZF is in fact true. (to be continued) | |
| Aug 14, 2013 at 22:29 | comment | added | The User | @KeshavSrinivasan Then you would have to give another definition of soundness in a different system than NBG. And NBG is already very mild, it is a conservative extension and they are equiconsistent. Furthermore, you can play the same game in any extension of ZF where you can speak about soundness. | |
| Aug 14, 2013 at 22:05 | comment | added | Keshav Srinivasan | @TheUser Yes, an inconsistency in NBG + "ZF is sound" would imply that NBG proves that ZF is not sound, but that wouldn't imply that ZF is not sound. It's certainly possible for ZF to be sound and for NBG to imply that ZF is not sound. All that would mean is that NBG is not sound. | |
| Aug 14, 2013 at 21:45 | comment | added | Joel David Hamkins | @Keshav, I'm sorry that you don't like the Con(KM) example, although I believe it does answer the question that you've asked. Indeed, it is my impression that you've received several thoughtful answers here to your various questions, as well as help in formulating your intention... | |
| Aug 14, 2013 at 21:27 | comment | added | The User | @KeshavSrinivasan Assuming your formal definition of soundness of ZF in NBG a contradiction in NBG+“ZF is sound” would of course imply that NBG proves that ZF is not sound. And I cannot imagine formal formulations of soundness with weaker consistency assumptions. | |
| Aug 14, 2013 at 20:49 | comment | added | Keshav Srinivasan | @TheUser No, that's not true. The inconsistency of NBG + "ZF is sound" would imply that NBG is unsound, but I don't see how it would imply that ZF is unsound. In any case, even if you're right, then that's all the more reason to reject Con(NBG+“ZF is sound”) as the kind of statement I'm looking for, because its truth value would follow from the assumption that ZF is sound. | |
| Aug 14, 2013 at 20:28 | comment | added | The User | @KeshavSrinivasan But if Con(NBG+“ZF is sound”) is false, then your assumption of soundness of ZF cannot hold. | |
| Aug 14, 2013 at 20:17 | comment | added | Will Sawin | I think we can prove the existence of an undecidable statement that is not decided by any true consistency statement by considering the theory ZF + all true $\Pi_1$ statements. We just need an arithmetic statement that is undecidable in this theory. Such a statement exists, because if it didn't, a Turing machine with a Halting oracle could decide truth values of arithmetic statements. But it is known that it cannot. | |
| Aug 14, 2013 at 20:14 | comment | added | Keshav Srinivasan | Ny problem with your example Con(KM) and @TheUser's example Con(NBG + "ZF is sound"), is that if they're true, then yes they are independent of ZF. But if they're false, i.e. if the underlying theory is inconsistent, then they can be proven false in ZF and even in PA. The same goes for any consistency statement, so I want something other than a consistency statement, something that must be independent of ZF regardless of whether it's true or false. The axiom of choice meets that condition, but again it proves no new arithmetical truths. So I want something that does. | |
| Aug 14, 2013 at 18:45 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
Update
|
| Aug 14, 2013 at 8:55 | comment | added | The User | @KeshavSrinivasan So you are using an informal metalanguage and assume a Platonic notion of sets and soundness of ZF means that these sets are a “model” of ZF? Well, if your notion of soundness is not defined by a formal system but a philosophical notion, then what is an “implication” of this kind of soundness? And how should we tell whether there is such an implication? (and even philosophically this notion is questionable) | |
| Aug 14, 2013 at 4:37 | comment | added | Keshav Srinivasan | @JoelDavidHamkins I'm not trying to define truth or soundness within the language of set theory. I'm speaking metamathematically about the soundness of ZF. I want a statement X which, metamathematically speaking, is not consequence of the soundness of ZF. (And neither is the negation of X.) The axiom of choice is an example of such a statement, because you can't conclude either choice or its negation from the assumption that the axioms of ZF are true. But unfortunately, the axiom of choice can't prove any statements of first-order arithmetic that ZF can't already prove. | |
| Aug 14, 2013 at 4:25 | comment | added | Joel David Hamkins | That is, while we are able to express in set theory that a given theory T is arithmetically sound, or sound for assertions about hereditarily countable sets, or about $H_{\omega_2}$ and so on, we are not able to formulate the notion of a set theory $T$ being "sound" in general, in the sense of having only true consequences. A straightforward way to saying it would use a truth predicate, which we have none by Tarski's theorem. | |
| Aug 14, 2013 at 4:22 | comment | added | Joel David Hamkins | I'm not sure exactly what you mean. Tarski's theorem on the non-definability of truth shows that we can have no formal concept of "true" that is expressible within our theory. So you'll have to be more precise about exactly what you mean. | |
| Aug 14, 2013 at 4:15 | comment | added | Keshav Srinivasan | @JoelDavidHamkins I didn't mean arithmetic soundness, I meant soundness in general; I want a statement whose truth value is not a consequence of the assumption that the axioms of ZF are true. If ZF is sound, then it's consistent, so ZF + there is a measurable cardinal is consistent, so Con(ZF + there is a measurable cardinal) is true. | |
| Aug 14, 2013 at 3:40 | comment | added | Joel David Hamkins | Keshav, my edit show that there are many example arising from the large cardinal hiearchy. Basically, any true assertion of the form Con(ZF+ $\exists$ large cardinal) will be independent of ZF, but not deducible merely from the arithmetic soundness of ZF, since the consistency strength exceeds the strength of the existence of an $\omega$-model of ZF, which implies the arithmetic soundness of ZF. | |
| Aug 14, 2013 at 3:39 | comment | added | Asaf Karagila♦ | Joel, nice example on the consistency of large cardinals. I feel that this example is still somehow "cheating" and misses the examples the OP is after; but I'm getting a vibe that maybe the OP doesn't know what he is looking for exactly either. | |
| Aug 14, 2013 at 3:36 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
added 1296 characters in body
|
| Aug 14, 2013 at 3:26 | comment | added | Keshav Srinivasan | Yes, I want examples which you can't deduce the truth value of simply by assuming that ZF is sound. | |
| Aug 14, 2013 at 3:23 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |