Name the thesis: "Formal sentences capture informal ones"
in [Theory]
|
From: tchow on 4 Feb 2005 09:45 In article <1107395315.781677.218670(a)o13g2000cwo.googlegroups.com>, <examachine(a)gmail.com> wrote: >tchow(a)lsa.umich.edu wrote: >> Logicists don't claim that a finite set of axioms suffices to capture >>"all mathematical truth," whatever that is. >Ok. So, what was Torkel's concern about logicism? Well, someone (Wikipedia?) said that Goedel's theorem refuted logicism. Torkel Franzen said that he didn't think it did. So I don't think it's really "Torkel's concern"; the burden of proof should be on the person who thinks that Goedel's theorem refuted logicism to explain what is meant by that. Certainly, on the surface, the philosophical claim that mathematics reduces to logic does not appear to be refuted by Goedel's technical achievements. -- 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 4 Feb 2005 09:56 In article <36d2nfF4uqm0mU1(a)news.dfncis.de>, Mitch Harris <harrisq(a)tcs.inf.tu-dresden.de> wrote: >hmmm... but what does intelligible mean? is correctness involved with >that? >Wouldn't you say that some informal statements are imprecise, and so >must not be intelligible? That is, to the extent we can understand a >statement correctly, that must be formal enough (rather than informal). Sticking to the view that informality has something to do with intelligibility while formality has something to do with manipulability, I would say that some informal statements are imprecise, while others are quite precise, as far as meaning goes. In mathematics we're usually interested in the ones that are precise---or at least, we can't do much in the way of mathematical analysis until we have precise statements to work with. Having a precise *meaning* doesn't mean that the syntactic *form* of the sentences is precisely specified enough to allow mathematical manipulations of that formal structure. >(I'm not trying to be contrary for arguments sake; I'm trying to get a >reasonable understanding of what informal to mean for the purposes of your >proposed "thesis") Informal statements are the ones we understand the meanings of. Formal ones are the ones we can manipulate syntactically. [Re: how formal is formal enough] >but this sense seems to be captured fully by "precision" or "removal of >doubt" For independence results, the syntactic form does indeed need to be precisely specified enough. But my point is that the term "precision" can be applied either to *meaning* or to *syntactic form*. Either of these can be precise or imprecise. My "thesis" is that when you make the transition from something whose meaning we already understand to something with a syntactic form that can be manipulated, nothing of consequence is lost. -- 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: Stephen Harris on 4 Feb 2005 14:35 <tchow(a)lsa.umich.edu> wrote in message news:41ff9ff6$0$563$b45e6eb0(a)senator-bedfellow.mit.edu... > In article <1107246412.251830.121830(a)z14g2000cwz.googlegroups.com>, > <Helene.Boucher(a)wanadoo.fr> wrote: >>In any case, *if* that is the logicist thesis, then indeed it would >>seem to depend on your (*). That is, informal mathematics cannot >>reduce to formal logic unless informal mathematical assertions can be >>captured by assertions in formal logic. > > I agree with this. However, I would describe the situation as follows. > There are two steps involved: first, we translate informal mathematical > statements into formal ones. Second, the formal mathematical statements > are reduced to purely logical ones. > > The possibility of performing the first step is what I was focusing on. > The second step is, I think, the heart of logicism. If someone were to > propose a slightly different philosophical position from what you're > calling > logicism, namely that informal mathematics reduces to informal logic, I > would still be inclined to call that a variant of logicism. On the other > hand, someone who only accepts the first step but rejects the second > >doesn't > sound at all like a logicist to me. So I wouldn't call the first step any > kind of "logicist thesis." > > Something like "1+1=2" prima facie speaks of natural numbers. It is > rather > controversial whether natural numbers are purely *logical* entities. > Simply > formalizing the statement "1+1=2" without explicating how numbers reduce > >to > logic might be the *first* step to demonstrating how logicism "works," but > it is really the subsequent step (reduction of numbers to logic) that is > crucial for the logicist. > -- "There I conjectured that all of scientifically applicable mathematics can be directly formalized in W; further discussion of this conjecture further discussion will be found in the paper [Feferman 1993]." http://math.stanford.edu/~feferman/papers/ResponseToHellman.pdf "The first substantial work on predicative foundations of analysis (where, as pointed out above, the set-theoretical account immediately leads to impredicative definitions) was carried out by Hermann Weyl in Das Kontinuum (1918).3 He showed that all of the 19th century analysis of (step-wise) continuous functions could just as well be done predicatively. In my (1988) I brought Weyl's work up to date with use of a system W of variable finite types; in it much of 20th century functional analysis can also be developed. Surprisingly, the system W is of the same proof-theoretical strength as the system PA of Peano Arithmetic, which is just the base of the above progression of systems.4 Also, as explained there, it appears that all of scientifically applicable analysis can be formalized in W and hence rests on ultimately purely arithmetical foundations." ----------------------------------------------------------- http://math.stanford.edu/~feferman/papers/whatrests.pdf What rests on what? Proof-theoretical and foundational reductions. "In the following we use the letters: M, for an informal part of mathematics (such as number theory, analysis, algebra, etc., or a subdivision of such); L, for a formal language for a part of mathematics (e.g. the language of elementary number theory); phi, psi, . . . for well-formed formulas or statements of L; T, for a formal axiomatic system in L (e.g. the system of first-order Peano Arithmetic PA in the language of elementary number theory); and F, for a general foundational framework (e.g. finitary, constructive, predicative, countable infinitary, set-theoretical or uncountable infinitary, etc.). These categories provide different senses in which we can deal with the question of whatrests on what from a logical point of view: M rests on T, in the sense that M can be formalized in T; phi rests on T, in the sense that phi is provable in T; T rests on F, in the sense that T is justified by F; and T_1 rests on T_2, in the sense that T_1 is reducible to T_2. With respect to the last of these, there are different technical notions of reducibility of one axiomatic system to another. We want to contrast, in particular, the notion of T_1 being _interpretable_ (or _translatable_) in T_2 with that of T_1 being _proof-theoretically reducible_ to T_2, written T_1 < or = T_2 (this will be defined in #2). In general, these move in opposite directions from a foundational point of view, since we are mainly concerned with the relation T_1 < or = T_2 when T_2 is a _part_ of T_1, either directly or by translation. In contrast, T_2 tends to be more comprehensive than T_1 in the case of interpretations; a familiar example is that of Peano Arithmetic PA (as T_1) in Zermelo-Fraenkel set theory ZF (as T_2), where the natural numbers are interpreted as the finite ordinals. This is a _conceptual reduction_ of number theory to set theory, but not a _foundational reduction_, because the latter system is justified only by an uncountable infinitary framework whereas the former is justified simply by a countable infinitary framework. The driving aim of the original Hilbert program (H.P.) was to provide a finitary justification for the use of the "actual infinite" in mathematics. This was to be accomplished by directly formalizing one body or another of infinitary mathematics M in a formal axiomatic theory T_1 and then demonstrating the consistency of T_1 by purely finitary means; in practice, that would be established by a proof-theoretic reduction of T_1 to a system T_2 justified on finitary grounds. It is generally acknowledged that H.P. as originally conceived could not be carried through even for elementary number theory PA as the system T_1, in consequence of Godel's 1931 incompleteness theorems. This then gave rise to certain relativized forms of H.P.; the history will be traced briefly below. In our approach, what the results of a relativized H.P. should achieve are best expressed in the following way. ([Feferman 1988], p.364): A body of mathematics M is represented directly in a formal system T_1 which is justified by a foundational framework F_1. T_1 is reduced proof-theoretically to a system T_2 which is justified by another, more elementary such framework F_2. In Hilbert's scheme, F1 was to be the infinitary framework of modern mathematics featuring (i) the "completed" or "actual" infinite (both countable and uncountable) and (ii) non-constructive reasoning, while F_2 was to be the framework of finitary mathematics featuring (i)' only the "potential" infinite of finite combinatorial objects, and (ii)' constructive reasoning applied to quantifier-free statements (typically, equations). According to Hilbert, already the system PA embodies (i) and (ii) by the use of quantified variables which are supposed to range over the set N of natural numbers and the assumption of the Law of the Excluded Middle, ... The general problem raised by Godel's incompleteness results [1931] for H.P. is that if finitary mathematics is itself to count as a significant body of informal mathematics, it must be formalizable in a consistent formal axiomatic theory T. Then by Godel's second incompleteness theorem, the consistency of T would not be provable in T, hence could not be finitarily provable, and so H.P. cannot be carried out for T. Just what T could serve this purpose was not analyzed in the Hilbert school. Despite Hilbert's continued optimism, the general feeling after 1931 was that Godel's second incompleteness theorem doomed H.P. to failure, and that some essentially new idea would be needed to carry out anything like it, even for PA. Yet another result of Godel in his paper [1933] (independently found by Bernays and Gentzen) forced a further reconsideration of H.P.: This showed that PA could be translated in a simple way into the intuitionistic system HA of Heyting's arithmetic, which differs from PA only in omitting the Law of the Excluded Middle from its basic logical principles. ... Two matters remain to be dealt with in this final section in order to fill out the scheme (*) of #1. The first is to say something about the passage by formalization from a body of mathematics M to a formal theory T, especially with reference to the systems presented in #2. The second is to indicate the philosophical significance of the kind of reduction of T_1 to T_2 illustrated by the results in #2. We take these up in that order. The scheme (*) calls for M to have a direct formalization in T_1; at the same time we should expect that T_1 does not go beyond M in any essential respects. It is worth elaborating what is required, following the criteria for formalization set forth in [Feferman 1979] pp. 171-72, for any M and T, as follows. (i) T is an adequate formalization of M if every concept, argument and result of M may be represented by a (basic or defined) concept, proof and theorem, resp. of T. (ii) T is in accordance with (or faithful to) M if every basic concept of T corresponds to a basic concept of M and every axiom and rule of T corresponds to, or is implicit in, the assumption and reasoning followed in M (in other words, if T does not go beyond M conceptually or in principle). The idea of T being directly adequate to, resp. directly in accordance withMis clear. We would say that T is indirectly adequate to M if a theory directly adequate to Mis reducible to T in an elementary way (e.g. by a translation or proof- theoretic reduction) while it is indirectly in accordance with M if T is reducible to a theory directly in accordance with M. There is a second way in which a theory T may be indirectly adequate to M: that is to reformulate the concepts, proofs and theorems of M informally in such a way that the resulting M' can be directly formalized in T. Obviously these criteria are not precise and there may be reasonable differences of opinion as to their application in specific cases. The idea, again, is to say what strikes us as a just ascription on the basis of general experience. Detailed work of formalization may then lead us to modify such an attribution. In particular, it is a common result of such work that a system T which appears to us to provide an adequate and faithful formalization of a body of mathematics M goes far beyond what is actually needed to represent M in practice. ... "There I conjectured that all of scientifically applicable mathematics can be directly formalized in W; further discussion of this conjecture further discussion will be found in the paper [Feferman 1993]." Regards, Stephen
From: Stephen Harris on 4 Feb 2005 18:15
<tchow(a)lsa.umich.edu> wrote in message news:42038a7c$0$580$b45e6eb0(a)senator-bedfellow.mit.edu... > In article <1107395315.781677.218670(a)o13g2000cwo.googlegroups.com>, > <examachine(a)gmail.com> wrote: >>tchow(a)lsa.umich.edu wrote: >>> Logicists don't claim that a finite set of axioms suffices to capture >>>"all mathematical truth," whatever that is. >>Ok. So, what was Torkel's concern about logicism? > > Well, someone (Wikipedia?) said that Goedel's theorem refuted logicism. > Torkel Franzen said that he didn't think it did. So I don't think it's > really "Torkel's concern"; the burden of proof should be on the person > who thinks that Goedel's theorem refuted logicism to explain what is > meant by that. Certainly, on the surface, the philosophical claim that > mathematics reduces to logic does not appear to be refuted by Goedel's > technical achievements. > -- > There is an analogous thesis that is relevant to logic and the foundations > of mathematics: > > (*) Formal sentences (in PA or ZFC for example) adequately express > their informal counterparts. http://math.stanford.edu/~feferman/papers/whatrests.pdf What rests on what? Proof-theoretical and foundational reductions. "The general problem raised by Godel's incompleteness results [1931] for H.P. (Hilbert Program) is that if finitary mathematics is itself to count as a significant body of informal mathematics, it must be formalizable in a consistent formal axiomatic theory T. Then by Godel's second incompleteness theorem, the consistency of T would not be provable in T, hence could not be finitarily provable, and so H.P. cannot be carried out for T. Just what T could serve this purpose was not analyzed in the Hilbert school." -------------------------------------------------------------- Why a Little Bit Goes a Long Way: Logical Foundations of Scientifically Applicable Mathematics Solomon Feferman Stanford Mathematics http://www-csli.stanford.edu/Archive/calendar/1994-95/msg00010.html "An axiomatic theory W of functions and classes will be described which has been proved (in joint work with G. Jaeger) to be a conservative extension of the system PA of Peano Arithmetic. I will sketch how considerable portions of modern analysis can be carried out in W. It is conjectured that W comprehends all (or almost all) of scientifically applicable mathematics. This work is a modern extension of the program set out by Hermann Weyl in his 1918 monograph "Das Kontinuum"; hence the choice of 'W' for the system in question." |