'When Are Relations Neither True Nor False?
in [Math]
|
From: herbzet on 28 Feb 2010 01:10 Daryl McCullough wrote: > Newberry says... > > > >On Feb 25, 8:18=A0am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > >wrote: > >> Newberry says... > > >> >This is what Torkel Franzen said. Look, Frege also believed that the > >> >axioms in his system were manifestly true. > >> > >> Well, he was mistaken. The belief that a system is consistent > >> can be mistaken. > > > >Which of his axioms was not manifestly true? > > Unrestricted comprehension, which says if Phi(x) is a formula > with one free variable, then there is a set y such that forall > x, > > x is an element of y > <-> > Phi(x) > > This is clearly not true in the case Phi(x) is the formula > "x is an element of x". I think you mean: This is clearly not true in the case Phi(x) is the formula "x is *not* an element of x" for in that case y is the set of sets that are not elements of themselves, and therefore y is an element of y iff y is not an element of y. -- Mr. Nitpick
From: Frederick Williams on 28 Feb 2010 09:31 Nam Nguyen wrote: > > Frederick Williams wrote: > > Nam Nguyen wrote: > > > >> But how do we demonstrate by _pure syntactical mean_ this "proving" system > >> is consistent? The answer is we can't, and neither could Godel possible have. > > > > As I remarked, G\"odel had no need to: he assumed omega consistency > > which is defined syntactically. > > Right: that's what you said (and I didn't have a chance to make comment > the last time). > > OK syntactical proof means the entire proof is a _finite sequence_ > of _finite formulas_. So how did Godel manage to bring _infinitely_ > many constant-terms (i.e. numerals), which would be required for > encoding the concept of w-consistency, his "finite" proof? This will look a mess but, as I said before, you should read it for yourself. From van Heijenoort p 607: "Let kappa be any class of FORMULAS... kappa is said to be omega-consistent if there is no CLASS SIGN a such that (n)[Sb(a_{Z(n)}^v \in Flg(kappa)] & [Neg(v Gen a)] \in Flg(kappa) where v is the FREE VARIABLE of the CLASS SIGN a." Capitalized words indicate numerical predicates. > > > > I'll say it again Theorem VI (it's that which I'm talking about and > > nothing else) is stated and proved in purely syntactic terms. > > You just _said_ that but you've not proven it. Well I'm not G�del. In the words of the computer folk: read the flippin' manual. > Anybody could "say" > anything! > > > Furthermore the proof is carried out in the system P, that's G\"odel's > > P. You seem to say in your news:P_fin.119$QL4.116(a)newsfe24.iad that > > there are other possible P's. But I was taking about G\"odel's P. > > You should really read my recent post again where I said something > about ZF as an example of a P, about "proving" system, and about > what Godel himself said: > > >> We proceed now to the rigorous development of the proof sketched above, > >> and _begin by giving an exact description of the formal system P_, > >> _for which_ we seek to demonstrate the _existence of undecidable propositions_. > > (The highlight is mine). Do you understand now P is just _a_ system under > investigation, Yes. Roughly P = Principia + Peano arithmetic. > and not in general written in the language where he'd express > the formula such as "~Bew_c[(17 Gen r)] /\ ~Bew_c[Neg(17 Gen r)]"? Bew_c and Gen are defined via G�del numbering, all the relevant predicates are representable in P. > Why is so hard for you to understand the distinction between _a_ P and his > alleged "proving" formal system? See Aatu's news:87hbp3j3ka.fsf(a)dialatheia.truth.invalid for what a proof of G�del's theorem needs.
From: Nam Nguyen on 28 Feb 2010 11:45 Frederick Williams wrote: > Nam Nguyen wrote: >> Frederick Williams wrote: >>> Nam Nguyen wrote: >>> >>>> But how do we demonstrate by _pure syntactical mean_ this "proving" system >>>> is consistent? The answer is we can't, and neither could Godel possible have. >>> As I remarked, G\"odel had no need to: he assumed omega consistency >>> which is defined syntactically. >> Right: that's what you said (and I didn't have a chance to make comment >> the last time). >> >> OK syntactical proof means the entire proof is a _finite sequence_ >> of _finite formulas_. So how did Godel manage to bring _infinitely_ >> many constant-terms (i.e. numerals), which would be required for >> encoding the concept of w-consistency, his "finite" proof? > > This will look a mess but, as I said before, you should read it for > yourself. From van Heijenoort p 607: > > "Let kappa be any class of FORMULAS... kappa is said to be > omega-consistent if there is no CLASS SIGN a such that > > (n)[Sb(a_{Z(n)}^v \in Flg(kappa)] & [Neg(v Gen a)] \in Flg(kappa) > > where v is the FREE VARIABLE of the CLASS SIGN a." > > Capitalized words indicate numerical predicates. You missing understood my question: how did he prove that formula (the omega formula) in his proof using the "proving" formal system, which is different from P? A _proof in that "proving" system_ isn't the same as an _assumption in P_. Then again you fail to see the the distinction between the roles of the 2 systems, while ignore what I said about ZF as *one* example of a P that Godel's paper refers to. > >>> I'll say it again Theorem VI (it's that which I'm talking about and >>> nothing else) is stated and proved in purely syntactic terms. >> You just _said_ that but you've not proven it. > > Well I'm not G�del. In the words of the computer folk: read the > flippin' manual. > >> Anybody could "say" >> anything! >> >>> Furthermore the proof is carried out in the system P, that's G\"odel's >>> P. You seem to say in your news:P_fin.119$QL4.116(a)newsfe24.iad that >>> there are other possible P's. But I was taking about G\"odel's P. >> You should really read my recent post again where I said something >> about ZF as an example of a P, about "proving" system, and about >> what Godel himself said: >> >> >> We proceed now to the rigorous development of the proof sketched above, >> >> and _begin by giving an exact description of the formal system P_, >> >> _for which_ we seek to demonstrate the _existence of undecidable propositions_. >> >> (The highlight is mine). Do you understand now P is just _a_ system under >> investigation, > > Yes. Roughly P = Principia + Peano arithmetic. I emphasis "_a_" to indicate P in his paper is only *one of many examples* of formal system under investigation. You seem to ignore that (and my mentioning of ZF). Why? Let me ask you a simple question: is Godel's "Roughly P = Principia + Peano arithmetic" *the only system* that the results of his paper could be applied and, say, ZF is not? [Note: Godel himself did mention "set theory of Zermelo-Fraenkel" as one of "The most comprehensive formal systems"]. > >> and not in general written in the language where he'd express >> the formula such as "~Bew_c[(17 Gen r)] /\ ~Bew_c[Neg(17 Gen r)]"? > > Bew_c and Gen are defined via G�del numbering, all the relevant > predicates are representable in P. Iow, the formulas are written in the language of arithmetic, L(PA), as I already mention. Right? Let me repeat my question a moment ago: Is Godel's "Roughly P = Principia + Peano arithmetic" *the only system* that the results of his paper could be applied and, say, ZF is not? > >> Why is so hard for you to understand the distinction between _a_ P and his >> alleged "proving" formal system? > > See Aatu's news:87hbp3j3ka.fsf(a)dialatheia.truth.invalid for what a proof > of G�del's theorem needs. For whatever the reason, my Shaw ISP doesn't seem to allow me to access "news" so perhaps you just cite what you think as relevant here and I'll take a look and might make some comments about. I don't know what translation you have, but here's what I find in the one by R. B. Braithwaite: Thus Godel's two great theorems ... assert the 'unprovability' within P of certain well-formulas of P ... he indicates how similar proofs would apply to any calculus (formal system) satisfying two very general conditions [190], conditions so general that any calculus (formal system) capable of expressing arithmetic can hardly fail to satisfy them. [The text in parentheses are mine]. As I noted before, ZF is one formal system Godel himself mentioned (the other is PM). So apparently *_ZF_ can be* one system under investigation, and in such case, Frederick, would, say: Bew_c[(17 Gen r)] be written in L(ZF)? If your answer is yes, then it'd apparently be the case you misunderstood Godel's _proof_ completely. If your answer is no, then ZF is just one of (probably infinitely many) different formal systems GIT could be about. But what is the proving formal system whose language the formulas in his proof are written in? Apparently it's not L(ZF) - meaning the proving formal system is not ZF!
From: Aatu Koskensilta on 28 Feb 2010 12:09 Nam Nguyen <namducnguyen(a)shaw.ca> writes: > For whatever the reason, my Shaw ISP doesn't seem to allow me to access > "news" so perhaps you just cite what you think as relevant here and I'll > take a look and might make some comments about. I observed that inspecting G�del's proof (in excruciating detail) we find that it can be formalised in (the logic free formulation of) primitive recursive arithmetic. That is, taking Rosser's strengthening instead of G�del's original result, we have that we can explicitly write down primitive recursive function f, g and h such that (*) If e is a p.r. index of a set A of sentences in the language of arithmetic then f(e) is the code of a (Pi-1) formula R such that if x is the code of a proof of R from A + Robinson arithmetic then g(x) is the code of a proof of a contradiction from A + Robinson arithmetic; and if x is the code of a proof of the negation of R from A + Robinson arithmetic then h(x) is the code of a proof of a contradiction from A + Robinson arithmetic. can be proved using nothing but computation on open terms (involving functions defined by primitive recursion), propositional logic (applied to decidable predicates), and the induction rule P(0) P(a) --> P(a + 1) ------------------------ P(a) The statement (*) essentially asserts the functions f, g and h witness the claim Let A be a p.r. set of sentences in the language of arithmetic. Then the Rosser sentence of A + Robinson arithmetic is undecidable in A + Robinson arithmetic if A + Robinson arithmetic is consistent. This is standard stuff from proof theory. If you take an interest in these matters, Girard's _Proof Theory and Logical Complexity_ is an excellent source. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Nam Nguyen on 28 Feb 2010 12:25
Nam Nguyen wrote: > I don't know what translation you have, but here's what I find in the one > by R. B. Braithwaite: > > Thus Godel's two great theorems ... assert the 'unprovability' within > P of certain well-formulas of P ... he indicates how similar proofs > would apply to any calculus (formal system) satisfying two very general > conditions [190], conditions so general that any calculus (formal system) > capable of expressing arithmetic can hardly fail to satisfy them. > > [The text in parentheses are mine]. As I noted before, ZF is one formal > system Godel himself mentioned (the other is PM). So apparently *_ZF_ > can be* > one system under investigation, and in such case, Frederick, would, say: > > Bew_c[(17 Gen r)] > > be written in L(ZF)? > > If your answer is yes, then it'd apparently be the case you misunderstood > Godel's _proof_ completely. > > If your answer is no, then ZF is just one of (probably infinitely many) > different formal systems GIT could be about. But what is the proving formal > system whose language the formulas in his proof are written in? > > Apparently it's not L(ZF) - meaning the proving formal system is not ZF! Think of it this way. Godel himself said: P is essentially the [formal] system obtained by superimposing on the Peano axioms the logic of PM ... Are you saying that had Godel written: P is Zermerlo-Fraenkel set formal system then now you, I, and others would have never heard of Godel's _numbering_, hence would have never heard of Godel Incompleteness Theorem? You should really make this distinction: - P, PA, ZF, ZFC, ... are only systems his proof is _about_ - You believe there's a formal system his proof is _in_. If you don't really know what system his proof is _in_ then you failed to know what it means when you said GIT proof is "entirely syntactic ... proof". |