[FOM] Formalization Thesis

[catarina dutilh]

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