From: Aatu Koskensilta on 1 Jul 2010 00:17 Charlie-Boo <shymathguy(a)gmail.com> writes: > If so, what is the formal expression in ZFC that PA is consistent? On any scheme for expressing such statements in the unextended language of set theory it's a virtually incomprehensible string of symbols. If you really want to have a look, go through a set theory text and write a computer program to output it for you. Why would you want to see it in the first place? -- 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 1 Jul 2010 02:04 Charlie-Boo <shymathguy(a)gmail.com> writes: > To see it means to have actually created it, and its actual creation > would answer the very interesting question of whether ZFC can prove > that PA is consistent even though PA can't. We already know the answer. The axioms used in the proof are a restricted form of comprehension, infinity, union and pairing. Spelling out the formalization of "PA is consistent" in the language of set theory would be a tedious, trivial and pointless undertaking, of no apparent mathematical interest whatsoever. > It would substantiate your assertions. Is that of value? Well, no. I can't think of any pressing reason I should want to convince you of anything. -- 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 1 Jul 2010 02:45 Ki Song <kiwisquash(a)gmail.com> writes: > Perhaps an analogy is in order! > > I feel like what Charlie-Boo is asking people to do is analogous to > asking someone to perform the addition: > > Sqrt{2}+Sqrt{3}, with a decimal precision of 10^(10^(10^100)) place. The analogy is apt, but it's not really quite that bad. Based on nothing at all I'd estimate that a formalization of "PA is consistent", fully spelled-out in the language of set theory, fits in less than ten pages. But perhaps you were thinking of Bourbaki, whose term for the number 1 already consists of 4,523,659,424,929 symbols and 1,179,618,517,981 disambiguatory links? -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Jesse F. Hughes on 1 Jul 2010 08:33 billh04 <hale(a)tulane.edu> writes: >> > Theorem. (all x in N)(all y in N)(if S x = S y then x = y) >> >> > Here N is a set (defined as mentioned before). >> > Here x and y are sets since everything in ZFC is a set. >> > Here S is a set (the successor function). >> > Thus, the theorem is a statement about sets. >> > ZFC can proves statements about sets using the ZFC axioms. >> >> > Why do you think this theorem cannot be proved using the ZFC axioms? >> >> If it could be done without the axiom of infinity, then the axiom of >> infinity wouldn't be needed in ZFC. Maybe it is, but I doubt that. > > But the axiom of infinity is a ZFC axiom. So, I am allowed to use it > in proving a theorem in ZFC. In fact, the use of infinity for this particular theorem is trivial indeed. ZFC proves (Ax)(Ay)( Sx = Sy -> x = y ). To prove (Ax in N)(Ay in N)( Sx = Sy -> x = y ), we need merely add a definition of N to ZFC. The axiom of infinity is used to show that there is a unique set satisfying certain conditions and we define N to be that set[1]. But the properties of that set are literally irrelevant to this particular proof. Footnotes: [1] Yes, Charlie, by *adding* an axiom to ZFC, resulting in a conservative extension, but this is only a nicety. We could prove a theorem with the same content without adding the definition. Suppose our defining axiom is P(x), so that our definition of N is the axiom P(N). Now, ZFC proves (Ex)(Px & (Ay)(Py -> y=x)). So, the statement (Ax in N)(Ay in N)( Sx = Sy -> x = y ) means the same thing as (Ew)(Pw & (Ax in w)(Ay in w)( Sx = Sy -> x = y )). -- Jesse F. Hughes "How lucky we are to be able to hear how miserable Willie Nelson could imagine himself to be." -- Ken Tucker on Fresh Air
From: Alan Smaill on 1 Jul 2010 09:31
Charlie-Boo <shymathguy(a)gmail.com> writes: > On Jun 29, 5:28�pm, MoeBlee <jazzm...(a)hotmail.com> wrote: >> On Jun 29, 4:23�pm, Transfer Principle <lwal...(a)lausd.net> wrote: >> >> > I'm not skeptical (in the way that Charlie-Boo is skeptical) about >> > the provability of Con(PA) in either ZFC or PRA+epsilon_0. But I >> > am suspicious of the fact that the induction needs only to be >> > taken up to epsilon_0, >> >> As to ZFC, you don't need such fancy stuff as epsilon_0. Just do the >> routine proof that with the system of omega with 0, successor, >> addition, and multiplication we get a model of all the PA axioms. > > The problem isn't to conclude that a model exists, using ZFC. The > problem is to prove that PA is consistent, using ZFC. If you admit that ZF can express "structure S is a model for theory T", then have a go at working out how the provable existence of a model shows consistency. Hint: a semantic definition of consistency of T is that there is no formula P such that P and ~P are logical consequences of T. Hint: recall the definition of satisfaction of a negated formula in a structure. Hint: try using FOL. Is that enough hints? > C-B > >> MoeBlee > -- Alan Smaill |