命题逻辑公理化.ppt

命题逻辑的公理化形式化与公理化此前我们讨论命题逻辑,是从语义角度,非形式化地、、:符号化,只有语法定义,:从初始符号串(公理)出发,根据符号变换规则,推导出其他符号串(定理).具体的公理化系统:语法+语义形式的公理化系统:,SJTU*形式系统的组成形式系统组成:初始符号:(wff定义):规定如何构成合法的符号串(wff).初始公式(公理):(推理规则):,即可进行推理,从老wff产生新的wff(定理).,SJTU*例:一个形式系统形式系统:初始符号:,,形成规则:,,:令x是任一串,系统有唯一公理(模式) A1:xx变形规则:令x,y,z表示任意串. R1:若xyz是定理,则xyz: (1) A1[x/] (2). (1)R1此系统有意义吗?试试这个解释:解释为+,解释为=.LuChaojun,SJTU*:初始符号表示有真假的命题及真值联结词;初始命题是重言式;从公理出发,利用推理规则,,,SJTU*命题逻辑公理系统初始符号命题符号:A,B,C,……联结词:,辅助符号:(,)可证符号:|(后接公式,表示该公式在系统中是可证明的)LuChaojun,SJTU*命题逻辑公理系统(续)形成规则(1)命题符号是公式;(2)若是公式,则是公式;(3)若和是公式,则是公式;(4),SJTU*命题逻辑公理系统(续)定义D1.定义为()D2.定义为D3.定义为()()作为初始符号,,SJTU*命题逻辑公理系统(续)公理A1.|(PP)PA2.|P(PQ)A3.|(PQ)(QP)A4.|(QR)((PQ)(PR))LuChaojun,SJTU*命题逻辑公理系统(续)变形规则(推理规则):若|,则|[p/]. (将公式中的某符号p处处代以公式,称为代入,结果记作[p/].):若|,|,则|.:施以置换后得到公式.若|,则|.LuChaojun,SJTU*