Name the thesis: "Formal sentences capture informal ones"
in [Theory]
|
From: tchow on 31 Jan 2005 10:35 In article <vcbhdkxfxc8.fsf(a)beta19.sm.ltu.se>, Torkel Franzen <torkel(a)sm.luth.se> wrote: >tchow(a)lsa.umich.edu writes: >> Granted, "PA is consistent" >> is very precise, but I don't think it's *sufficiently* precise for >> us to prove theorems about it as it stands. > I don't see what you have in mind here. What imprecision makes >itself felt, and how and when? On reflection, I see that "precise" is the wrong word. The literal sentence "PA is consistent" doesn't have all the *properties* that are needed for the kind of mathematical analysis that we would like to perform on it. If we want to study whether it is provable, it is convenient for it to have a certain syntactic form that the sentence, as it stands, does not have. So we need to translate it into a suitable form. But anyway, whether you call it a social agreement or an assumption, there is some kind of important principle in the background here. I think that it's useful to state it explicitly and succinctly---unless for some reason that's impossible, which I don't believe (yet). -- 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 10:43 tchow(a)lsa.umich.edu writes: > But anyway, whether you call it a social agreement or an assumption, there > is some kind of important principle in the background here. I think that > it's useful to state it explicitly and succinctly---unless for some reason > that's impossible, which I don't believe (yet). In the case of actual instances of formalization on which people are agreed, I think it is sufficient to observe that the informal version A and the formalized version A* are both equivalent, in a weak theory, to some direct formalization A**. The equivalence of A and A** is a matter of agreement on usage, based on the standard informal explanations of quantifiers and connectives.
From: yaoziyuan on 31 Jan 2005 12:28 So your this post was 29 Jan 2005 20:00:28 GMT. Interestingly, I posted a maybe relevant post to the newsgroup list.linguist on 29 Jan 2005 17:39:12 GMT, Message-ID: <1107020352.414946.304230(a)f14g2000cwb.googlegroups.com>. My that post was about a possible "computer-based human translator testing" program, which exactly attempts to use a formal sentence to verify if a natural language sentence is semantically equivalent. Here's how my speculative testing program works: STEP 1: Randomly generate a formal sentence F from a knowledge base; STEP 2: Generate a source natural language sentence S based on F; STEP 3: Let the human trainee to translate S to a target natural language sentence T; STEP 4: Validate if the human answer T is ANY OF ALL THE POSSIBLE CORRECT TRANSLATIONS inferrable from F with enough symbolic transform rules (or "rule-based transfer rules" in terms of machine translation) applied. This is exactly "to capture informal sentence T using formal sentence F". Later then I generalized this idea to a class of "computer-based training programs", which may start a new, useful branch in AI research... Yao
From: Helene.Boucher on 31 Jan 2005 13:06 LordBeotian wrote: > <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... > > > > It is not usually explicitly stated, but it is assumed when one > > supposes that the sequential operator is total, i.e. that for every > > natural number n, (n') exists. > > Ok, so we would have to change PA in such a way that S is just a relation > symbol... > In the case you suggest PA has the model given by {0,1}. > Are you suggesting that {0,1} *could be* the whole set of natural numbers?> If not we can add the axiom "1 has a successor". > Are you suggesting that {0,1,2} *could be* the whole set of natural numbers? > If not we can add the axiom "2 has a successor". > And so on... unless there is a point when you say "yes, I suggest that the > set {0,1,..,890} (for example) *could be* the whole set of natural numbers". > If this never happen we have added enough axioms to have a system that > believe that any natural number has a successor. If there is a problem with the successor axiom itself, there is a problem with you using "and so on..." as you have done.
From: LordBeotian on 31 Jan 2005 13:54
<Helene.Boucher(a)wanadoo.fr> ha scritto > > Ok, so we would have to change PA in such a way that S is just a > relation > > symbol... > > In the case you suggest PA has the model given by {0,1}. > > Are you suggesting that {0,1} *could be* the whole set of natural > numbers?> If not we can add the axiom "1 has a successor". > > Are you suggesting that {0,1,2} *could be* the whole set of natural > numbers? > > If not we can add the axiom "2 has a successor". > > And so on... unless there is a point when you say "yes, I suggest > that the > > set {0,1,..,890} (for example) *could be* the whole set of natural > numbers". > > If this never happen we have added enough axioms to have a system > that > > believe that any natural number has a successor. > > If there is a problem with the successor axiom itself, there is a > problem with you using "and so on..." as you have done. The only "problem" I see is if there is a point when you say "yes, I suggest that the set {0,1,..,890} (for example) *could be* the whole set of natural numbers", is this the case? |