Prev: since Physics has no numbers beyond 10^500, then that should be infinity for mathematics #622 Correcting Math
Next: A collatz-inequality related to the waring-problem; a further question
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
 | 
Pages: 1
Prev: since Physics has no numbers beyond 10^500, then that should be infinity for mathematics #622 Correcting Math
Next: A collatz-inequality related to the waring-problem; a further question