Name the thesis: "Formal sentences capture informal ones"
in [Theory]
|
From: |-|erc on 31 Jan 2005 04:11 "Torkel Franzen" <torkel(a)sm.luth.se> wrote in > > > 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. Informal statements are countable! There shouldn't be a problem its just the AI problem in disguise, you guys will spend 100 trilobytes tripping over "you can't prove me" and swear 'it can't be done it can't be done' but a good kick in the teeth will fix that! unless someone actually bothers to reason correctly about proof2truth as a perspective and dismisses your HOPELESS model assertions that prove stuff they don't know is true themselves....yeah right, I think we'll just flush the few million modern day theorists and start over with AI running to stop all your moronic Godel "justifications". what do we know about informal statements? 1/ they have double meanings, the shorter the utterance the more free scope that must be bounded 2/ there are several ways to say the same thing, higher generalisation hierarchies of statements. 3/ knowledge my be incomplete, fill in the added words 4/ utterance may be a generic statement in exampler form (see i just made up a word then!) 5/ fuzzy start and end points, granularity 6/ pronouns, combine with environmental information, brevity 7/ obscure topics 8/ interpreted as spoken, linear 9/ massive massive databases of text 10/ real world database (examples) and platonic mathematical Universe of Discourse ..... Is it CORRECT to assign godel numbers to english sentences? paragraphs? or is 'formalising' a real time process of a less memory intensive 'comprehension' or 'understanding' procedure? Interpretation / translation is only a STEP of theorem proving. What about modus ponens? It has to be modelled in a computational framework, the sentences aren't stagnant. Herc
From: Mitch Harris on 31 Jan 2005 05:02 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 (*)). (given that "people" really refers to mathematicians) I'd expect that most would not be terribly put out if confronted with the distinction (i.e. that the work they do is not formal). > Any candidates for a catchy name for (*)? Whether the concept is well-defined or not, we can still give the thing we want to talk about a name. "Hilbert's thesis" seems to have been taken by a related but much more specific concept "the informal concept of proof is adequately modeled by the first-order model of proof" http://www.cs.nyu.edu/pipermail/fom/1997-October/000127.html how about the "formalization thesis/principle/program"? -- Mitch Harris (remove q to reply)
From: Mitch Harris on 31 Jan 2005 05:14 Torkel Franzen wrote: > 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. Yes, but I think that's the kind of discussion Tim is looking for, to help make it more precise, if possible. I think the statement has difficulties not with precision (or possible precision) but about self-reference. If it is to be made more precise, then the concept "informal sentence" must be made more precise. > What is the > informal counterpart of a formal sentence in PA or ZFC? It sounds to me like Tim's direction is from the informal to the formal, though at some point your question needs to be addressed, too. As someone else mentioned, is the informal counterpart of a formal sentence just its expression in natural language? -- Mitch Harris (remove q to reply)
From: Herman Jurjus on 31 Jan 2005 06:07 tchow(a)lsa.umich.edu wrote: > 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"? That might be called 'Bourbaki thesis', perhaps? -- Cheers, Herman Jurjus
From: LordBeotian on 31 Jan 2005 06:22
<Helene.Boucher(a)wanadoo.fr> ha scritto > No, it's the axiom "(x)(Nx => there exists y such that Sxy)", i.e. > every natural number has a successor. As far as I know it is not an axiom of PA... |