Re: Some thoughts on formalization

[Calvin Ostrum <***>]

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

> To summarize, I do not think that Rosen has made any comments with respect
> to this topic which are either misleading or not factual. Nor do his
> comments seem to me to be at all controversial. 

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

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. 

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

But in that case, he is very misleading, at least to me,
since in all his fulminations about Goedel's theorem and
the like, I can't find one place where he makes this
anywhere near explicit.   In fact, he constantly talks
about algorithms and computability, and how the items
of a formal system are generable by a set of
finite rules applied mechanically.  I cannot find one
place where instead of *computability*, he talks 
about *decidability*.  If there are such places, they
are rare.

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

There is no mention or inclusion of a decision 
procedure for theoremhood here.   It is only 
required for formalization that the theorems be 
effectively  generated by an algorithm, as indeed 
they are in PA and ZFC.  Indeed "expressed" 
above I take to be essentially the same as
"captured" as it has been used here and in 
Rosen.  

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.  But of course there
is no question of a decision procedure in
this case, and moreover, the model is
certain nowhere near "finitistic" in the
sense desired by Hilbert.

I could give many other passages where
similar things are said.  For example, in
"On the philosophy of craft", p305.  But
I think the negative point has been very clearly
made.

Let's try again for a positive point.  Let's compare
Rosen, the Newton of Biology, to Goedel, Church,
and Turing in regards to their common area of
concern, that of computability, decidability, and
the like.

Turing proved a given problem to be undecidable,
after rigorously defining that problem:  H(X) = "1 if
Turing machine X of no inputs halts, 0 otherwise".
Technically, he showed the problem to be semi-
decidable.  (i.e., the set of X such that H(X)=1 is 
enumerable)

Church proved a given problem to be undecidable
after rigorously defining that problem: P(X) = "1 if
X is a theorem of the predicate calculus, 0 otherwise"
Again, he showed the problem to be semi-decidable.

Goedel proved a given problem to be undecidable
after rigorously defining that problem T(X) = "1 if
X is a truth of arithmetic, 0 otherwise".   He
showed that the problem was not even semi-decidable.

Rosen has alleged that certain functions necessary to
model biological systems are undecidable and not
even semi-decidable).  But what precisely are 
these functions?   Where precidely are they
defined.   Why can't they be given a simple and
rigorous definition in the same way that Turing, 
Church, and Goedel have done?  Forget trying
to prove it, let's just have the rigorous definition.

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?