命题逻辑公理系统

计算机学院1计算机学院1主要内容概述命题逻辑公理系统谓词逻辑公理系统公理系统性质理论与模型判定问题总结计算机学院2计算机学院2逻辑公理系统公理系统•从一些公理出发，根据演绎法，推导出一系列定理，形成的演绎体系叫作公理系统。公理系统的组成：•符号集；•公式集–公式是用于表达命题的符号串；•公理集–公理是用于表达推理由之出发的初始肯定命题；•推理规则集–推理规则是由公理及已证定理得出新定理的规则；•定理集–表达了肯定的所有命题。计算机学院3计算机学院3命题逻辑的公理系统定义3.1命题逻辑的公理系统定义:符号•命题变元p1,p2,…pn•联结词符号，;•括号(,)合式公式•命题变元是合式公式；•若Q是公式，则(Q)是合式公式；•若Q,R是公式，则(QR)是合式公式。定义了所有合式公式计算机学院4计算机学院4命题逻辑的公理系统有以下三个公理模式，其中P,Q,R可为任意公式•公理模式A1–Q(RQ)•公理模式A2–(P(QR))((PQ)(PR))•公理模式A3–(QR)(RQ)推理规则(分离规则,MP规则)•从Q和QR推出R–Q和QR称为前提–R称为结论计算机学院5计算机学院5公理系统罗素公理系统QQQQQRQRRQ(PQ)(PRQR)弗雷格公理系统Q(RQ)(P(QR))((PQ)(PR))(P(QR))(Q(PR))(QR)(RQ)QQQQ卢卡西维茨公理系统Q(RQ)(P(QR))((PQ)(PR))(QR)(RQ)计算机学院6计算机学院6缩写公式QR=(QR)QR=(QR)QR=(QR)(RQ)QR=(QR)计算机学院7计算机学院7公式复杂度公式Q的复杂度表示为FC(Q)•命题变元复杂度为0，如果Q是命题变元，则FC(Q)=0。•如果公式Q=R，则FC(Q)=FC(R)+1。•如果公式Q=R1R2，则FC(Q)=max{FC(R1),FC(R2)}+1。计算机学院8计算机学院8推理序列已知Q成立，证明R→Q成立A1=Q(RQ)A1A2=QQΓA3=RQ推理序列•Γ=Q，公式集——前提•A1、A2、A3——推理序列•A3——结论计算机学院9计算机学院9演绎与推理序列定义3.2设Γ是合式公式集,Q是合式公式，有推理步骤A1,A2,…An，公式序列α1,α2,…αn，其中•A1=α1•A2=α2•….•An=αn(αn=Q)每个αk满足以下条件之一，•(1)α是公理；•(2)αkΓ；•(3)有i,jkαk=αiαj由αi,αj用MP规则推出。则称它为Q的从Γ的一个推演(演绎),记为Γ├Q。Γ称为推演的前提集，称α为结论推理序列•如果推理步骤序列是A1,A2,…An，则推理序列长度n。推论：•如果Q是公理或QΓ，则Γ├Q计算机学院10计算机学院10证明与定理如果存在从Γ推演出Q，则记为Γ├Q。{Q1,Q2,…Qn}├Q简记为•Q1,Q2,…Qn├Q如果Γ为空集，则记为├Q。如果Γ├Q，并且有推理步骤A1,A2,…An，则A1,A2,…An称为的一个证明。如果├Q，则Q称为定理。计算机学院11计算机学院11P,Q(PR)├QRA1=PA1ΓA2=P(QP)A1A3=QPA2=A1A3A4=Q(PR)A4ΓA5=(Q(PR))((QP)(QR))A2A6=(QP)(QR)A5=A4A6A7=(QR)A6=A3A7计算机学院12计算机学院12例：├(QR)(QQ)A1=Q(RQ)A1A2=(Q(RQ))((QR)(QQ))A2A3=(QR)(QQ)A2=A1A3计算机学院13计算机学院13重要定律三段论：Q,QR├R传递律：PQ,QR├PR反证律：如果Γ,Q├R,Γ,Q├R,则Γ├Q归谬律：如果Γ,Q├R,Γ,Q├R，则Γ├Q计算机学院14计算机学院14重要定理├(P(QR))(Q(PR))├(QR)((PQ)(PR))├(PQ)((QR)(PR))├QQ├QQ├QQ├(QR)(QR)├Q((QR)R)├(QR)(RQ)├(QR)(RQ)├(QR)(RQ)├Q(QR)├(QQ)(RQ)├(QQ)Q计算机学院15计算机学院15三段论Q,QR├RA1=QRA1ΓA2=QA2ΓA3=RA1=A2A3计算机学院16计算机学院16传递律PQ,QR├PRA1=(QR)(P(QR))A1A2=QRA2ΓA3=P(QR)A1=A2A3A4=(P(QR))((PQ)(PR))A2A5=(PQ)(PR)A4=A3A5A6=(PQ)A6ΓA7=(PR)A5=A6→A7计算机学院17计算机学院17├(P(QR))(Q(PR))A1=(P(QR))((PQ)(PR))A2A2=((PQ)(PR))(Q((PQ)(PR)))A1A3=(Q((PQ)(PR)))((Q(PQ))(Q(PR)))A2A4=((P(QR))((Q(PQ))(Q(PR))))A1,A2,A3├A4A5=((P(QR))((Q(PQ))(Q(PR))))((P(QR))(Q(PQ))(P(QR))(Q(PR)))A2A6=((P(QR))(Q(PQ))(P(QR))(Q(PR))A5=A4A6A7=Q(PQ)A1A8=(Q(PQ))((P(QR))(Q(PQ)))A1A9=(P(QR))(Q(PQ))A8=A7A9A10=(P(QR))(Q(PR))A6=A9A10计算机学院18计算机学院18├(QR)((PQ)(PR))A1=(QR)(P(QR))A1A2=(P(QR))((PQ)(PR))A2A3=(QR)((PQ)(PR))A1,A2├A3计算机学院19计算机学院19├(PQ)((QR)(PR))A1=(QR)((PQ)(PR))├(QR)((PQ)(PR))A2=((QR)((PQ)(PR)))((PQ)((QR)(PR)))├(P(QR))(Q(PR))A3=((PQ)((QR)(PR)))A2=A1A3计算机学院20计算机学院20├QQA1=(Q((QQ)Q))((Q(QQ)(QQ)A2A2=Q((QQ)Q))A1A3=(Q(QQ))(QQ)A1=A2A3A4=Q(QQ)A1A5=QQA3=A4A5计算机学院21计算机学院21├QQ•A1=Q(QQ)A1•A2=(QQ)(QQ)A3•A3=(QQ)(QQ)A3•A4=Q(QQ)A1,A2,A3├A4•A5=(Q(QQ))•((QQ)(QQ))A2•A6=(QQ)(QQ)A5=A4A6•A7=(QQ)├QQ•A8=QQA6=A7A8计算机学院22计算机学院22├QQA1=(QQ)(QQ)A3A2=(QQ)├QQA3=(QQ)(QQ)A3A4=QQA3=A2A4计算机学院23计算机学院23├(QR)(QR)A1=RR├QQA2=(RR)(Q(RR))A1A3=Q(RR)A2=A1A3A4=(Q(RR))((QR)(QR))A2A5=(QR)(QR)A4=A3A5A6=QQ├QQA7=(QQ)((QR)(QR))├(PQ)((QR)(PR))A8=(QR)(QR)A7=A6A8A9=(QR)(QR)A8,A5├A9计算机学院24计算机学院24├Q((QR)R)A1=(QR)(QR)├QQA2=((QR)(QR))(Q((QR)R))├(P(QR))(Q(PR))A3=Q((QR)R)A2=A1A3计算机学院25计算机学院25├(QR)(RQ)A1=(QR)(QR)├(QR)(QR)A2=(QR)(RQ)A3A3=(QR)(QR)A2=A1A3计算机学院26计算机学院26├(QR)(RQ)A1=(QR)(RQ)├(QR)(RQ)A2=QQ├QQA3=(QQ)((RQ)(RQ))├(QR)((PQ)(PR))A4=(RQ)(RQ)A3=A2A4A5=(QR)(RQ)A1,A4├A5计算机学院27计算机学院27├(QR)(RQ)A1=(QR)(RQ)A3A2=(QQ)((QR)(QR))├(PQ)((QR)(PR))A3=(QQ)├(QQ)A4=(QR)(QR)A2=A3A4A5=(QR)(RQ)A4,A1├A5计算机学院28计算机学院28├Q(QR)(涵义)A1=Q(RQ)A1A2=(RQ)(Q→R)A3A3=Q(QR)A1，A2├A3计算机学院29计算机学院29├(QQ)(RQ)A1=Q(RQ)A1A2=(RQ)(QR)A3A3=Q(QR)A1,A2├A3A4=(Q(QR))((QQ)(QR))A2A5=(QQ)(QR)A4=A3A5A6=(QR)(RQ)A3A7=(QQ)(RQ)A5,A6├A7计算机学院30计算机学院30├(QQ)QA1=(QQ)((QQ)Q)├(QQ)(RQ)A2=((QQ)((QQ)Q))(((QQ)(QQ))((QQ)Q)))A2A3=((QQ)(QQ))((QQ)Q)A2=A1A3A4=(QQ)(QQ)A1A5=(QQ)QA3=A4A5计算机学院31计算机学院31├QRQA1=Q(RQ)A1A2=QRQQR=(QR)计算机学院32计算机学院32├QRRQA1=(RQ)(QR)├(RQ)(QR)A2=((RQ)(QR))((QR)(RQ))├(RQ)(QR)A3=(QR)(RQ)QR=(QR)A4=QRRQ计算机学院33计算机学院33├QRQA1=Q(RQ)A1A2=(RQ)(QR)├(QR)(RQ)A3=Q(QR)A1,A2├A3A4=(Q(QR)))(