[FOM] Formalization Thesis

[catarina dutilh]

The problem with the Formalization Thesis thus stated is, I think, the difficulties concerning the phrase " is faithfully expressed". What exactly does it mean, to express faithfully? Such a transformation from 'informal' theorems of mathematics into 'formal' theorems of ZFC or the like is in fact a kind of translation from one language into another (I'd be interested in hearing from people who disagree with this claim). Now, as widely discussed within the philosophy of language (e.g. Quine's Gavagai example), accuracy of translation is far from being a straightforward, objective matter; I think the same applies to translations such as those that would verify the Formalization Thesis.
 
The point raised by Bill Tait is one of the issues that would arise in translating ordinary mathematical theorems into formal set-theory: the fact that content that is not part of the original statements seems to 'sneak in', namely the reduction of all kinds of mathematical entities to sets. Quoting Tait, "the reduction adds structure to the type that is not part of its real *meaning*" (my emphasis). It seems to me that a wide array of similar 'translation' problems would arise.
 
Moreover, even if we accept that a given expression of an ordinary mathematical theorem by means of a formal set-theoretical theorem is faithful, it is very likely that there would be more than one such 'faithful expressions' of the same original mathematical theorem. In other words, this relation of 'faithful expression' would, or so it seems to me, be a one-many relation. This may or may not be a problem, depending on the moral one wishes to extract from the Formalization Thesis.
 
So, unless one can make sense of the idea of 'expressing faithfully' in a precise way, the Formalization Thesis thus stated does not seem to be sufficiently precise. This said, I find the *attempt* to give a precise formulation to the idea of (all of) ordinary mathematical theorems corresponding in some sense or another to theorems of formal set-theory extremely important and interesting; so thanks, Timothy, for raising this discussion.
 
Best,
 
Catarina


----- Original Message ---- 
From: William Tait <williamtait at mac.com> 
To: tchow at alum.mit.edu; Foundations of Mathematics <fom at cs.nyu.edu> 
Cc: William Tait <williamtait at mac.com> 
Sent: Wednesday, December 26, 2007 10:35:50 PM 
Subject: Re: [FOM] Formalization Thesis 

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 

_______________________________________________ 
FOM mailing list 
FOM at cs.nyu.edu 
http://www.cs.nyu.edu/mailman/listinfo/fom


      ____________________________________________________________________________________
Never miss a thing.  Make Yahoo your home page. 
http://www.yahoo.com/r/hs