Re: Some thoughts on formalization

[Tim Gwinn <***>]

Calvin,

I admit I wondered why you stayed, when you were so adamantly certain that
Rosen was misleading and nonfactual on so many points.

I daresay it is you who are grasping at straws in your comments below. :)

Oh yes, I forgot to mention this in my previous post -- you might recall
that in ZFC, the Axiom of Choice (the "C" in "ZFC") is not effective. The
Axiom of Choice specifies that a choice function exists, however it does not
provide an effective procedure for selecting it. In this manner, ZFC does
not even meet your restricted definition of "formalization" in your previous
post, to wit, "It is only required for formalization that the theorems be
effectively  generated by an algorithm, as indeed they are in PA and ZFC.".

Regards,
Tim

> -----Original Message-----
> From: ROSEN Forum [mailto:*** Behalf Of Calvin
> Ostrum
> Sent: Sunday, August 21, 2005 8:27 PM
> To: ***
> Subject: Re: Some thoughts on formalization
>
>
> On 8/21/05, Tim Gwinn <***> wrote:
>
> Wow, I give up.  Obviously I am not as fast a learner as Torkel
> is.  Or Glen, who before leaving noted the similarity of Rosen
> disciples to Randoids.
>
> Just to take one example:
>
> > > In fact, on the very page you cite, Rosen quotes Kleene
> > > as giving an adequate characterization of the
> > > notion of formalizability he is concerned with:
> > >
> > > "[Formalization [Rosen's interpolation]] will not be
> > > finished until all the properties of undefined terms
> > > which matter for the deduction of theorems have
> > > been expressed by axioms".
> >
> > TG: Again, you misstate the facts. Rosen does NOT quote "Kleene
> as giving an
> > adequate characterization of the notion of formalizability he
> is concerned
> > with", nor is that the full quoted text. Instead Rosen says, "The best
> > statement I have seen regarding the formalistic program is that given by
> > Kleene; it does no harm to quote it again:".[LI p.6]
>
> You are truly grasping at straws.  Rosen gives Kleene's
> quote, with it referring to "formalization", right after he uses his
> own sense of the term, and right after talking about Goedel's
> constructible hierarchy.
>
> He then goes on immediately, on the page you cited, to say
>
> "The status of all these formalizations [thus even including
> Goedel's constructible hierarchy] is informative.  They turn out
> to be infinitely feeble compared with the original mathematical
> systems they attempted to objective.  Indeed, these attempts
> to secure  mathematics from paradox by invoking constructibility,
> [again, referring clearly to Goedel's constructable hierarchy]
> or formalizability,  end up by losing most of it"
>
> To make clear he is also including something that goes
> well beyond Hilbert and totally decidable systems, he then
> once again says
>
> "In other words, a "constructible universe" is at best only
> an infinitesimal fragment of "mathematical reality"".
>
> That can only be a reference, in this context, to the phrase
> "constructible universe" (and its subsequent abuse) used
> a few paragraphs previously in reference to Goedel's
> constructible hierarchy.