# [FOM] Formalization Thesis

Timothy Y. Chow tchow at alum.mit.edu
Fri Jan 4 15:02:05 EST 2008

```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
```