Name the thesis: "Formal sentences capture informal ones"
in [Theory]
|
From: tchow on 29 Jan 2005 15:00 The Church-Turing thesis is familiar to many people, largely because it has been widely discussed both in textbooks and in popular science writing. Having a name helps, too. 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. Years of discussion, on USENET and elsewhere, has convinced me that the average level of understanding of foundational issues would be enormously improved if (*) were, like the Church-Turing thesis, given a name and widely discussed. As matters stand today, a lot of people don't seem to even acknowledge the existence of informal mathematical discourse, despite the fact that all but a tiny fraction of mathematical discourse they've ever seen is informal (in the sense of (*)). At a somewhat more sophisticated level, I can testify that my own ability to grasp intermediate-level concepts such as the proof of the reflection theorem and Rosser-style proof predicates would have been improved if I had already had a firm grasp of the significance of (*). Any candidates for a catchy name for (*)? -- 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 29 Jan 2005 15:18 tchow(a)lsa.umich.edu writes: > The Church-Turing thesis is familiar to many people, largely because it > has been widely discussed both in textbooks and in popular science writing. > Having a name helps, too. > > 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. (*) is rather too imprecise to be given a catchy name. What is the informal counterpart of a formal sentence in PA or ZFC?
From: r.e.s. on 29 Jan 2005 15:40 <tchow(a)lsa.umich.edu> wrote ... > The Church-Turing thesis is familiar to many people, largely because it > has been widely discussed both in textbooks and in popular science > writing. > Having a name helps, too. > > 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. > > Years of discussion, on USENET and elsewhere, has convinced me that the > average level of understanding of foundational issues would be enormously > improved if (*) were, like the Church-Turing thesis, given a name and > widely discussed. > > As matters stand today, a lot of people don't seem to even acknowledge the > existence of informal mathematical discourse, despite the fact that all > but > a tiny fraction of mathematical discourse they've ever seen is informal > (in > the sense of (*)). That reminds me of what Davis & Hersh say about Hilbert's "formalist premise" ... "Hilbert's program rested on two unexamined premises; first, the Kantian premise that _something_ in mathematics -- at least the purely "finitary part" -- is a solid foundation, is indubitable; and second, the formalist premise, that a solidly founded theory about formal sentences could validate the mathematical activity of real life [...]" --r.e.s.
From: tchow on 29 Jan 2005 15:31 In article <vcbsm4kj8g7.fsf(a)beta19.sm.ltu.se>, Torkel Franzen <torkel(a)sm.luth.se> wrote: >> (*) Formal sentences (in PA or ZFC for example) adequately express >> their informal counterparts. > (*) is rather too imprecise to be given a catchy name. What is the >informal counterpart of a formal sentence in PA or ZFC? Then how about, "All informal statements of ordinary mathematics are expressible by formal sentences in ZFC"? -- 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: Aatu Koskensilta on 29 Jan 2005 15:32
tchow(a)lsa.umich.edu wrote: > The Church-Turing thesis is familiar to many people, largely because it > has been widely discussed both in textbooks and in popular science writing. > Having a name helps, too. > > 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. Erhm. What is the informal counterpart of a randomly chosen formal sentence, in the language of arithmetic or in the language of set theory? Do arbitrarily complex formal sentences have informal counterparts? How do we know this? It seems that the following very vaguely formulated thesis is more strongly supported by the evidence we have, and more relevant to applications: (*) Every informal mathematical statement can be given a faithful formal rendition in a suitably chosen formal language and relevant background theory I'm not at all convinced that all sentences of, say, the language of arithmetic have informal counterparts if by informal counterparti we're supposed to mean anything more substantial than "for every natural number x there exists a natural number y such that for all natural numbers z there exists a natural number w such that for all natural numbers u ..." -- Aatu Koskensilta (aatu.koskensilta(a)xortec.fi) "Wovon man nicht sprechen kann, daruber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus |