[FOM] Formalization Thesis

[catarina dutilh]

Andre Rodin wrote:

A mathematical
theory, which suggests itself for the purpose of studying “translations”
between different parts of mathematics is Category theory (CT). In particular
it suggests a precise definition of faithfulness (I mean, of course) the notion
of faithful functor), which seems to be appropriate in the given context – but
perhaps needs to be somehow specified. In any event CT clearly shows that the
issue of “translation” invoked by FT is *mathematically* non-trivial. To study
(categories of) translations between different mathematical theories (including
those called “formal systems”) is, in my view, more important than only
establish that such-and-such translation exists.


This sounds very interesting and promising. I simply do not know enough Category Theory to be able to evaluate this claim, but the idea of a mathematical technique that can be used for the translation of theorems formulated in the idiom of ordinary mathematical (which is typically a mix of vernacular with some symbolism) into a formal language is certainly very important in the present context. I wonder what others who know more CT than I do would say about Andre's claim. I am familiar with translations of one logic into another done with purely logical/mathematical techniques (e.g. the work of Albert Visser), but what strikes me in such cases is that both ends of the translation process are already in some formalized form, which is of course not the case in the present debate.

Two questions:

- At some point, there must be a proof or an argument to the effect that the translation procedure provided by CT is indeed 'faithful' in the sense that we are after here. Is there already such a proof or argument?

- In how much of a formalized form must a theorem of ordinary mathematics already be in order to allow for the application of the techniques that Andre mentions?



Timothy Chow wrote:

However, I decided (at least preliminarily---maybe I could be convinced 
otherwise) against using ET as my basic formulation, for the following 
reason.  If we eschew all axioms and take just a first-order language with 
equality plus a binary relation symbol to be our "first-order language of 
set theory," then it seems somewhat dubious to me that formal sentences in 
such a language can "faithfully express" mathematical statements in 
anything like the desired sense.  Statements that are not *logically* 
equivalent, but that are equivalent only on the basis of a very weak 
fragment of ZFC, would not be equivalent if we do not lay down any axioms.  
For simple statements this might not be a big deal, but once you start 
trying to make nontrivial definitions, it becomes very awkward not to be 
able to assume (for example) that such-and-such a thing is *unique*.  
Unless we have structures have some minimal set-like behavior, I'm not 
sure I believe that the formal sentences are "expressing" the mathematical 
statements that they're trying to capture.



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.



Timothy Chow wrote:

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. Even in ordinary mathematics we usually say that there are different proofs of the same theorem, say of the Pythagorean theorem, if the steps taking one from A (premises) to B (conclusion, theorem) are different (even if A are the same). FT does not require equality (or faithful representation) of *proofs*: as you phrased it (every theorem of ordinary mathematics is a theorem of the suitable formal theory), what is required is that for every theorem of mathematics there is *a* proof in the formal theory with the same conclusion. 

FT clearly has the form: 

'For all T [theorems of mathematics] there is T' [a statement in the formal language] and there is P [a proof in the formal theory] such that (T's is the translation of T in the formal language (ET)) and (T' is the conclusion of P (PT))''. 

But from that to say that the original *proof* of the theorem in ordinary mathematics is faithfully represented just because it reaches the same conclusions, that seems to me to be misguided. Or would you say, for example, that two proofs of a given (logical) theorem, one which uses cut while the other is cut-free, are the same?


Catarina


      ____________________________________________________________________________________
Never miss a thing.  Make Yahoo your home page. 
http://www.yahoo.com/r/hs