Torkel Franzen on truth
in [Logic]
|
From: Newberry on 20 Nov 2007 22:36 On Nov 20, 6:30 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > > > >On Nov 19, 11:34 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> >Do you mean that there is no such extension of PA (classical logic > >> >with Peano axioms) or do you mean there is no such extension of ANY > >> >theory capable of arithmetic. > > >> I mean the latter, but I'm not sure about the distinction you > >> are making. It's hard to see how something could be "capable > >> of arithmetic" without being an extension of PA (or at least > >> an extension of Robinson arithmetic). > > >When you say "arithmetic" what do you mean by that? > > For me, to say that a theory is capable of arithmetic means > that it can prove the following theorems: > > 1. Ax x+0 = x > 2. Ax Ay x+(y+1) = (x+y) + 1 > 3. Ax x * 0 = 0 > 4. Ax x * (y+1) = (x*y) + x > 5. Ax ~ ((x+1)=0) > 6. Ax Ay ((x+1) = (y+1) -> x=y) > > >And what do you mean by "PA"? > > Basically, axioms 1-6 together with the induction schema: > > Phi(0) & (Ax (Phi(x) -> Phi(x+1))) -> Ax (Phi(x)) > Do we have to prove 1+0 = 1 v 1 = 0 ? (1) or ~(1+0 # 1 & 1 = 1) (2) ? What if we are able to prove only 1+0 = 1 (3) ~(1+0 # 1) (4) but not (1), (2)? Is it still Peano arithmetic? > >"Peano arithmetic" or a specific formal system = > >classical logic + Peano axioms"? What if we do not use classical > >logic? Is it still Peano arithmetic? Is it still "arithmetic"? > > You can use the same axioms for intuitionistic arithmetic. > The distinction is not really important for discussing > Godel's theorem. > > >> >If you mean the later then I think it is > >> >not true. > > >> Yes, it is. That's what Godel's second incompleteness theorem > >> proves: If T_ultimate is consistent, then it cannot prove its > >> own consistency. > > >Even Aatu Koskensilta posted a contribution not to long ago where he > >concedes that the 2-nd theorem depends on the particulars of the > >formal system. > >I have never seen a proof of "Any conceivable formal > >system capable of arithmetic (representing all p.r. functions) > >cannot prove its own consistency." > > I'm not sure what Aatu meant, but if you define consistency of > a theory T via the provability predicate, > > Con(#T) == Ax ~Pr(#T,x,#0=1) > > "there does not exist a proof of 0=1 from the axioms of T", > then if T is capable of proving some routine facts about > arithmetic (I'm not sure whether induction is needed or not) > then it follows that if T proves Con(#T), then T is inconsistent. > > -- > Daryl McCullough > Ithaca, NY
From: Newberry on 20 Nov 2007 22:43 On Nov 20, 8:58 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > >On Nov 20, 6:38 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >"T(F)" means "F is true" > > Well, there is no such formula that means "F is true" > for *arbitrary* F. You can restrict yourself to a specific > language L and introduce a predicate T(F) with the interpration > that T(F) holds if F is a true formula of language L, but > as proved by Tarski, the predicate T cannot be in the language > L. I never said it was in the language of L. It is in the meta-langage. > > >> >I did not say that it was in the language of PA. I said that > >> >T(F) --> F > >> >is just as compelling as any other axiom. > > >> Axiom for *what*? > > >If a sentence F is true then F. > > I meant: axiom for what theory? For any sentence in any theory "if a sentence F is true then F" is intuitively self-evident. It is at least as compelling as "truth cannot be inconsistent with itself."
From: Daryl McCullough on 21 Nov 2007 09:23 Newberry says... > >On Nov 20, 8:58 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) >wrote: >> Well, there is no such formula that means "F is true" >> for *arbitrary* F. You can restrict yourself to a specific >> language L and introduce a predicate T(F) with the interpration >> that T(F) holds if F is a true formula of language L, but >> as proved by Tarski, the predicate T cannot be in the language >> L. > >I never said it was in the language of L. It is in the meta-langage. Well, in the meta-language the schema is just plain vaccuously true. >For any sentence in any theory "if a sentence F is true then F" is >intuitively self-evident. I would say that it is true by definition. "F is true" means the same thing as F. But now I've lost track of what you are claiming follows from this schema. -- Daryl McCullough Ithaca, NY
From: Daryl McCullough on 21 Nov 2007 09:27 Newberry says... > >On Nov 20, 6:30 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) >wrote: >> Newberry says... >> >> >> >> >On Nov 19, 11:34 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) >> >wrote: >> >> >Do you mean that there is no such extension of PA (classical logic >> >> >with Peano axioms) or do you mean there is no such extension of ANY >> >> >theory capable of arithmetic. >> >> >> I mean the latter, but I'm not sure about the distinction you >> >> are making. It's hard to see how something could be "capable >> >> of arithmetic" without being an extension of PA (or at least >> >> an extension of Robinson arithmetic). >> >> >When you say "arithmetic" what do you mean by that? >> >> For me, to say that a theory is capable of arithmetic means >> that it can prove the following theorems: >> >> 1. Ax x+0 = x >> 2. Ax Ay x+(y+1) = (x+y) + 1 >> 3. Ax x * 0 = 0 >> 4. Ax x * (y+1) = (x*y) + x >> 5. Ax ~ ((x+1)=0) >> 6. Ax Ay ((x+1) = (y+1) -> x=y) >> >> >And what do you mean by "PA"? >> >> Basically, axioms 1-6 together with the induction schema: >> >> Phi(0) & (Ax (Phi(x) -> Phi(x+1))) -> Ax (Phi(x)) >> > >Do we have to prove >1+0 = 1 v 1 = 0 ? (1) >or >~(1+0 # 1 & 1 = 1) (2) >? You don't have to prove anything. I don't understand what you are asking. >What if we are able to prove only >1+0 = 1 (3) >~(1+0 # 1) (4) >but not (1), (2)? Is it still Peano arithmetic? As I said, Peano arithmetic is a specific theory. I suppose there are minor variants that would still be considered Peano arithmetic, but giving up (1) seems pretty major to me. But I don't understand what you are getting at. -- Daryl McCullough Ithaca, NY
From: Newberry on 21 Nov 2007 10:08
On Nov 21, 6:27 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Newberry says... > > > > > > > > >On Nov 20, 6:30 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> Newberry says... > > >> >On Nov 19, 11:34 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >> >wrote: > >> >> >Do you mean that there is no such extension of PA (classical logic > >> >> >with Peano axioms) or do you mean there is no such extension of ANY > >> >> >theory capable of arithmetic. > > >> >> I mean the latter, but I'm not sure about the distinction you > >> >> are making. It's hard to see how something could be "capable > >> >> of arithmetic" without being an extension of PA (or at least > >> >> an extension of Robinson arithmetic). > > >> >When you say "arithmetic" what do you mean by that? > > >> For me, to say that a theory is capable of arithmetic means > >> that it can prove the following theorems: > > >> 1. Ax x+0 = x > >> 2. Ax Ay x+(y+1) = (x+y) + 1 > >> 3. Ax x * 0 = 0 > >> 4. Ax x * (y+1) = (x*y) + x > >> 5. Ax ~ ((x+1)=0) > >> 6. Ax Ay ((x+1) = (y+1) -> x=y) > > >> >And what do you mean by "PA"? > > >> Basically, axioms 1-6 together with the induction schema: > > >> Phi(0) & (Ax (Phi(x) -> Phi(x+1))) -> Ax (Phi(x)) > > >Do we have to prove > >1+0 = 1 v 1 = 0 ? (1) > >or > >~(1+0 # 1 & 1 = 1) (2) > >? > > You don't have to prove anything. I don't understand > what you are asking. > > >What if we are able to prove only > >1+0 = 1 (3) > >~(1+0 # 1) (4) > >but not (1), (2)? Is it still Peano arithmetic? > > As I said, Peano arithmetic is a specific theory. > I suppose there are minor variants that would still > be considered Peano arithmetic, but giving up (1) seems > pretty major to me. > > But I don't understand what you are getting at. The question is if any conveivable theory capable of artithmetic is unable to prove its own consistency. Let's say we give up (1) and (2) and they become undecidable. OK, let's not call it Peano arithmetic. But why exactly do we need (1), (2)? And let's take it a step further. If for some predicate F we can prove ~(Ex)Fx do we also have to prove ~(Ex)(Fx & Gx)? For example if we prove ~(Ex)(x+0 # x) (5) do we also need to prove ~(Ex)((x+0 # x) & (x = x)) (6) ? When we are able to prove (5) why do we have to prove (6)? Will we lose any knowledhe of arithmetic if (6) is undecidable? |