Prev: equivalence
Next: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent (EASY PROOF)
From: Charlie-Boo on 3 Jul 2010 07:22 On Jun 29, 10:16 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > Charlie-Boo <shymath...(a)gmail.com> writes: > > Ok. What is the reference to the proof in ZFC of PA consistency doing > > it that way? > > It's in Shelah's _Cardinal Arithmetic_ p.3245 - 4325238532. Basically, > you just do a triple-fold transfinite recursion over a coherent extender > sequence to obtain a suitable premouse, and iterate the upward Mostowski > collapsing lemma a few times. To remove the extendible cardinal > introduce some Aronszjan trees using Sacks forcing. Where's the part about how ZFC is used to do it? C-B > -- > Aatu Koskensilta (aatu.koskensi...(a)uta.fi) > > "Wovon man nicht sprechan kann, darüber muss man schweigen" > - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Charlie-Boo on 3 Jul 2010 07:26 On Jun 29, 9:16 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > billh04 <h...(a)tulane.edu> writes: > > Are you saying that it is a theorem of ZFC that PA is consistent? > > Sure. That is, the statement "PA is consistent" formalized in the > language of set theory as usual is formally derivable in ZFC (and No it isn't. PA can't do it and ZFC has nothing outside of PA relevant to the proof. Now, I refuted it - either prove it can be done, or refute my refutation, or retract the statment, ok? Isn't that how Mathematics works? C-B > already in much weaker theories). > > -- > Aatu Koskensilta (aatu.koskensi...(a)uta.fi) > > "Wovon man nicht sprechan kann, darüber muss man schweigen" > - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Charlie-Boo on 3 Jul 2010 07:28 On Jun 29, 9:13 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > Charlie-Boo <shymath...(a)gmail.com> writes: > > ZFC was designed to avoid paradoxes by making explicit what can be a > > set. It doesn't do anything else except what the Peano Axioms give > > it. > > Does PA give us Borel determinacy? Is Borel determinacy trivial? Prove ZFC can prove it and PA can't. C-B > -- > Aatu Koskensilta (aatu.koskensi...(a)uta.fi) > > "Wovon man nicht sprechan kann, darüber muss man schweigen" > - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Charlie-Boo on 3 Jul 2010 07:53 On Jun 29, 8:58 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > Charlie-Boo <shymath...(a)gmail.com> writes: > > How about when you said that Gentzen proved PA consistent using ZFC? > > No one ever proves anything using ZFC in the sense of producing formal > derivations. Rather, they prove mathematical theorems using mathematical > principles formalized in ZFC. By certain elementary considerations we > know the formalizations of such theorems are formally derivable in ZFC. How do you know that all of the logical argument can be formalized in ZFC? This is an example of what I call The Fallacy of the Famous Result. People will attribute special status to a result (rather than other similar results) whose only distinction is that it is famous. They are often famous because they were the first (seminal) result in a certain subject (e.g. a branch of Computer Science e.g. the Theory of Computation or Incompleteness in Logic.) But why does that argument not apply to the other results? Turings Halting Problem theorem proved for computers what Godels First Incompleteness theorem proved for logic. But these results were simply the first theorems discovered in their respective areas. It would be quite the coincidence if they were equivalent in some way that distinguishes them from other theorems, especially more general theorems discovered later (e.g. Rossers extension of Godels results.) Why is it Gödels theorem instead of Rossers theorem that is equivalent to Turings result? Because Godels is more famous and the author cant figure out Rossers. It has no simple This is unprovable. puzzle/joke/amusement to describe it that anyone can talk about. Gregory Chaitin never mentions Rossers stronger results. Its too complicated for him to understand. The recursion theorem proves/explains/formalizes Godels Incompleteness Theorem. Why doesnt it prove/explain/formalize Rossers theorem? Or does it explain EVERY theorem? And here we have the assertion that ZFC formalizes a proof of consistency of PA. There are a good dozen axiomatizations of set theory. Does ZFC2 (read: NF, NFU, CST, CZF, IZF etc.) formalize this argument? How about ZFC3 that has only one short axiom!? How do you know when an axiomatization of set theory has enough axioms to do the job? Or the right axioms to do the job? Without showing this specific proof being carried out in ZFC, how can you show properties capabilities of ZFC that are sure to include what is needed in this particular proof? The answer is, you cant. Unfortunately, even people like you who know the names of lots of theorems also tow the party line despite the fact that in all references given (Gentzen by Frederick Williams and Hinman by MoeBlee) there is no mention of any of ZFCs axioms anywhere in their proofs (including earlier results on which it relies) at all. Not just not all but none at all. C-B > -- > Aatu Koskensilta (aatu.koskensi...(a)uta.fi) > > "Wovon man nicht sprechan kann, darüber muss man schweigen" > - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Frederick Williams on 3 Jul 2010 08:48
Charlie-Boo wrote: > > On Jun 29, 10:16 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote: > > Charlie-Boo <shymath...(a)gmail.com> writes: > > > Ok. What is the reference to the proof in ZFC of PA consistency doing > > > it that way? > > > > It's in Shelah's _Cardinal Arithmetic_ p.3245 - 4325238532. Basically, > > you just do a triple-fold transfinite recursion over a coherent extender > > sequence to obtain a suitable premouse, and iterate the upward Mostowski > > collapsing lemma a few times. To remove the extendible cardinal > > introduce some Aronszjan trees using Sacks forcing. > > Where's the part about how ZFC is used to do it? Woosh. -- I can't go on, I'll go on. |