[FOM] Two remarks on the Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Thu Jan 10 22:46:02 EST 2008
There are two remarks about the Formalization Thesis that I want to make
in light of the excellent feedback from FOMers.
First, the objection that I neglected non-classical logic is well taken.
I did not have non-classical logic in mind at first, and it is pretty
clear (at least to me) that the Formalization Thesis as I stated it fails
for non-classical logic. We can try to "fake" a theorem T of (say) IZF by
using "T is an intuitionistic theorem of IZF" as a surrogate for T itself,
but this doesn't quite work: Mizar can verify that "T is an intuitionistic
theorem of IZF" is a theorem of ZFC, but this falls short of a mechanical
verification that T is an intuitionistic theorem of IZF. Even classically,
we can't pass from theoremhood in ZFC to "truth" without some kind of
So all my comments about the Formalization Thesis should be taken with the
implicit background assumption of classical logic. By saying this, I am
not denying the importance of non-classical logic, but am restricting
myself to classical logic for expository simplicity.
The second remark is that I now see that the Formalization Thesis as I
stated it conflates two things: the relationship between formal and
informal on the one hand, and the relationship between set theory and the
rest of mathematics on the other hand. Probably these two ingredients
should be disentangled. I am not going to attempt to do so right now, but
as an illustration of the distinction, I note that Sazonov argues for a
view of mathematics in which the Formalization Thesis is vacuously true.
Implicitly, Sazonov is focusing only on the part of the Formalization
Thesis that talks about formal vs. informal, because even on Sazonov's
view, the notion that all (or most) branches of mathematics can be
"reduced" to set theory is not vacuously true.
More information about the FOM