[FOM] Formalization Thesis

[Aatu Koskensilta]

Timothy Y. Chow wrote:
> (1) Is the Formalization Thesis, as I've formulated it, approximately as 
> precise as the Church-Turing Thesis?  If not, can the precision problem be 
> fixed easily with a simple rewording?

Not as far as I can see. To express the objection I and, I think, 
Torkel, presented when you proposed this thesis in sci.logic, succintly: 
the problem is that "correctly capturing" is not at all as clear and 
unambiguous notion as the notion of extensional equality for functions.

The post <slrnf6am4g.q15.aatu.koskensilta at localhost.localdomain> 
(http://groups.google.com/group/sci.logic/msg/1cf3026be617d644) might be 
of some relevance here. I write, in particular, that

> To recapitulate: a sentence P formalises, or expresses, a mathematical 
> statement if it's truth
> is equivalent to the statement using trivial mathematical reasoning, 
> and a
> formula R(x1, ..., xn) formalises, or expresses, a mathematical 
> relation P
> if it can be established, using trivial mathematical reasoning, that
> for all a1, ..., an R[num(a1)/x1, ..., num(an)/xn] is true iff P(a1, 
> ..., an). 

If we take "trivial mathematical reasoning" -- presumably reasoning 
formalisable in some weak base theory, perhaps determined by context -- 
modulo some coding, it seems very plausible that all statements of 
"ordinary mathematics" are expressible in the language of set theory in 
this sense; and if we take ordinary mathematical talk to be 
set-theoretical, all with presentations of this and that in terms of 
sets, we needn't even bother with coding. But it's a stretch to think of 
ordinary mathematical talk in terms of such a reduction, and then we 
need to consider all sorts of intensional questions, e.g. whether facts 
about the coding itself are relevant, etc.

-- 
Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus