FoundationsofLogic (12).pdf
《FoundationsofLogic (12).pdf》由会员分享,可在线阅读,更多相关《FoundationsofLogic (12).pdf(31页珍藏版)》请在得力文库 - 分享文档赚钱的网站上搜索。
1、PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)Online Course:Foundations of LogicLecture 13:ArithmetizationMarch 30,2020Dag Westerst ahlTsinghua LogicPlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)PlanNow finally we have enough things in place to
2、 carry through theproofs of G odels incompleteness theorems.The main ideas were alreadyoutlined in Chapter 7.Recall that we are working on three levels:(1)Claims about first-order theories:their symbols,terms and formulas,proofs(derivations),theorems.(2)Via G odel numbering(coding),these become clai
3、ms about naturalnumbers,e.g.that the number m is the G odel number of a proof ina theory T of a sentence with number n.(3)Then we can translate(some of)these claims back into PA,so that(hopefully)some true claims translate to theorems of PA.Ok,but whats the point?We can now(hopefully)find a sentence
4、 G inPA which,via the translation,says“I am not provable in T”.Then theargument outlined before should show that G is undecidable in T.1 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)G odel numbering:symbolsWe assign the following numbers to all symbols:u()=00+vidi#(
5、u)135791113 15171923i+125i+1Other logical symbols can be regarded as defined.(d0,d1,.is the list ofspecial individual constants that are used as parameters in derivations.)All symbols get odd numbers,except that the infinitely many variablesv0,v1,v2,.get special numbers(and similarly for the extra p
6、arameters).2 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)G odel numbering:symbol stringsThen we use our sequence coding functions hikto give G odel numbersto finite strings of symbols:If u0u1.uk1is a string of symbols,then#(u0u1.uk1)=h#(u0),#(u1),.,#(uk1)ikIn other
7、 words:#(u0u1.uk1)=2#(u0)+1 3#(u1)+1.(k1)#(uk1)+1Example:What is the G odel number of 0 6=1,that is,of 0=00?NB Officially,this formula is written=000.See p.214 to see you gotit right.Example:What is the G odel number of v5v2=v5,i.e.of v5=v2v5?3 of 30PlanG odel numberingCoded relationsSubstitutionPro
8、ofsThe formula PrfT(x,y)G odel numbering:sequences of symbol stringsFinally,we number sequences of symbol strings(such as proofs)in thesame way:If(s0,s1,.,sk1)is a sequence of symbol strings,then#(s0,s1,.,sk1)=h#(s0),#(s1),.,#(sk1)ikThe G odel numbers of the symbols 0,v0,v1,.,d0,d1,.are distinctfrom
9、 the G odel numbers of the terms consisting of the strings with justthat symbol as an element.E.g.in the case of 0,as a symbol,#(0)=13,but as a term,it is 213+1.Likewise the number of a sentence,i.e.#(),is distinct from thenumber of the derivation consisting of just that one sentence,whosenumber wil
10、l be 2#()+1.(For example,if is a logical axiom.)That actually captures a reasonable intuition.4 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)G odel numbering in generalThere are many ways to code syntactic objects as numbers.An acceptable coding should have the foll
11、owing properties:IDifferent syntactic objects should have different code numbers:thefunction#is injective.IThere is an effective way to find the code number of each syntacticobject.IFor any number n,there is an effective way to determine if it is thecode number of some syntactic object,and in that c
12、ase to find thatobject.FactThe G odel numbering just given is acceptable in this sense.Proof.Use the Fundamental Theorem of Arithmetic.5 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)Properties of syntactic objects become properties of numbers 1For example:(a)var(n)n
13、 is the G odel number of a variable(b)term(n)n is the G odel number of a term(in LPA)(c)fml(n)n is the G odel number of a formula(d)sent(n)n is the G odel number of a sentence(e)logax(n)n is the G odel number of a logical axiom(f)axT(n)n is the G odel number of an axiom in T(g)prfT(m,n)m is the G od
14、el number of a proof in T of thesentence with G odel number nWe will check that(a)(e),and some other relations and functions,areprimitive recursive,and that if axTis primitive recursive,then so is prfT.6 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)Properties of syn
15、tactic objects become properties of numbers 2We start with some simple cases:var(n)n is(the G odel number of)a variable termn=h23i+1i for some iiinn=h23i+1iSo we see that var is primitive recursive.Next,recall the concatenation function:ha0,.,ak1i hb0,.,bm1i=ha0,.,ak1,b0,.,bm1i(We often skip the sup
16、erscript k on ha0,.,ak1ik.)7 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)Properties of syntactic objects become properties of numbers 3More easy cases:neg(n)=the negation of n(i.e.the number of the result of placing in front of the string with number n)=impl(n,m)=t
17、he implication from n to m=exquant(j,n)=the result of placing vjin front of the stringwith number n=So if,are formulas,neg(#()is the G odel number of the formula,impl(#(),#()of(),and exquant(j,#()of vj.8 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)TermsRecall:t is
18、a term(in LPA)ifft is 0 ort is a variable or a parameter ort is0t1for some term t1ort is+t1t2for some terms t1,t2ort is t1t2for some terms t1,t2This is essentially a definition of terms by course-of-values induction:term(n)9 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(
19、x,y)FormulasAtomic LPA-formulas have the form s=t,where s,t are terms.Thus:atom(n)So atom is primitive recursive.Next:fml(n)n is the G odel number of a formula10 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)Free variables:informallyTo define the set of(G odel number
20、s of)sentences we must firstdeal with free occurrences of variables in formulas.In Chapter 2,we gave the following Definition 2.2.1:An occurrence of a variable x in an L-formula is free,if it isnot within the scope of any quantifier expression x or xin.Dealing formally with occurrences is a bit mess
21、y.On p.25 there isan inductive definition which doesnt mention occurrences.11 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)Free variables:formally(p.25)We include occurrences of variables in terms too(though“free”has nomeaning then).x occurs free in x.x occurs free
22、in Pt1.tn(or ft1.tn)if x occurs free in some oft1,.,tn.x occurs free in if x occurs free in.x occurs free in()if x occurs free in or in.x occurs free in y if x occurs free in and y is a variable distinctfrom x.One can show that this gives the same result as the earlier definition interms of occurren
23、ces and scopes.12 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)Free variables:primitive recursiveThis definition translates via the G odel numbering as follows:oc-free(j,n)vjoccurs free in(the term or formula with number)nn=h2 3j+1immnsubterm(m,n)oc-free(j,m)mmnkknt
24、erm(m)term(k)n=h11imk(oc-free(j,m)oc-free(j,k)mmnfml(m)n=neg(m)oc-free(j,m)mmnkknfml(m)fml(k)n=impl(m,k)(oc-free(j,m)oc-free(j,k)mmniinfml(m)n=exquant(i,m)i 6=j oc-free(j,m)Again,this is course-of-values recursion,so oc-free is primitive recursive.13 of 30PlanG odel numberingCoded relationsSubstitut
25、ionProofsThe formula PrfT(x,y)SentencesAnd now we can check that the property of being(the G odelnumber of)a sentence is primitive recursive:sent(n)n is the G odel number of a sentence14 of 30PlanG odel numberingCoded relationsSubstitutionProofsThe formula PrfT(x,y)SubstitutionOne more thing needs t
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- FoundationsofLogic 12 12
限制150内