[FOM] Formalization Thesis

[Timothy Y. Chow]

On Mon, 31 Dec 2007, catarina dutilh wrote:
> Something that seems to have gone a bit astray is the distinction 
> between *formulating* the Formalization Thesis or other Theses, and 
> *arguing* in its favor.

There is certainly a distinction; I don't believe that I lost sight of the 
distinction, so much as I pursued the discussion on both fronts at the 
same time (depending on who I was responding to).

> I, for one, have not had the intention of arguing pro or con FT, as I 
> think that a clear understanding of its content (and thus a sufficiently 
> precise formulation thereof) must come prior to defending or attacking 
> it.

I've thought a bit more about your distinction between ET and PT.  ET is 
originally how I thought I might phrase the Formalization Thesis, and 
something along the same lines was suggested by Joe Shipman.  In this way 
one sidesteps part of the Inexhaustibility Objection, because no 
particular set of axioms is chosen---only the language is.

However, I decided (at least preliminarily---maybe I could be convinced 
otherwise) against using ET as my basic formulation, for the following 
reason.  If we eschew all axioms and take just a first-order language with 
equality plus a binary relation symbol to be our "first-order language of 
set theory," then it seems somewhat dubious to me that formal sentences in 
such a language can "faithfully express" mathematical statements in 
anything like the desired sense.  Statements that are not *logically* 
equivalent, but that are equivalent only on the basis of a very weak 
fragment of ZFC, would not be equivalent if we do not lay down any axioms.  
For simple statements this might not be a big deal, but once you start 
trying to make nontrivial definitions, it becomes very awkward not to be 
able to assume (for example) that such-and-such a thing is *unique*.  
Unless we have structures have some minimal set-like behavior, I'm not 
sure I believe that the formal sentences are "expressing" the mathematical 
statements that they're trying to capture.

Perhaps the above worry is an unfounded one, but it's what has influenced 
me towards what you call an "instrumental" stance.  "Faithfully" just 
means "good enough," and the term "good enough" begs the question, "good 
enough for what purposes?"  Perfectly capturing the meaning seems 
hopeless, and so I focused on *provability*: "good enough" means "good 
enough so that for any correct informal proof, a corresponding correct 
formal proof can always be found."

As a cross-check, we can look back at the textbooks where authors often
(somewhat glibly) assert that such-and-such an argument can be seen to be 
formalizable in ZFC or whatnot, and what's important is that there is a 
formal version of the theorem that can be *proved* on the basis of a 
certain set of axioms.

> From all the discussions on this so far, I gather that it is 
> sufficiently clear to everyone that there is no formal method to perform 
> such a translation, that it is essentially a conceptual matter, which is 
> the point I was trying to bring up in the first place.

Yes, this is obviously true, as I said initially when explaining why I 
chose the word "Thesis."

> I suspect that certain moves that are allowed in mathematics would not 
> be allowed in the formal theory in question not only in the sense that 
> mathematics allows for direct jumps, but also in the sense that 
> different paths are required in the formalization.

I guess my concept of a formal proof faithfully representing an informal 
one requires only that any informal path from A to B can be mimicked by 
*some* formal path from A to B, not that the road taken must somehow 
correspond one-to-one at some microscopic level.

Tim