[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Mon Dec 31 11:29:12 EST 2007
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
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.
More information about the FOM