Prev: JSH: Integer factorization IS the short-cut
Next: Such a surreal thing
From: Chris Menzel on 30 Jun 2010 00:29
On Tue, 29 Jun 2010 21:54:50 -0400, herbzet <herbzet(a)gmail.com> said:
> Chris Menzel wrote:
>> billh04 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.

From: herbzet on 30 Jun 2010 18:26


Chris Menzel wrote:
> herbzet said:
> > Chris Menzel wrote:
> >> billh04 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.

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 theorem of ZF.

--
hz
From: Chris Menzel on 2 Jul 2010 05:08
On Wed, 30 Jun 2010 14:31:26 +0100, Frederick Williams
<frederick.williams2(a)tesco.net> said:
> Chris Menzel wrote:
>
>>
>> Hm, don't really know of any books. There's a recent article by Kaye
>> and Wang called "On Interpretations of Arithmetic and Set Theory" that
>
> Wong. It would be quite w(r)ong of you to get your Wongs and Wangs
> mixed up.

Indeed, good catch. It would have been a miracle from beyond the grave
had Wang been the co-author!

>> occurred in 2007 or 2008 in the Notre Dame Journal of Formal Logic that

I meant "appeared".

> Vol 48, 2007, updated here:
>
> http://web.mat.bham.ac.uk/R.W.Kaye/papers/finitesettheory/

Nice.

 | 
Pages: 1
Prev: JSH: Integer factorization IS the short-cut
Next: Such a surreal thing