[FOM] Formalization Thesis

[Timothy Y. Chow]

catarina dutilh <cdutilhnovaes at yahoo.com> wrote:
>The issues you raise here seem again to concern the matter of the 
>*expressive power* of the language in question, and not its deducible 
>strength. You do not need axioms to be able to *express* that 
>"such-and-such a thing is *unique*", what you need is devices in the 
>language that allow you to express that. So, as I see it, it's again a 
>matter for ET.

I don't believe that the distinction is as clearcut as you make it.  Let 
me return to the example I gave before: "x = {{x_1}, {x_1,x_2}}" as a 
"faithful expression" of "x is the ordered pair (x_1,x_2)".  The reason we 
believe that this is a faithful expression is that we are able to *prove* 
that "{{x_1},{x_1,x_2}} = {{y_1},{y_1,y_2}} iff x_1 = y_1 and x_2 = y_2."  
If we did not give ourselves the set-theoretic axioms that allow us to 
prove this, then I don't think we would come to accept that the relevant 
formula in the language with one binary relation symbol "expresses" the 
concept of an ordered pair.  Derivability is intertwined with 
expressibility in an essential way.  This happens frequently in 
mathematics, e.g., whenever you have to prove a theorem in order to verify 
that a proposed definition makes sense.

>>I guess my concept of a formal proof faithfully representing an informal 
>>one requires only that any informal path from A to B can be mimicked by 
>>*some* formal path from A to B, not that the road taken must somehow 
>>correspond one-to-one at some microscopic level.
>
>I strongly disagree with that.

Whoops, you're right, I was careless here.  I was still thinking in terms 
of your original question about whether informal proofs of theorems can be 
given an "equivalent formulation" in the formal theory (as opposed to 
being "faithfully represented").  By "equivalent formulation" I understood 
something weaker than "faithful representation"---something to the effect 
that someone sitting down to formalize a correct informal proof will 
always be able to succeed, without having to invent an entirely new proof.  
The resulting formal proof might take byzantine byways that cause it to 
fall short of a *faithful representation of the informal proof*, but as 
long as we can replace informal jumps by formal steps in some relatively 
routine manner, we will still get the job done.

The question you raise as to whether informal proofs can always be 
faithfully represented, in the sense (for example) that informal judgments 
such as "P1 is essentially the same proof as P2" and "P1 is an essentially 
different proof from P2" are systematically captured by a formal notion of 
proof equivalence, is a deeper one.  My sense is that we're much further 
away from understanding the concept of faithful representations of proofs 
than we are from understanding the concept of faithful representations of 
theorems.

Tim