Re: Name the thesis: "Formal sentences capture informal ones"

tchow_at_lsa.umich.edu
Date: 01/30/05 

Date: 30 Jan 2005 21:53:56 GMT

In article <ctid7v$dus$1@phys-news1.kolumbus.fi>,
Aatu Koskensilta <aatu.koskensilta@xortec.fi> wrote:
>tchow@lsa.umich.edu wrote:
>> (*) Intension-preserving formalization of informal mathematical
>> statements is always possible.
>>
>> (+) Con("PA") is an intension-preserving formalization of "PA is
>> consistent."
>
>But (+) isn't an instance of (*).

Right, that's what I meant by "abusing the term `schema.'" What I want
is probably neither (*) nor (+) but some schema of which (+) will be an
instance.

>For example, how do we know that Con("PA") - expressed in what ever way
>- instead of the myriard other possible arithmetical sentences is the
>formal counterpart of "PA is consistent"?

I don't see why this is relevant. I am not concerned with saying that
Con("PA") is *the* formalization of "PA is consistent"; indeed, that is
surely totally false. I only want to say that it is *an* acceptable
formalization.

>The point I'm trying to make here is that in order to
>instantiate (*) to get something like (+) for a particular mathematical
>statement P we would need to know what formal sentence is the
>intension-preserving formalization of P. This in turn requires that the
>notion of "intension-preserving formalization" is explicated in an
>informative, hopefully mathematical, way.

As I understand it, this is precisely the kind of project that Sol Feferman
undertook in his early years. He made a number of striking contributions,
which I have not taken the time to understand fully. However, I think I
understand enough of the issues involved to say something about the idea of
explicating "intension-preserving" in a mathematical way.

Let me first refer you to my article `What makes a representing formula
"reasonable"?' that I posted to sci.logic on Dec 12 2002. (You can find
it on Google Groups; I'd give the URL, but Google currently has an annoying
beta version whose URL's are ephemeral.) Even something as simple as
"x is even" admits deviant formalizations. One might then ask, is there
a way to say precisely what a "normal" or "intension-preserving"
formalization of "x is even" is? I asked this question of Ken Kunen
and he replied as follows (I believe he would not mind my quoting his
email here):

:This depends on what your framework is.
:If you are thinking of "x is even" as an informal concept defined in
:the metatheory, then there is no way to say formally what the
:correct expression is for "x is even" within ZF, since you don't
:have a formal definition of "x is even" to start with.
:
:On the other hand, you might think of the metatheory itself as
:a formal system, such as PRA (primitive recursive arithmetic).
:Then, one can formally define a map from PRA formulas into ZFC
:so that every theorem of PRA maps into a theorem of ZFC.
:Of course, you are just pushing the problem back one step.
:You would still have to argue informally that the standard
:primitive recursive definition of "x is even" captures
:the informal notion of "even".

I think what Kunen's remarks indicate is that there is no way out of
the infinite regress other than by starting with an informal-to-formal
transition somewhere and then baldly postulating that it is correct.
This, to me, is reminiscent of the Church-Turing thesis.

Furthermore, there is no doubt in anyone's mind that, for example, the
standard primitive recursive definition of "x is even" correctly captures
the informal notion of "even." So I don't think that the difficulty of
formulating precisely what "intension-preserving" means should lead us
to worry that my proposed thesis, when formulated properly, is not worthy
of trust.

>But even this thesis is problematic. What sort of consistency are we
>talking here? Herbrand consistency? Hilbert consistency? Or are these
>irrelevant and are we assuming some background theory in respect to
>which various formalizations are found to be equivalent? And how do we
>know that Con_phi "intension-preservingly" expressed the consistency of
>the theory defined by phi? What if it just expresses this in a
>non-intension-preserving way?

I would repeat what I said to Torkel Franzen, that I think these are good
questions, but that they shouldn't make us doubt that certain instances of
the thesis that I'm groping towards are meaningful and widely accepted,
nor should it make us doubt that the thesis is too vague to be formulated
properly. In fact, I'm encouraged that my attempt to state the thesis is
provoking exactly the kinds of questions that I think it ought to provoke,
providing a basis for which to examine them. 

-- 
Tim Chow       tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth.  ---Galileo, Dialogues Concerning Two New Sciences

Relevant Pages