[FOM] Two remarks on the Formalization Thesis

[Timothy Y. Chow]

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 
reflection principle.

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.

Tim