(¬Q→¬R) →(R →Q)
计算机学院
5
5
缩写公式
Q∨R=(¬Q→R) Q∧R=¬ (Q→¬R) Q↔R=(Q→R) ∧(R→Q) Q⊕R=¬ (Q↔R)
计算机学院
计算机学院
6
6
公式复杂度
公式Q的复杂度表示为FC(Q)
• 命题变元复杂度为0，如果 是命题变元，则FC (Q)=0。 命题变元复杂度为0 如果Q是命题变元 是命题变元， • 如果公式 ¬R，则FC (Q)=FC(R)+1。 如果公式Q=¬ ， 。 • 如果公式Q=R1→R2，则FC (Q)=max{FC(R1), FC(R2)}+1。 如果公式 。
定义了所有合式公式
计算机学院
3
3
命题逻辑的公理系统
有以下三个公理模式，其中P,Q,R可为任意公式 有以下三个公理模式，其中P,Q,R可为任意公式 P,Q,R
• 公理模式T1 公理模式T • 公理模式T2 公理模式T
–(P→ (Q→R)) →((P→Q) →(P→R)) (P –Q→ (R→Q) Q
定义3.2 是合式公式集, 定义3.2 设Γ是合式公式集, Q是 合式公式， 合式公式，有推理步骤A1,A2,…An， 公式序列α1, α2,… αn ，其中 公式序列α
• • • •
Γ称为推演的前提集， 称为推演的前提集， 前提集 称α为结论
A1=α1 A2=α2 An=αn
….
推理序列
(αn =Q) =Q)
• 命题变元p1,p2,…pn • 联结词符号¬，→; • 括号(,) 括号(,)
合式公式
• 命题变元是合式公式； 命题变元是合式公式； • 若Q是公式，则(¬Q)是合式公式； 是公式， 是合式公式； 是合式公式 计算机学院 • 若Q,R是公式，则(Q→R)是合式公式。 是合式公式。 Q,R是公式， 是公式 R)是合式公式
• 如果 如果Q 计算机学院 Q是公理或 Q ∈Γ，则Γ├ Q
则称它为Q 的一个推演 推演( 则称它为Q的从Γ的一个推演(演 Q。 绎),记为Γ├ Q。 计算机学院 9
9
证明与定理
如果存在从Γ推演出 ，则记为Γ├Q 。 如果存在从 推演出Q，则记为 推演出 {Q1,Q2,…Qn}├Q简记为 简记为 如果Γ为空集 则记为├Q。 如果 为空集∅ ，则记为 。 如果Γ├Q，并且有推理步骤A1,A2,…An， ，并且有推理步骤 如果 称为的一个证明 证明。 则A1,A2,…An称为的一个证明。 计算机学院 如果├Q ，则Q称为定理。 称为定理 如果 称为定理。
每个αk满足以下条件之一， 每个α 满足以下条件之一，
• (1) α是公理； α是公理 是公理； • (2) α k∈Γ； • (3) 有i,j<k αk= αi→ αj由αi, αj用MP规则 MP规则 推出。 推出。
推论： 推论：
• 如果推理步骤序列 是A1,A2,…An，则推 理序列长度n 理序列长度n。
计算机学院
A2 A1
A1=A2→A3 A1 A3=A4→A5
计算机学院
20
20
├¬¬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
主要内容
概述 命题逻辑公理系统 谓词逻辑公理系统 公理系统性质 理论与模型 判定问题 总结
计算机学院
计算机学院
1
1
逻辑公理系统
公理系统
• 从一些公理出发，根据演绎法，推导出一系列定理，形成的演绎体 从一些公理出发，根据演绎法，推导出一系列定理， 公理出发 演绎法 定理 系叫作公理系统 公理系统。 系叫作公理系统。
A2 计算机学院 5 = A4→A6 A
A6 = A3→A7
计算机学院
11
11
例：├(Q→R) →(Q→Q) → → A1=Q→ (R→Q) A3= (Q→R) →(Q→Q) A1 A2=A1→A3 A2= (Q→ (R→Q)) →((Q→R) →(Q→Q)) A2
计算机学院
计算机学院
12
12
重要定律
├ (P→(Q→R)) →(Q→(P→R)) → → → →
A3=((P → Q)→((Q→R)→(P→R))) 计算机学院 A1→ A3 A2= → → → →
计算机学院
19
19
├Q→Q
A1=(Q→ ((Q→Q)→Q))→((Q→(Q→Q)→(Q→Q) A2=Q→ ((Q→Q) →Q)) A3=(Q→ (Q→Q)) →(Q→Q) A4=Q→ (Q→Q) A5=Q→Q
–表达了肯定的所有命题。 表达了肯定的所有命题。 表达了肯定的所有命题
–推理规则是由公理及已证定理得出新定理的规则； 推理规则是由公理及已证定理得出新定理的规则； 推理规则是由公理及已证定理得出新定理的规则
计算机学院
计算机学院
2
2
命题逻辑的公理系统
定义3.1 命题逻辑的公理系统定义: 定义3.1 命题逻辑的公理系统定义: 符号
计算机学院
14
14
三段论
Q, Q→R ├R
A1= Q→R A2= Q A3= R A1∈ Γ A2∈ Γ A1=A2 → A3
计算机学院
计算机学院
15
15
传递律
P→Q,Q→R├P→R →
A1=(Q→R) →(P→ (Q→R)) A2=Q→R A3=P→ (Q→R) A4=(P→ (Q→R)) →((P→Q) →(P→R)) A5=(P→Q) →(P→R) A6=(P→Q) A7=(P→R) 计算机学院 A1 A2∈ Γ A1=A2 → A3 A2 A4=A3 → A5 A6∈ Γ A5=A6→A7
• 公理模式T3 公理模式T
–(¬Q →¬R) →(R→Q) (
推理规则(分离规则,MP规则) 推理规则(分离规则,MP规则) ,MP规则
• 从Q和Q→R推出R 推出R
–Q和Q→R称为前提 Q –R称为结论 R
计算机学院
计算机学院
4
4
公理系统
罗素公理系统 Q ∨ Q →Q Q →Q ∨ R Q ∨ R → R∨ Q (P→Q)→(P∨ (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→(R→Q) (P→(Q→R)) →((P→Q) →(P→R)) Q→¬¬Q 计算机学院
三段论： 三段论：Q, Q→R ├R 传递律： 传递律：P→Q,Q→R├P→R 反证律：如果 反证律：如果Γ, ¬Q├ R, Γ, ¬Q├¬R,则Γ├ Q ¬ 则 归谬律：如果 归谬律：如果Γ, Q├ R, Γ, Q├ ¬R，则Γ├ ¬Q ，
计算机学院
计算机学院
13
13
重要定理
├ (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 ¬ → → 计算机学院
公理系统的组成： 公理系统的组成：
• 符号集； 符号集； • 公式集
–公式是用于表达命题的符号串； 公式是用于表达命题的符号串； 公式是用于表达命题的符号串
• 公理集
–公理是用于表达推理由之出发的初始肯定命题； 公理是用于表达推理由之出发的初始肯定命题； 公理是用于表达推理由之出发的初始肯定命题
• 推理规则集 • 定理集
• Q1,Q2,…Qn ├Q
计算机学院
10
10
P, Q→(P→R)├Q→R A 1= P A2=P→ (Q→P) A3=Q→P A4= Q→(P→R) A5= (Q→(P→R))→((Q→P)→(Q→R)) A6= (Q→P)→(Q→R) A7= (Q→R) A1∈Γ
A1
A2 = A1 →A3 A4 ∈Γ
=(Q Q)→ Q→ (Q→ A3=(Q→(( P →Q)→(P →R))) →(( Q→( P →Q)) →(Q→(P →R)))
计算机学院
A1 A1 A8=A7→ A9 A6=A9→ A10
计算机学院
17
17
├(Q → R)→((P →Q) →(P→R)) → →
A1= (Q → R) →(P →(Q →R)) A2= (P→(Q →R)) → ((P →Q) →(P →R)) → A3= (Q → R)→((P →Q)→(P →R)) → →
A1 A2
A1, A2├ A3
计算机学院
计算机学院
18
18
├(P→Q)→((Q→R)→(P→R)) → → → → →