# [FOM] Formalization Thesis

catarina dutilh cdutilhnovaes at yahoo.com
Mon Dec 31 05:17:59 EST 2007

```Well, the discussion has now branched into so many (interesting!) paths that it is hard to come up with a coherent and yet sufficiently general reply at this point. But let me advance some comments nevertheless.

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. My impression from your first post was that you (Tim) were (originally) interested in reaching a precise enough *formulation* of it. But then you quickly moved on to actually arguing that FT does obtain of mathematics. 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 it.

As to whether FT does or does not hold, this is basically an *empirical* question, a matter of rolling up sleeves and moving on to formalizing theorems of mathematics (which is, of course, something that is already happening). But again, the hardest part seems to me to be the precise account of the relation of 'faithful expression' between a theorem of ordinary mathematics and a statement in some formal language. 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.

In your new formulation of FT, you adopt a much more 'instrumental' stance, where the transport of exact meaning from T in ordinary mathematics to T' in the formal language is less important. But then, whether the verification of T by means of T' is *indeed* a verification of T is again a matter of agreement or disagreement among mathematicians, and thus again not something that can be decided by purely formal, algorithming means.

I said:
> 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.

To which you replied:
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.

What I meant is something stronger than this. What I have in mind is something like the distinction between cut-free proofs and proofs with cut in proof theory: it is not only that cut-free proofs simply have more intermediary steps than the corresponding proofs with cut, but also that they often have to take a completely different path to get to the same place, i.e. the same conclusion. 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.

Catarina

----- Original Message ----
From: Timothy Y. Chow <tchow at alum.mit.edu>
To: fom at cs.nyu.edu
Sent: Friday, December 28, 2007 4:58:25 PM
Subject: Re: [FOM] Formalization Thesis

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
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom

____________________________________________________________________________________
Be a better friend, newshound, and
know-it-all with Yahoo! Mobile.  Try it now.  http://mobile.yahoo.com/;_ylt=Ahu06i62sR8HDtDypao8Wcj9tAcJ

```