Prev: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent(EASY PROOF)
Next: prof. Charles N. Moore ?
From: Frederick Williams on 26 Jun 2010 11:26
Chris Menzel wrote:
>
> On Sat, 26 Jun 2010 01:17:17 +0000 (UTC), Chris Menzel
> <cmenzel(a)remove-this.tamu.edu> said:
> > On Fri, 25 Jun 2010 14:29:26 -0700 (PDT), George Greene
> > <greeneg(a)email.unc.edu> said:
> > ...
> >> on the grounds that one can prove "a certain sort of equivalence"
> >> between PA and ZF withOUT the axiom of infinity.
> >
> > Entirely true of course, but (as you explain quite clearly) that doesn't
> > make PA a *subset* of ZF. It only shows that there is a natural
> > embedding * of the language of PA into the language of ZF such that
> > PA |- A iff ZF |- A*.
>
> Whoops, that needs to be "such that, if PA |- A, then ZF |- A*". ZF,
> for example, proves Con(PA) which, of course, PA does not (assuming its
> consistency). The weaker (true) claim is all we need for the point:
>
> > Thus, we do have that {A* : PA |- A} is a subset of ZF. It is not
> > difficult to prove this, but it is far from trivial. Hence, even if
> > you understand the details (which I doubt very much Charlie does), to
> > express this fact as "PA is a subset of ZF" is, at best, misleading.
>
> I believe the false claim above holds if we replace ZF with ZF-Inf+~Inf.

Yes, it does. I think there's a proof in Wang's 'Logic, Computers,
Sets' but I don't have it readily to hand. I don't remember if the
theorem is due to Wang, or Lorenzen (or somebody).

--
I can't go on, I'll go on.
From: Frederick Williams on 27 Jun 2010 08:03
Frederick Williams wrote:
>
> Chris Menzel wrote:
> >
> > On Sat, 26 Jun 2010 01:17:17 +0000 (UTC), Chris Menzel
> > <cmenzel(a)remove-this.tamu.edu> said:
> > > On Fri, 25 Jun 2010 14:29:26 -0700 (PDT), George Greene
> > > <greeneg(a)email.unc.edu> said:
> > > ...
> > >> on the grounds that one can prove "a certain sort of equivalence"
> > >> between PA and ZF withOUT the axiom of infinity.
> > >
> > > Entirely true of course, but (as you explain quite clearly) that doesn't
> > > make PA a *subset* of ZF. It only shows that there is a natural
> > > embedding * of the language of PA into the language of ZF such that
> > > PA |- A iff ZF |- A*.
> >
> > Whoops, that needs to be "such that, if PA |- A, then ZF |- A*". ZF,
> > for example, proves Con(PA) which, of course, PA does not (assuming its
> > consistency). The weaker (true) claim is all we need for the point:
> >
> > > Thus, we do have that {A* : PA |- A} is a subset of ZF. It is not
> > > difficult to prove this, but it is far from trivial. Hence, even if
> > > you understand the details (which I doubt very much Charlie does), to
> > > express this fact as "PA is a subset of ZF" is, at best, misleading.
> >
> > I believe the false claim above holds if we replace ZF with ZF-Inf+~Inf.
>
> Yes, it does. I think there's a proof in Wang's 'Logic, Computers,
> Sets' but I don't have it readily to hand.

Having looked, I don't think it is in there. (Not that I've read it
cover to cover.)

--
I can't go on, I'll go on.
From: Frederick Williams on 29 Jun 2010 12:10
Chris Menzel wrote:

> [...] any such proof [of the consistency of PA], when formalized, will be in a
> system stronger than PA itself [...]

It seems to me that PA and a theory that proves its consistency can be
incomparable. Isn't this the case with PRA + induction up to epsilon_0?

--
I can't go on, I'll go on.
From: herbzet on 29 Jun 2010 21:54


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).

But what is a "metatheory", and specifically, what is "the metatheory
for the language of PA"?

--
hz
From: Frederick Williams on 30 Jun 2010 09:31
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.

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

Vol 48, 2007, updated here:

http://web.mat.bham.ac.uk/R.W.Kaye/papers/finitesettheory/

> discusses the mapping in detail. There's also an old paper by Hao Wang
> in which he discusses the construction but I can't lay my hands on it.

--
I can't go on, I'll go on.
 |  Next  |  Last
Pages: 1 2 3 4 5
Prev: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent(EASY PROOF)
Next: prof. Charles N. Moore ?