[FOM] Formalization Thesis

[William Tait]

One challenge to the Formalization Thesis, or maybe better, to a  
satisfactory formulation of it, arises from the 'reduction to sets' of  
various types of objects: ordered pairs, functions, ordinal numbers,  
cardinal numbers, real numbers, etc. In each case, the reduction adds  
structure to the type that is not part of its real meaning. In fact,  
this was Dedekind's challenge. (And, as Benacerraf pointed out, there  
is in general some arbitrariness about what structure is added.)

Timothy, this may not be the direction in which you want the  
discussion of the FT to go, but I would be interested in reading  
responses to it.

Best wishes for the New Year to All,

Bill Tait

On Dec 26, 2007, at 11:40 AM, Timothy Y. Chow wrote:

> In 2005, I started a thread entitled "Formal sentences capture  
> informal
> ones" in the USENET newsgroup sci.logic, with the suggestion that the
> following statement, or something like it, should be given a name--- 
> e.g.,
> "the Formalization Thesis":
>
>   Every theorem of ordinary mathematics is faithfully expressed by a
>   formal theorem of ZFC.
>
> Here, my focus is not so much on ZFC particularly; that is, I will not
> quibble with someone who wishes to replace "ZFC" with another system  
> that
> is somewhat weaker or stronger.  I am also not focusing on theorems,  
> in
> contradistinction to definitions or conjectures or proofs; indeed, I  
> *do*
> want to include these things, and I chose "theorems" above only  
> because it
> makes for a snappier statement (e.g., the term "formal conjecture of  
> ZFC"
> is not standard, and would require some explanation).  What I am  
> focusing
> on is the notion that formal sentences "correctly capture"  
> statements of
> mathematics that are made informally in natural language.
>
> I use the word "Thesis," as the Formalization Thesis is reminiscent  
> of the
> Church-Turing Thesis, which also equates an informal notion  
> ("effective
> procedure" or "algorithm") with a formal one.  The Formalization  
> Thesis is
> often tacitly invoked in much the same way that the Church-Turing  
> Thesis
> is sometimes invoked.  That is, authors often give informal proofs and
> then make a claim of the form, "It is clear that the above argument  
> can be
> converted into a formal proof in such-and-such a system," relying on  
> the
> reader's "experience" in formalizing informal mathematics to avoid
> explicitly writing down a very long and tedious verification.   
> Similarly,
> authors often describe algorithms informally, relying on the reader's
> programming experience to avoid writing down a long piece of code in a
> machine-readable programming language.
>
> I advocate giving a *name* to the Formalization Thesis because I  
> believe
> that doing so would be a valuable expository move.  For example,  
> there has
> been some discussion in the literature (e.g., by Detlefsen I think)  
> about
> whether Hilbert's program can still be salvaged in the light of  
> Goedel's
> second theorem.  The debate, as I understand it, centers on a  
> particular
> instance of the Formalization Thesis, namely whether the formal  
> sentence
> Con(PA) (in any one of its usual incarnations) correctly captures the
> meaning of the statement "PA is consistent."  Giving the Formalization
> Thesis a name seems to me to allow the arguments on both sides of this
> debate to be formulated with greater succinctness and clarity than is
> currently the case.
>
> I also think that giving the Formalization Thesis a name would have  
> helped
> me when first studying Kunen's set theory textbook, especially when  
> I was
> trying to understand what he meant by a "reasonable" representing  
> formula
> and when I was studying the proof of the reflection theorem for ZFC.
>
> In the aforementioned sci.logic thread, Torkel Franzen and Aatu
> Koskensilta raised some objections.  Rereading the discussion now, I
> confess that I still do not fully understand the objection, but it is
> something to the effect that the Formalization Thesis as I stated it  
> was
> not sufficiently precise to be of any value.  I would therefore like  
> to
> ask FOM readers:
>
> (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?
>
> (2) Assuming that the answer to (1) is yes, does it seem useful,  
> from a
> pedagogical and expository point of view, to give the Formalization  
> Thesis
> a name?
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom