Torkel Franzen on truth
in [Logic]
|
From: Daryl McCullough on 16 Nov 2007 10:57 Newberry says... > >On Nov 15, 7:33 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) >wrote: >> 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. No, not really. The types are not different; it can all be done in the language of arithmetic, where the only type is "natural number". It's more like Tarski's levels of truth. There is no problem having a truth predicate for arithmetic in a language that goes beyond arithmetic. But you can't have a truth predicate for arithmetic *within* arithmetic. >But the theory of types has its own >difficulties. Does T surpass the machine P? That's what I just said: "T will necessarily go beyond what P can prove". >BTW, I do not see any reason why the axiom schema should be on another >level. What do you mean by "on another level"? Let me just introduce a bit of terminology. The axiom schema "(P proves S) -> S" is the "soundness schema" for P. It says that P is sound, in the sense that it never proves a false statement. So the way I've defined T, T proves the soundness schema for P. But T *cannot* prove its own soundness schema. There is no consistent theory T (at least not with ordinary first-order logic) that has an axiom saying (T proves S) -> S >It is just as compelling as the rest of them. What is just as compelling? >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. PA is *already* a specific, well-defined theory. If you add axioms to it, you have formed a *new* theory, PA-plus. Of course PA can't take advantage of these new axioms, because they aren't axioms of PA. The same is true of a program P that proves theorems. If P is sound, then the soundness schema for P is true, but is not provable by P. You can certainly *modify* P by adding the soundness schema, but then you've created a *new* program, P'. >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. It's not that the machine cannot prove them *because* a contradiction would result. Machines don't care whether they prove a contradiction or not. Rather, the implication is this: *if* you construct a theory that can prove its own soundness schema, *then* that theory is inconsistent. -- Daryl McCullough Ithaca, NY
From: Daryl McCullough on 16 Nov 2007 11:07 Newberry says... >A couple of comments. Firstly, I do not know if the proof you are >showing is the same as the manifest truth proof. I have no idea what you mean by "the manifest truth proof", unless it is just the informal argument: Every axiom of PA is true. Truth is preserved under logical deduction. Therefore, every theorem of PA is true. A contradiction can't be true. Therefore, PA can't prove any contradictions. This proof can certainly be formalized. It just can't be formalized in PA. >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. No, it can't be formalized in PA, because there is no formula in PA which says "S is a true sentence of arithmetic". >Did we put the axiom on a meta-level just to avoid the >contradiction? We put it in at the meta-level because PA doesn't have a truth predicate. >BTW, I do not understand this: >S <-> T(#S), where #S means the Godel code of S. >The Goedel number of S is true ... ? No, T(#S) doesn't say #S is true, it says "#S is the Godel code of a true statement". -- Daryl McCullough Ithaca, NY
From: Newberry on 17 Nov 2007 12:02 On Nov 16, 7:57 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > > > >On Nov 15, 7:33 pm, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> 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. > > No, not really. The types are not different; it can all > be done in the language of arithmetic, where the only type > is "natural number". > > It's more like Tarski's levels of truth. OK, Tarski's truth level. Whatever. Same thing. There is no problem > having a truth predicate for arithmetic in a language that > goes beyond arithmetic. But you can't have a truth predicate > for arithmetic *within* arithmetic. If you say "can't" what does the impossibility consist of. Is it somehow inherently impossible or it "can't" be done because a contradiction would result? > > >But the theory of types has its own > >difficulties. Does T surpass the machine P? > > That's what I just said: "T will necessarily go beyond > what P can prove". > > >BTW, I do not see any reason why the axiom schema should be on another > >level. > > What do you mean by "on another level"? Let me just introduce > a bit of terminology. The axiom schema > > "(P proves S) -> S" > > is the "soundness schema" for P. It says that P is sound, > in the sense that it never proves a false statement. > > So the way I've defined T, T proves the soundness schema > for P. But T *cannot* prove its own soundness schema. There > is no consistent theory T (at least not with ordinary > first-order logic) that has an axiom saying > > (T proves S) -> S > > >It is just as compelling as the rest of them. > > What is just as compelling? This: T(F) --> F > >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. > > PA is *already* a specific, well-defined theory. If you > add axioms to it, you have formed a *new* theory, PA-plus. > Of course PA can't take advantage of these new axioms, > because they aren't axioms of PA. > > The same is true of a program P that proves theorems. > If P is sound, then the soundness schema for P is true, > but is not provable by P. You can certainly *modify* P > by adding the soundness schema, but then you've created > a *new* program, P'. > > >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. > > It's not that the machine cannot prove them *because* a contradiction > would result. Machines don't care whether they prove a contradiction > or not. > > Rather, the implication is this: *if* you construct > a theory that can prove its own soundness schema, > *then* that theory is inconsistent. > > -- > Daryl McCullough > Ithaca, NY
From: Newberry on 17 Nov 2007 12:11 On Nov 16, 8:07 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > >A couple of comments. Firstly, I do not know if the proof you are > >showing is the same as the manifest truth proof. > > I have no idea what you mean by "the manifest truth proof", > unless it is just the informal argument: > > Every axiom of PA is true. > Truth is preserved under logical deduction. > Therefore, every theorem of PA is true. > A contradiction can't be true. > Therefore, PA can't prove any contradictions. > > This proof can certainly be formalized. It just > can't be formalized in PA. 1) We can see that every axiom of PA is true. In you proof it is probably just an assumption. 2) The proof can be formalized in ZFC but we do not know if ZFC is consistent. So it may prove falsehoods. > > >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. > > No, it can't be formalized in PA, because there is no formula > in PA which says "S is a true sentence of arithmetic". What I meant is that we can say (Ex)(Px, #(F)) --> F leaving the T out. Yes, it is inconsistent. That is my point. But you claimed it was not the reason we put (Ex)(Px, #(F)) --> T(F) on the meta-level. > > >Did we put the axiom on a meta-level just to avoid the > >contradiction? > > We put it in at the meta-level because PA doesn't have > a truth predicate. > > >BTW, I do not understand this: > >S <-> T(#S), where #S means the Godel code of S. > >The Goedel number of S is true ... ? > > No, T(#S) doesn't say #S is true, it says "#S is the > Godel code of a true statement". What does it say then? > > -- > Daryl McCullough > Ithaca, NY
From: Daryl McCullough on 17 Nov 2007 13:26
Newberry says... > >On Nov 16, 8:07 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) >wrote: >> I have no idea what you mean by "the manifest truth proof", >> unless it is just the informal argument: >> >> Every axiom of PA is true. >> Truth is preserved under logical deduction. >> Therefore, every theorem of PA is true. >> A contradiction can't be true. >> Therefore, PA can't prove any contradictions. >> >> This proof can certainly be formalized. It just >> can't be formalized in PA. > >1) We can see that every axiom of PA is true. In you proof it is >probably just an assumption. > >2) The proof can be formalized in ZFC but we do not know if ZFC is >consistent. So it may prove falsehoods. So? >What I meant is that we can say >(Ex)(Px, #(F)) --> F >leaving the T out. >Yes, it is inconsistent. No, it's not inconsistent, if you are careful about it. >> >Did we put the axiom on a meta-level just to avoid the >> >contradiction? >> >> We put it in at the meta-level because PA doesn't have >> a truth predicate. >> >> >BTW, I do not understand this: >> >S <-> T(#S), where #S means the Godel code of S. >> >The Goedel number of S is true ... ? >> >> No, T(#S) doesn't say #S is true, it says "#S is the >> Godel code of a true statement". > >What does it say then? I just said it: T(#S) says "S is the code of a true statement". -- Daryl McCullough Ithaca, NY |