'When Are Relations Neither True Nor False?
in [Math]
|
From: Nam Nguyen on 28 Feb 2010 13:00 Aatu Koskensilta wrote: > 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. > Thanks, Aatu, for the information. I'll respond sometimes today or tomorrow.
From: Frederick Williams on 28 Feb 2010 13:09 Nam Nguyen wrote: > > 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". Aatu has reposted his description of an adequate system: primitive recursive arithmetic. A proof in that system will be entirely syntactic.
From: Frederick Williams on 28 Feb 2010 13:12 Nam Nguyen wrote: > 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? No. > > [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? No.
From: Nam Nguyen on 28 Feb 2010 13:31 Frederick Williams wrote: > Nam Nguyen wrote: > >> 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". > > Aatu has reposted his description of an adequate system: primitive > recursive arithmetic. Good then. We all have clarified that there are many _encoded_ formal systems and there's one purported _encoding_ ("proving"). We could now move the discussion forward. > A proof in that system will be entirely syntactic. We'll see if we can agree what is meant by "being syntactic" in this context, and overall we'll see whether or not Godel's proof in the encoding formal system is indeed syntactic in the agreed sense.
From: Aatu Koskensilta on 28 Feb 2010 13:32
Nam Nguyen <namducnguyen(a)shaw.ca> writes: > 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". G�del's proof isn't a formal proof in a formal system. It is an ordinary mathematical proof, presented originally in mathematical German. When people say it's entirely syntactic they're not claiming it's a formal proof -- we meet precious few formal proofs in mathematics, fortunately! -- but rather that it proceeds solely by way of reasoning about the syntactic form of formal expressions, formal structure of derivations, and so on, and doesn't involve e.g. model theoretic notions. As with any mathematical proof we can of course formalise the proof in any number of formal systems: primitive recursive arithmetic or even weaker fragments of arithmetic, Peano arithmetic, ZFC, Per Martin-L�f's constructive type theory, higher-order set theory with the axiom that the class of ordinals is weakly compact, what have you. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus |