Name the thesis: "Formal sentences capture informal ones"
in [Theory]
|
From: Torkel Franzen on 30 Jan 2005 13:14 Helene.Boucher(a)wanadoo.fr writes: > On the other hand if one could show that S1, which > purported to be a correct formalization of the FTA, was not true under > the same conditions as FTA, then that would be good grounds for > rejecting that S1 is a correct formalization. Does "under the same conditions" involve what we can imagine, and possible worlds?
From: tchow on 30 Jan 2005 16:30 In article <vcbmzurjyep.fsf(a)beta19.sm.ltu.se>, Torkel Franzen <torkel(a)sm.luth.se> wrote: >> (+) Con("PA") is an intension-preserving formalization of "PA is >> consistent" > (+) is not on the face of it an instance of (*), since it states not >only that an itension-preserving formalization of "PA is consistent" >is possible, but that a particular arithmetical formula is such a >formalization. Yes, that's what I meant by abusing the word "schema." What I probably want is not either (+) or (*), but some schema (which I'm having difficulty formulating) of which (+) is an instance. >What is required of an intension-preserving >formalization? In formalizing Con(PA) or the fundamental theorem of >arithmetic in PA, we need to represent finite sequences of numbers >as numbers. This can be done in many ways, but are they >intension-preserving? These are excellent questions, and part of the purpose of formulating the thesis is so that these questions can be raised explicitly and debated. I would say that *something like* (+) is implicitly accepted by most people, and forms the basis for concluding that Goedel's 2nd theorem effectively kills Hilbert's program as originally conceived. Detlefsen has raised the possibility that this received wisdom is ill-founded, and as I recall, his argument hinges on considering deviant consistency predicates and, in effect, questioning whether standard consistency predicates adequately capture the true meaning of consistency. Most people don't buy this argument, and I think that it's because they accept (+). I think, then, that there is no doubt that (+), or something like it, is firmly held by many people, despite the vagueness of the term "intension- preserving" and the difficulty of formulating it more precisely. So as long as you agree that the thesis I'm trying to articulate has many instances that are widely accepted, I regard the questions you raise as indicating the usefulness of articulating the thesis explicitly, not as reasons to doubt the possibility of such articulation. -- Tim Chow tchow-at-alum-dot-mit-dot-edu The range of our projectiles---even ... the artillery---however great, will never exceed four of those miles of which as many thousand separate us from the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
From: tchow on 30 Jan 2005 16:53 In article <ctid7v$dus$1(a)phys-news1.kolumbus.fi>, Aatu Koskensilta <aatu.koskensilta(a)xortec.fi> wrote: >tchow(a)lsa.umich.edu wrote: >> (*) Intension-preserving formalization of informal mathematical >> statements is always possible. >> >> (+) Con("PA") is an intension-preserving formalization of "PA is >> consistent." > >But (+) isn't an instance of (*). Right, that's what I meant by "abusing the term `schema.'" What I want is probably neither (*) nor (+) but some schema of which (+) will be an instance. >For example, how do we know that Con("PA") - expressed in what ever way >- instead of the myriard other possible arithmetical sentences is the >formal counterpart of "PA is consistent"? I don't see why this is relevant. I am not concerned with saying that Con("PA") is *the* formalization of "PA is consistent"; indeed, that is surely totally false. I only want to say that it is *an* acceptable formalization. >The point I'm trying to make here is that in order to >instantiate (*) to get something like (+) for a particular mathematical >statement P we would need to know what formal sentence is the >intension-preserving formalization of P. This in turn requires that the >notion of "intension-preserving formalization" is explicated in an >informative, hopefully mathematical, way. As I understand it, this is precisely the kind of project that Sol Feferman undertook in his early years. He made a number of striking contributions, which I have not taken the time to understand fully. However, I think I understand enough of the issues involved to say something about the idea of explicating "intension-preserving" in a mathematical way. Let me first refer you to my article `What makes a representing formula "reasonable"?' that I posted to sci.logic on Dec 12 2002. (You can find it on Google Groups; I'd give the URL, but Google currently has an annoying beta version whose URL's are ephemeral.) Even something as simple as "x is even" admits deviant formalizations. One might then ask, is there a way to say precisely what a "normal" or "intension-preserving" formalization of "x is even" is? I asked this question of Ken Kunen and he replied as follows (I believe he would not mind my quoting his email here): :This depends on what your framework is. :If you are thinking of "x is even" as an informal concept defined in :the metatheory, then there is no way to say formally what the :correct expression is for "x is even" within ZF, since you don't :have a formal definition of "x is even" to start with. : :On the other hand, you might think of the metatheory itself as :a formal system, such as PRA (primitive recursive arithmetic). :Then, one can formally define a map from PRA formulas into ZFC :so that every theorem of PRA maps into a theorem of ZFC. :Of course, you are just pushing the problem back one step. :You would still have to argue informally that the standard :primitive recursive definition of "x is even" captures :the informal notion of "even". I think what Kunen's remarks indicate is that there is no way out of the infinite regress other than by starting with an informal-to-formal transition somewhere and then baldly postulating that it is correct. This, to me, is reminiscent of the Church-Turing thesis. Furthermore, there is no doubt in anyone's mind that, for example, the standard primitive recursive definition of "x is even" correctly captures the informal notion of "even." So I don't think that the difficulty of formulating precisely what "intension-preserving" means should lead us to worry that my proposed thesis, when formulated properly, is not worthy of trust. >But even this thesis is problematic. What sort of consistency are we >talking here? Herbrand consistency? Hilbert consistency? Or are these >irrelevant and are we assuming some background theory in respect to >which various formalizations are found to be equivalent? And how do we >know that Con_phi "intension-preservingly" expressed the consistency of >the theory defined by phi? What if it just expresses this in a >non-intension-preserving way? I would repeat what I said to Torkel Franzen, that I think these are good questions, but that they shouldn't make us doubt that certain instances of the thesis that I'm groping towards are meaningful and widely accepted, nor should it make us doubt that the thesis is too vague to be formulated properly. In fact, I'm encouraged that my attempt to state the thesis is provoking exactly the kinds of questions that I think it ought to provoke, providing a basis for which to examine them. -- Tim Chow tchow-at-alum-dot-mit-dot-edu The range of our projectiles---even ... the artillery---however great, will never exceed four of those miles of which as many thousand separate us from the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
From: Torkel Franzen on 31 Jan 2005 02:15 tchow(a)lsa.umich.edu writes: > I would say that *something like* (+) is implicitly accepted by most > people, and forms the basis for concluding that Goedel's 2nd theorem > effectively kills Hilbert's program as originally conceived. Certainly. However, for this we don't need "intension-preserving". It is sufficient that the equivalence of Con(PA) and a "direct" formalization of "PA is consistent" is provable in a weak theory.
From: Torkel Franzen on 31 Jan 2005 02:20
tchow(a)lsa.umich.edu writes: > As I understand it, this is precisely the kind of project that Sol Feferman > undertook in his early years. If you mean the work in "Arithmetization of metamathematics in a general setting", this dealt with more pressing problems. He showed among other things that the incompleteness theorem holds in a general formulation provided we require the axioms of a theory to be defined by what we now call a Sigma-formula. However, a Sigma-formula which extensionally defines the axioms of e.g. PA can still be intensionally incorrect. > I think what Kunen's remarks indicate is that there is no way out of > the infinite regress other than by starting with an informal-to-formal > transition somewhere and then baldly postulating that it is correct. Yes, what I called a "direct" translation. |