Re: Some thoughts on formalization

[Tim Gwinn <***>]

Calvin,

> I think it is quite clear that Rosen is either misleading or
> nonfactual in what he says on these issues.   We have already
> seen how things he says about impredicativity are either
> misleading or nonfactual, for example.


TG: I leave the topic of 'impredicativity' for another day. To be sure, I
find you claim here incorrect.


>   Your own post here
> shows that his discussion is misleading, in that rather than
> accept PA and ZFC as formal in the relevant sense as other
> attempts to defend him have done (thus being reduced
> to employing such meaningless slogans as "creativity
> is impredicative") you take the entirely different route
> of disparaging such systems as not being adequately
> formal.


TG: Calvin, I hardly consider it "disparaging" to say that PA or ZFC are not
formalizable in the sense of Hilbert's formalist program. Quite the
contrary, I said of ZFC/PA that: "This has intrinsic interest, to be sure,
however it does not bear at all on the question Rosen was interested in...".
That is hardly disparaging. You seem to be equating 'formal' with
'formalization'. All of mathematics is formal. Please specify precisely what
you mean by "formal in the relevant sense". What sense is that?


> I suppose it is possible that Rosen all along meant to
> exclude such systems, and instead, refer to a much
> more limited class of system which he has nowhere
> rigorously specified.   It appears that what you claim is
> meant by "formal", then, is systems which have an
> effective decision procedure, as opposed merely
> to systems all of whose results can be proven formally.


TG: Again, my post was about *formalization* in the sense of Hilbert's
formalist program, not formal systems generally. Equating 'formalization'
and 'formal' is patently incorrect. Likewise, as I mentioned, in discussing
'formalization', Rosen repeatedly referred specifically to Hilbert's
formalist program when mentioning formalization. It is simply false that "he
has nowhere rigorously specified" this.


> Now, if this is truly what is meant by formal in Rosen-speak,
> then Rosen is indeed correct (in a vague but perfectly
> acceptable sense) that formal systems only
> capture an infinitesimal amount of "real mathematics".

TG: That is an flatly incorrect statement of Rosen's remarks. He stated that
*formalizations* (again, in the sense of Hilbert's formalist program) only
capture an infinitesimal fragment of "mathematical reality". [EL p. 92] You
are consistently confusing 'formal' with 'formalization'.

<snip>

> 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]


> There is no mention or inclusion of a decision
> procedure for theoremhood here.


TG: The quote was *not* intended as a comprehensive description of the
details of formalization.


>  It is only
> required for formalization that the theorems be
> effectively  generated by an algorithm, as indeed
> they are in PA and ZFC.

TG: According to whom? That is not Hilbert's sense of the word
'formalization', and thus is irrelevant to this discussion.

<snip>

> On the very same page (the quotation spans
> two pages) Rosen is again misleading in talking
> about Goedel's constructible universe in a
> disparaging manner ("machine like",
> "algorithmically generated") as if it fits his
> criterion of formality.


TG: Apparently, then you also must think Kleene and Simpson are disparaging
in their characterization of formalization.


<snip>


> Rosen has alleged that certain functions necessary to
> model biological systems are undecidable and not
> even semi-decidable).

TG: Please provide a specific quote or reference, and we can discuss this.

> And how is this for just one example of "misleading"?
> As early as page five in Life Itself, we find claims such
> as "Mathematics over the past century has given little
> evidence that it is concerned with eternal, timeless,
> and hence unarguable truth".   Aside from confusing
> metaphysics with epistemology (there is no reason that
> eternal and timeless truth is going to be "unarguable"),
> this is misleading and arguably insulting.   Mathematics
> of course, has no concern and supplies no evidence.
> It is mathematicians who do this.   What is Rosen's
> own evidence for this generic attack upon
> mathematicians?

TG: This single sentence, pulled out of context of the discussion of p. 4-6,
does not even rise to the level of an argument.

Regards,
Tim