Models of set theory vs. models of first order theories
in [Logic]
|
Prev: found the 10% in Geometry; Poincare dodecahedral space; 36 degree twist; matched-circles #378 Correcting Math
Next: The set theoretic content of the transfinite recursion theorem
From: Marc Alcobé García on 11 Feb 2010 10:19 > So there is an important distinction between (1) a theory proving the > consistency of another theory and (2) a relative consistency. What you say sounds good, and I am sure it is correct. But I would like to see the reason why things go the way you mean. It is a bit hard for me because: |-_ZFI Con(ZF) is a statement in the metatheory that says that there is a formal proof in ZFI of the statement Con(ZF). So in the formal theory ZFI there must be a statement asserting the consistency of ZF. I wonder how does that statement look like, because ZFI talks about sets, and not about theories of sets... You say that |-_ZFI Con(ZF) leads you to look at its proof, which is showing that V_i (where i is some inaccessbible cardinal) is a universe for a model of ZF. How do you prove that V_i is a universe for a model of ZF? Is it by showing that every axiom of ZF relativized to V_i is provable in ZFI? In that case, the notation |-_ZFI Con(ZF) is misleading, because, what we actually have is |-_ZFI (A relativized to V_i) for every axiom A of ZF. You already know that ZF is not finitely axiomatizable, and keeping our metatheory finitistic, there is no way to express in ZFI the conjunction of every formula (A relativized to V_i). From the proofs of |-_ZFI (A relativized to V_i) for every axiom A of ZF in the metatheory it follows, via the interpretation theorem, whose proof every author says is finitary, that the consistency of ZF follows from the consistency of ZFI. On the contrary, Con(ZFI) -> Con(ZF) is a statement in the metatheory that says that there is no way to formally derive a contradiction from ZF whenever the same happens with ZFI. Of course, the proof of this in the metatheory is trivial since all the axioms of ZF belong to ZFI. We obtain the same result but with much less effort... Perhaps what you learn from the proofs of |-_ZFI (A relativized to V_i) for every axiom A of ZF is that ZF is interpretable in ZFI. This looks a lot less trivial.
From: MoeBlee on 11 Feb 2010 12:28 On Feb 11, 9:19 am, Marc Alcobé García <malc...(a)gmail.com> wrote: > |-_ZFI Con(ZF) is a statement in the metatheory that says that there > is a formal proof in ZFI of the statement Con(ZF). > > So in the formal theory ZFI there must be a statement asserting the > consistency of ZF. I wonder how does that statement look like, because > ZFI talks about sets, and not about theories of sets... In Z (perforce in ZFI) we can formalize mathematical logic, including formalizing consistency statements. > How do you prove that V_i is a universe > for a model of ZF? As I recall, it's in Enderton's set theory book. If I'm not mistaken, it's even a standard model (i.e. the symbol 'e' maps to the membership relation on the universe) and consistency is proven by showing that every axiom of ZF is true in the model <V_i membership-on-V_i>. But I should doublecheck that. If you have the book, I recommend looking up the chapter. If you don't have the book, and if you like, I'll report back after I refresh my memory by looking it up. > Is it by showing that every axiom of ZF relativized > to V_i is provable in ZFI? As I recall, it's that M = <V_i membership-on-V_i> is a model of the ZF axioms. We do that by proving every ZF axiom is true in M. Of course, doing that may reduce to showing that ZF proves the relativization (to V_i) of every ZF axiom. > In that case, the notation |-_ZFI Con(ZF) is misleading, because, what > we actually have is |-_ZFI (A relativized to V_i) for every axiom A of > ZF. If I'm not mistaken, we can even say: |-_ZF (A relativized to V_i) for every axiom A of ZF. Notice though, that V_i is not a SET in ZF, but rather 'V_i' is shorthand for verbiage in some metalanguage for ZF. "|-_ZFI Con(ZF)" is not miseleading. It says that in the theory ZFI there is a proof that ZF is consistent. And that is true. In ZFI there is a proof that ZF has a model thus that ZF is consistent. > You already know that ZF is not finitely axiomatizable, and > keeping our metatheory finitistic, there is no way to express in ZFI > the conjunction of every formula (A relativized to V_i). (1) I didn't claim that ZFI is finitistic. There IS NO finitistic proof of the consistency of ZF (given a certain reasonable sense of 'finitistic"). (2) It is not required to try to cram the axioms of ZF into a finite set. Even though they are an infinite set, we may quantify over them. So we may say things like "For A, if A is a ZF axiom, then A is true in the model <V_i membership-on-V_i>". > From the proofs of |-_ZFI (A relativized to V_i) for every axiom A of > ZF in the metatheory it follows, via the interpretation theorem, whose > proof every author says is finitary, that the consistency of ZF > follows from the consistency of ZFI. I don't dispute that there is a finitary proof of the interpretation theorem. However, there is no finitary proof of the consistency of ZF. > On the contrary, > > Con(ZFI) -> Con(ZF) is a statement in the metatheory that says that > there is no way to formally derive a contradiction from ZF whenever > the same happens with ZFI. I think you mean: "Con(ZFI) -> Con(ZF)" is a statement in the metatheory that says that if ZF is inconsistent then ZFI is inconsistent. Yes, of course. > Of course, the proof of this in the > metatheory is trivial since all the axioms of ZF belong to ZFI. We > obtain the same result but with much less effort... Yes, that was exactly my point. > Perhaps what you learn from the proofs of |-_ZFI (A relativized to > V_i) for every axiom A of ZF is that ZF is interpretable in ZFI. This > looks a lot less trivial. As I recall, showing that one theory is interpretable in another theory shows relative consistency. But, in certain cases, we can also infer that it shows that one theory proves the consistency of the other theory. These are two related but different notions. If ZF is interpretable in ZFI, then the consistency of ZFI implies the consistency of ZF. but also In ZFI we may prove that ZF is consistent. (1) In ZF (quite personally I would say, a "higher copy" of ZF to serve as meta-theory, and same disclaimer throughout, but nevermind that unless it need be discussed) we can prove that ZF is interpretable in ZFI, thus that if ZFI is consistent then ZF is consistent (though that also follows trivially from the fact that ZF is a subtheory of ZFI). (2) In ZF (same disclaimer as above) we can prove (not trivially) that ZFI proves that ZF is consistent. And we should be careful not to conflate two related but different things: Interpeting one theory in another and relativizing axioms to a particluar class MoeBlee
From: Aatu Koskensilta on 11 Feb 2010 13:15 MoeBlee <jazzmobe(a)hotmail.com> writes: > As I recall, it's in Enderton's set theory book. If I'm not mistaken, > it's even a standard model (i.e. the symbol 'e' maps to the membership > relation on the universe) and consistency is proven by showing that > every axiom of ZF is true in the model <V_i membership-on-V_i>. But I > should doublecheck that. No need, if you'll take my word for it: in ZF(C) we can prove that all axioms of ZF(C) hold in <V_kappa, epsilon> for an inaccessible kappa. That is, the statement If kappa is inaccessible, <V_kappa, epsilon> |= A for all axioms A of ZF(C). is provable in ZF(C), and we do indeed find a proof in Enderton. It's probably not in Enderton, but we can also prove in ZF that If kappa is (weakly) inaccessible, <L_kappa, epsilon> |= A for all axioms of ZFC. where L_kappa is the kappa'th level of G�del's universe of constructible sets. > As I recall, showing that one theory is interpretable in another > theory shows relative consistency. Yep, since the interpretation of a contradiction is itself a contradiction. For theories T extending PA we also have: if T proves Con(S), S is interpretable in T. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on 11 Feb 2010 14:12 Marc Alcob� Garc�a <malcobe(a)gmail.com> writes: > So in the formal theory ZFI there must be a statement asserting the > consistency of ZF. I wonder how does that statement look like, because > ZFI talks about sets, and not about theories of sets... When we talk of ZF(I) proving this and that about formal theories we mean that, given some reasonable way of coding theories, formal sentences, and so on, as sets, the formalisation of the corresponding statement about sets is formally provable in ZF(I). Formal theories are not in any way special in this regard, and the same observation applies to theorems of number theory, analysis, what not. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Marc Alcobé García on 15 Feb 2010 15:52
> In Z (perforce in ZFI) we can formalize mathematical logic, including > formalizing consistency statements. This suggests a question: what necessary and sufficient condition must a theory meet to be able to formalize consistency statements in it? I think that to answer this question one must show that there is a formal theory T where one is able to define the notions of recursive or definable sets, of consistent sets of axioms, etc... Let me call that theory T a metatheory. I would expect a metatheory to be a theory where any other theory can be interpreted. Because interpretability is transitive, any theory that interprets a metatheory is also a metatheory. So, the original question becomes: how does one exactly show that a theory T is a metatheory? I think that Kunen tries to show that ZF is a metatheory in that sense in Ch. I §14. Appendix 3: Formalizing the metatheory. What he does is extend ZF by definitions with constant symbols that denote finitistic objects in the metatheory introducing Quine's corner notation. As customary, I have some trouble to follow him. Help in this respect would be welcome. > And we should be careful not to conflate two related but different > things: > > Interpeting one theory in another > and > relativizing axioms to a particluar class Formally, I see no difference, being the latter a particular case of the former. A class is but a unary predicate in an extension by definitions of the theory given by the axioms. |