[FOM] Formalization Thesis

[Timothy Y. Chow]

On Fri, 28 Dec 2007, catarina dutilh wrote:
> Expressibility Thesis (ET): Every theorem of ordinary mathematics is 
> faithfully expressed in the language of ZFC (or the appropriate formal 
> language).
[...]
> the verification of ET would require that the translation of every 
> theorem of ordinary mathematics into a formal language must be performed 
> on a one-by-one basis.  Also, I suspect that this is not an objective 
> matter: there would probably be disagreement as to whether statement T' 
> in the language of ZFC (or other) is or is not a faithful translation of 
> theorem T of ordinary mathematics.

Your prediction is an extremely interesting one to me, because it is not 
merely an academic one.  The project of translating every theorem of 
ordinary mathematics one by one into a formal language is being carried 
out as we speak.  I already mentioned a couple of examples, and there are 
others (e.g., Gonthier's project to formalize the Feit-Thompson odd-order 
theorem in COQ).  There are various well-known objections to such 
projects, e.g., the kernel of the proof-verification software could have a 
bug in it.  However, your remark here hints at an entirely different 
objection.  Suppose Hales completes his Flyspeck project.  One could 
potentially dismiss the entire project by saying, "What you have formally 
verified is not the Kepler conjecture at all, but something entirely 
different statement."

In practice, there does not seem to have been any kind of substantive 
disagreement of this type.  That could be because the field of 
machine-checkable proofs is still in its infancy, and not enough people 
have scrutinized it yet.  It would be very surprising to me, however, if 
fundamental disagreements were to arise about the faithfulness of the 
translation process.

It is true that, machine-checkable proofs aside, disagreements do exist in 
mathematics about the precise statements of certain theorems.  For 
example, the term "fundamental theorem of calculus" is known to every 
mathematician, but if you picked two mathematicians at random and asked 
them separately to write down its precise statement, chances are that they 
would differ.  (Riemann integral or Lebesgue integral?  Nice functions 
only or semi-pathological ones too?)  However, it seems to me that 
formalization would *clarify* such disagreements, not introduce new ones.  
That is, the process of formalization would force people to articulate 
exactly what version of a theorem they mean.  You might generate multiple 
versions of a theorem in the process, but I would be surprised if you got 
disagreements of the form, "Mathematician A believes that informal theorem 
T corresponds to formal theorem T_A while mathematician B believes that 
informal theorem T corresponds to formal theorem T_B, and their 
disagreement is irreconcilable."  Instead, I would expect that 
mathematicians A and B would come to agree that there are *two* distinct 
theorems, one of which corresponds to formal theorem T_A and the other of 
which corresponds to formal theorem T_B.  The Expressibility Thesis would 
not be undermined.

> my guess is that any experienced logician can give counterexamples to 
> this equivalence, i.e. proofs that are valid within ordinary mathematics 
> but which do not correspond to valid proofs in the formal language, even 
> assuming that ET and PT hold of the theorems in question.

This would be even more startling to me.  Here is an informal argument why 
this should not be the case.  A proof valid within ordinary mathematics 
would establish that theorem T is a correct logical consequence of the 
axioms A.  But the completeness theorem then implies that T must be 
formally provable from A.  So a counterexample of the type you envision 
would involve valid reasoning within ordinary mathematics that cannot be 
captured by first-order logic, and that would be *very* surprising.

Possibly you mean to claim something weaker, that informal mathematical 
reasoning might allow a "direct jump" from point P1 to point P2, while a 
formal prover might have to wend a meandering, tedious path from P1 to P2.  
This is certainly true.  But as long as the formal prover can always get 
from P1 to P2 somehow, I don't see a problem with calling its tortuous 
path the "formal equivalent" of the direct jump.

Tim