How Can ZFC/PA do much of Math - it Can't Even ProvePAisConsistent (EASY PROOF)
in [Logic]
|
Prev: since Physics has no numbers beyond 10^500, then that should be infinity for mathematics #622 Correcting Math
Next: New maths formula, maths 2&3^(a->38^7839_88)-34 MATHS 3+4=4 sin(x)=oo
From: Chris Menzel on 2 Jul 2010 05:06 On Wed, 30 Jun 2010 18:26:43 -0400, herbzet <herbzet(a)gmail.com> said: >> > ... >> >> > I thought that the proof of consistency of PA relative to ZFC by >> >> > showing that there is a model of PA in ZFC was a metatheorem, not a >> >> > theorem stated in ZFC and proved using the axioms of ZFC. >> >> >> >> You can formalize the metatheory for the language of PA in ZF and >> >> prove in ZF the existence of a model of PA and, hence, that PA is >> >> consistent, by the soundness theorem. >> > >> > I take it that "a metatheorem" is a theorem *about* a formal theory >> > T rather than a theorem *of* T (although of course these are not >> > mutually exclusive categories). >> >> Sounds about right. >> >> > But what is a "metatheory", and specifically, what is "the >> > metatheory for the language of PA"? >> >> The theory (well, a theory) that explicitly lays out the language of >> PA, the semantics of the language, a proof theory, the axioms of PA, >> along with relevant metatheorems, e.g., the soundness and >> completeness of the proof theory relative to the semantics. > > Ok -- I'm getting that the "metatheory" is stuff that is "outside of" > (and indeed prior to the description of) the formal system of PA. Yes, except I'd delete that qualification inside the parens -- I'm not sure what else you could mean by the description of PA other than its language, axioms, etc, which are all part of its metatheory. > And so one is to "formalize the metatheory for the language of PA in > ZF" (the said metatheory including a semantics for PA), and then show > in ZF that the formally described semantics exist, i.e., that PA has a > model in ZF. > > So the metatheorem (of PA) that there exists a model of PA in ZFC is > transformed into a theorem of ZF. Well, except for the reference to there ZFC; what we've been talking about is formalizing the proof of the proposition "PA has a model" in ZF. "ZFC proves that PA has a model" is a rather different proposition -- though, in fact, one that can also be formalized as a theorem of ZF, in virtue of the general fact that if ZF proves A, then ZF proves "ZF proves A" (and, hence, "ZFC proves A").
From: herbzet on 3 Jul 2010 01:58
Chris Menzel wrote: > herbzet said: > >> > ... > >> >> > I thought that the proof of consistency of PA relative to ZFC by > >> >> > showing that there is a model of PA in ZFC was a metatheorem, not a > >> >> > theorem stated in ZFC and proved using the axioms of ZFC. > >> >> > >> >> You can formalize the metatheory for the language of PA in ZF and > >> >> prove in ZF the existence of a model of PA and, hence, that PA is > >> >> consistent, by the soundness theorem. > >> > > >> > I take it that "a metatheorem" is a theorem *about* a formal theory > >> > T rather than a theorem *of* T (although of course these are not > >> > mutually exclusive categories). > >> > >> Sounds about right. > >> > >> > But what is a "metatheory", and specifically, what is "the > >> > metatheory for the language of PA"? > >> > >> The theory (well, a theory) that explicitly lays out the language of > >> PA, the semantics of the language, a proof theory, the axioms of PA, > >> along with relevant metatheorems, e.g., the soundness and > >> completeness of the proof theory relative to the semantics. > > > > Ok -- I'm getting that the "metatheory" is stuff that is "outside of" > > (and indeed prior to the description of) the formal system of PA. > > Yes, except I'd delete that qualification inside the parens -- I'm not > sure what else you could mean by the description of PA other than its > language, axioms, etc, which are all part of its metatheory. > > > And so one is to "formalize the metatheory for the language of PA in > > ZF" (the said metatheory including a semantics for PA), and then show > > in ZF that the formally described semantics exist, i.e., that PA has a > > model in ZF. > > > > So the metatheorem (of PA) that there exists a model of PA in ZFC is > > transformed into a theorem of ZF. > > Well, except for the reference to there ZFC; what we've been talking > about is formalizing the proof of the proposition "PA has a model" in > ZF. "ZFC proves that PA has a model" is a rather different proposition > -- though, in fact, one that can also be formalized as a theorem of ZF, > in virtue of the general fact that if ZF proves A, then ZF proves "ZF > proves A" (and, hence, "ZFC proves A"). Ok, yeah, good. -- hz |