Torkel Franzen on truth
in [Logic]
|
From: Newberry on 15 Nov 2007 22:28 On Nov 15, 9:10 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > > > >On Nov 15, 3:12 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> No, we *don't* have that the human mind surpasses any machine. > >> There is no reason to believe that's true. > > >But we do. We know that G is true. > > That does not prove that the human mind surpasses any machine. > You can certainly program a machine to know, among its basic > facts, that G(PA) is true. > > >Proof: > >The axioms of PA are manifestly true > >PA is consistent > >"PA is consistent" is equivalent to G > >G QED > > >This proof cannot be formalized. > > That's just not true. It can perfectly well be formalized. > It just can't be formalized in the language of PA. > > Extend PA to a new theory PA-plus in the following > way: > > Add a new predicate symbol T(x). For every statement S > in the language of PA, add the axiom > > S <-> T(#S) > > where #S means the Godel code of S. Then add the > axiom > > Ax Prove(PA,x) -> T(x) > > where Prove(PA,x) is the formalization of the proof > predicate. > > In PA-plus, it is perfectly straight-forward to prove > G(PA) (the Godel statement for PA). A couple of comments. Firstly, I do not know if the proof you are showing is the same as the manifest truth proof. Secondly, if I understand you correctly the only difference between (Ex)P(x, #("F") --> F and Ax Prove(PA,x) -> T(x) is the "T." It is not that it cannot be formalized in the language of PA, it is that it leads to a contradiction. Did we put the axiom on a meta-level just to avoid the contradiction? BTW, I do not understand this: S <-> T(#S), where #S means the Godel code of S. The Goedel number of S is true ... ?
From: MoeBlee on 15 Nov 2007 22:30 On Nov 15, 7:20 pm, Newberry <newberr...(a)gmail.com> wrote: > On Nov 15, 8:52 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > wrote: > > > Newberry says... > > > >On Nov 14, 9:13 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) > > >wrote: > > >> Are you asking how one would go about *programming* > > >> a computer program that would emulate a human's > > >> mathematical reasoning? If so, I have no idea. > > > >Easy. Just add this axiom: (Ex)P(x, #("F") --> F > > > But Godel shows that adding that axiom is inconsistent. > > I do not know if Goedel actually showed this particular case but it > certinly is inconsistent. But what is wrong with this axiom? It is > just as compelling as the rest of them. When people say that G is true > because of its meaning this is the derivation rule they use. What people? Where does anyone use such a rule? MoeBle
From: Daryl McCullough on 15 Nov 2007 22:33 Newberry says... >On Nov 15, 8:52 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) >wrote: >> Newberry says... >> >Easy. Just add this axiom: (Ex)P(x, #("F") --> F >> >> But Godel shows that adding that axiom is inconsistent. > >I do not know if Goedel actually showed this particular case but it >certainly is inconsistent. But what is wrong with this axiom? It is >just as compelling as the rest of them. When people say that G is true >because of its meaning this is the derivation rule they use. It depends on what P is. If you create a program P that proves theorems, and you have good reason to believe that P is consistent, then you can create a new theory T with the axiom schema (P proves S) -> S Program P itself can't take advantage of this axiom without being inconsistent, but T can. T will necessary go beyond what P can prove. -- Daryl McCullough Ithaca, NY
From: Newberry on 16 Nov 2007 00:05 On Nov 15, 7:33 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > >On Nov 15, 8:52 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> Newberry says... > >> >Easy. Just add this axiom: (Ex)P(x, #("F") --> F > > >> But Godel shows that adding that axiom is inconsistent. > > >I do not know if Goedel actually showed this particular case but it > >certainly is inconsistent. But what is wrong with this axiom? It is > >just as compelling as the rest of them. When people say that G is true > >because of its meaning this is the derivation rule they use. > > It depends on what P is. If you create a program P that proves > theorems, and you have good reason to believe that P is consistent, > then you can create a new theory T with the axiom schema > > (P proves S) -> S > > Program P itself can't take advantage of this axiom without > being inconsistent, but T can. T will necessary go beyond > what P can prove. Here we go again - a meta-level. This looks a little bit like Russell's theory of types. But the theory of types has its own difficulties. Does T surpass the machine P? BTW, I do not see any reason why the axiom schema should be on another level. It is just as compelling as the rest of them. We do not split Peano's axioms either and do not say these axioms hold in P, you can add two more in S but P cannot take any advantage of them. There is a difference between saying a theory or machine is intrinsically incapable of proving some true sentences and saying the machine "cannot" prove them because a contradiction would result. So we patch the system by creating an ad hoc meta-level.
From: LordBeotian on 16 Nov 2007 08:46
"Newberry" <newberryxy(a)gmail.com> ha scritto >> It depends on what P is. If you create a program P that proves >> theorems, and you have good reason to believe that P is consistent, >> then you can create a new theory T with the axiom schema >> >> (P proves S) -> S >> >> Program P itself can't take advantage of this axiom without >> being inconsistent, but T can. T will necessary go beyond >> what P can prove. > > Here we go again - a meta-level. This looks a little bit like > Russell's theory of types. But the theory of types has its own > difficulties. Does T surpass the machine P? > > BTW, I do not see any reason why the axiom schema should be on another > level. It is just as compelling as the rest of them. We do not split > Peano's axioms either and do not say these axioms hold in P, you can > add two more in S but P cannot take any advantage of them. There is no other levels. The statement G="(P proves S) -> S" is an arithmetical statement. You can of course add it to the axioms of P, but once you have done it you get another set of axioms, not P anymore. You can also consider the statement G'="(P+*this statement* proves S)->S" and add it to P. So you obtain a theory P' including the axiom "(P' proves S)->S". But the statement G' is false and can be proven to be false in P. So if you add it to P you obtain an inconsistent theory. |