Prev: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent(EASY PROOF)
Next: Herc does not understand any induction schema
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. |