# [FOM] Formalization Thesis

catarina dutilh cdutilhnovaes at yahoo.com
Mon Jan 7 05:43:18 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.

Tim Chow wrote:
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.

Well, in fact I think I totally agree with you on that! This may sound as a surprise at this point, after I have insisted so much on differentiating ET from PT; but I in fact sympathize a great deal with proof-theoretic semantics and inferentialism in general, i.e. the view according to which meaning is (to a great extent) determined by inferential relations. So while I still think that expressibility and provability must be (at least conceptually) distinguished, I grant that there is a great deal of intertwining between them.

Tim Chow wrote:
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.

I agree with that too: faithful representation of proofs is evidently a thornier matter than faithful representation of theorems (understood as statements for which there is a proof). So first things first: let us focus on the faithful representation of statements (be they theorems or not) from ordinary mathematics into some formal language.

Catarina

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

```