[FOM] Formalization Thesis

[catarina dutilh]

 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