Timeline for Can different extensions of ZF have contradictory consequences for first-order arithmetic?
Current License: CC BY-SA 3.0
24 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 15, 2013 at 1:18 | comment | added | Joel David Hamkins | Meanwhile, if $S$ is a full satisfaction class in NBG, then one can prove by induction on the lengths of proofs that whatever theory it shows as "true" must be consistent. In particular, if it shows ZF as true, then Con(ZF) holds. | |
| Aug 15, 2013 at 1:16 | comment | added | Joel David Hamkins | NBG cannot prove the existence of a truth predicate, if it is consistent, because some models of NBG have only first-order definable classes, and Tarski's theorem implies that there can never be a first-order definable truth predicate. | |
| Aug 15, 2013 at 0:58 | comment | added | Keshav Srinivasan | @JoelDavidHamkins Why can't the existence of a truth-predicate for truth in the language of ZF be proven in NBG? You said that if it were possible, then NBG would prove the consistency of ZF, but why is that? | |
| Aug 14, 2013 at 23:47 | comment | added | Joel David Hamkins | I suppose it would suffice to say: there is a partial truth predicate, with respect to which every theorem of ZF is true. | |
| Aug 14, 2013 at 23:05 | comment | added | Joel David Hamkins | Since the language of NBG is exactly the same as KM, defining "ZF is sound" in NBG is the same as defining it in KM. What one needs to say is: there is a truth predicate for first-order truth (this is provable in KM but not in NBG) and every theorem of ZF is true. | |
| Aug 14, 2013 at 20:31 | comment | added | Keshav Srinivasan | @TheUser I thought that Joel was saying that NBG can only prove for each formula that the proposed truth predicate works for that formula, and that you need KM to prove a single statement that says that a proposed truth predicate works for all formulas. But if you're right, then what distinguishes NBG and KM as far as the definability of a truth predicate? | |
| Aug 14, 2013 at 20:24 | comment | added | The User | @KeshavSrinivasan But then “working” is a property in your metalanguage, it cannot be expressed in NBG, thus you cannot ask whether its provability in NBG would imply anything. | |
| Aug 14, 2013 at 20:23 | comment | added | Keshav Srinivasan | @TheUser No, those consistency statements don't satisfy me; see the comment I just wrote in Joel's answer. | |
| Aug 14, 2013 at 20:19 | comment | added | Keshav Srinivasan | @TheUser The proposed truth predicate V(n) works for a given n if V(n) is equivalent to the formula coded by n. So the question is, does NBG prove that for all n, the proposed truth predicate works. | |
| Aug 14, 2013 at 20:10 | comment | added | The User | What do you mean by “works”? | |
| Aug 14, 2013 at 19:45 | comment | added | Keshav Srinivasan | @TheUser I assuned that Joel was talking about the statement that the proposed truth predicate works for all formulas in the language of ZF. And I was asking why NBG proving that statement would imply that NBG proves the consistency of ZF. | |
| Aug 14, 2013 at 19:27 | comment | added | The User | @KeshavSrinivasan Do the examples Con(NBG+“ZF is sound”) and Con(KM) satisfy you? | |
| Aug 14, 2013 at 19:25 | comment | added | The User | @KeshavSrinivasan Not by the specification, but by the assumption “every axiom of ZF is true (in V)”. I think that that is more or less what Joel called “every formula is covered by it”. @ Joel Or what did you mean? | |
| Aug 14, 2013 at 19:24 | comment | added | Keshav Srinivasan | @TheUser How would being able to prove in NBG that the proposed truth predicate for ZF works for all formulas allow you to prove the existence of a model of ZF? | |
| Aug 14, 2013 at 19:14 | comment | added | The User | @KeshavSrinivasan “how would that allow it to prove the consistency of ZF” You would have proved that V is a model of ZF, thus Con(ZF). Since NBG in conservative, this would imply that Con(ZF) is provable in ZF. | |
| Aug 14, 2013 at 19:10 | comment | added | The User | So consider the arithmetic statement Con(NBG+“NBG has an ω-model”), this cannot be proved using “soundness” of ZF. Or simply Con(NBG+“ZF is sound”). | |
| Aug 14, 2013 at 19:10 | comment | added | Keshav Srinivasan | @JoelDavidHamkins If NBG could prove that every formula is covered by the proposed truth predicate, how would that allow it to prove the consistency of ZF? | |
| Aug 14, 2013 at 19:07 | comment | added | Keshav Srinivasan | @TheUser Why does it matter that the soundness of ZF can't be proved in NBG? At least it can be defined in NBG, so within NBG we can still see what statements follow from the soundness of ZF. So does there exist some statement independent of ZF which doesn't follow from the soundness of ZF (and it's negation doesn't either), such that it has consequences for first-order arithmetic that ZF itself doesn't have? | |
| Aug 14, 2013 at 19:00 | comment | added | The User | @KeshavSrinivasan I have had a look at the paper: You are right, there is a truth predicate, but what you call “soundness” of ZF (i. e. the statement “every axiom of ZF is true”) cannot be proved in NBG. However, in an ω-model of NBG ZF is “sound”. | |
| Aug 14, 2013 at 18:51 | comment | added | Joel David Hamkins | To my (quick) reading of that theorem, Mostowski does not present a full satisfaction class, but rather a class that he proves works for any particular formula, as a scheme. This will result in merely a partial satisfaction class, as GBC will not in general prove that every formula is covered by it (and it cannot prove this, as this would mean GBC proves the consistency of ZF, which is impossible). If you google "partial satisfaction classes" you will find out more; most of the material is for models of arithmetic, but much of the theory carries over to set theory. | |
| Aug 14, 2013 at 18:44 | comment | added | Keshav Srinivasan | @JoelDavidHamkins I just put a link in my question to a paper by Mostowski, which seems to show that the truth predicate of ZF is expressible in NBG. Am I interpreting it incorrectly? Also, about Con(KM), is it possible for ZF to be sound and yet KM to be inconsistent? In other words, if someone found an inconsistency in Morse-Kelly set theory tomorrow, would that mean that the axioms of ZF can't all be true? | |
| Aug 14, 2013 at 12:12 | comment | added | Joel David Hamkins | @KeshavSrinivasan, NBG does not prove the existence of a first-order truth predicate, although KM does. In this case, you could use Con(KM), which if true, is independent of ZF and implies the consistency of a standard model of ZF, which is elementary in V. Thus, it is similar to the other examples we have here. | |
| Aug 14, 2013 at 4:53 | comment | added | Keshav Srinivasan | I am indeed talking about soundness in the sense of every theorem of ZF being true, or equivalently the axioms of ZF all being true. When I was talking about following from soundness, I was speaking metamathematically, I meant that there should be no way to conclude metamathematically that X or its negation is true from the assumption that ZF is sound. Or if you feel that talking about metamathematically reasoning is too informal, then here's a way to make it more precise: I think the truth predicate for ZF is expressible in NBG set theory, so we can talk about proving X using that. | |
| Aug 14, 2013 at 4:27 | history | answered | Andreas Blass | CC BY-SA 3.0 |