Re: Some thoughts on formalization

[Calvin Ostrum <***>]

On 8/21/05, Tim Gwinn <***> wrote:

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

Because, as I told you quite a while ago, I would like to see a 
clear and rigorous formulation of Rosen's claims, shed of all the 
vagueness, grandiosity and (hopefully incidental) error, so 
that they can clearly be shown  to be right or 
wrong or trivial (my bet strongly being on the last
two, assuming, once again, there is some interpretation of it all
that actually arise above the "it's not even wrong" category).   
But since this group is dedicated primarily to hagiography,
shallow recycling of scripture, and bitter ranting against
reductionism, I guess I am going to have to work 
on this on my own.  Should I continue to waste my 
time on this, you can look at my formalization and clarification 
once it is fairly and carefully done, and should it turn out not in 
Rosen's favour, try to weasel your way out of it as you have been 
doing so far on everything else.
 
> 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.".

Uh, no.  The theorems of ZFC are effectively generated by an
algorithm.  If you don't know even this, your knowledge of basic
mathematics and mathematical logic seems hardly any better than
that of Judith "the yin-yang of infinite series" Rosen!   Or maybe
it's just a metaphor.