[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Fri Dec 28 10:58:25 EST 2007
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
More information about the FOM
mailing list