模态命题逻辑.pptVIP

模态命题逻辑 必然命题 不可能命题 可能命题 模态命题语言L pm L pm是模态命题逻辑的形式语言，是对L p的扩充。 L pm是符号的集合 命题符号：p q r … 联结符号： 标点符号：（ ） 模态算子符号： L L pm的含义本质上不涉及语义，而只有语法。 公式集的归纳定义 L pm中表达式定义与L p相同 研究对象必须符合语法 原子公式集Atom(L pm)= Atom(L p)={U|U是由单个命题符号构成的表达式} 合式公式集Form(L pm) i） Atom(L pm)?Form(L pm) ii）若A∈Form(L p)，则(﹁A)， (LA)∈Form(L pm) iii）若A，B∈Form(L pm)，则(A*B)∈Form(L pm)。其中*表示∧，∨，→，?中的任何一个 iv）A是能由有限次应用i）—iii）形成的表达式 iff A∈Form(L pm) 模态命题逻辑的推演规则（一） A，B，C为公式 (Ref) A├A (+)若∑├A， 则∑， ∑’├A (﹁-)若∑， ﹁A ├B， ∑ ， ﹁A ├﹁B， 则∑├A (→-)若∑├A→B， ∑ ├A， 则∑├B (→+)若∑，A├B， 则∑├A→B (∧-)若∑├A∧B， 则∑├A， ∑├B 模态命题逻辑的推演规则（二） 记(MA)=(?(L(?A))) 简记(MA)、(?(L(?A)))、 (LA)分别为MA、?L?A、 LA A，B，C为公式 (L-)若∑├LA， 则∑├A (→-(L))若∑├L(A→B)， ∑ ├LA， 则∑├LB (L+)若Ф├A， 则Ф├LA (L+L)若∑├LA， 则∑├LLA ， (L+M)若∑├MA， 则∑├LMA 模态命题逻辑的自然推理系统 T系统 经典11条规则 (L-)、(→-(L))、(L+) S4系统 经典11条规则 (L-)、(→-(L))、(L+) (L+L) S5系统 经典11条规则 (L-)、(→-(L))、(L+) (L+L) (L+M) T(S4，S5)形式可证明， T(S4，S5)协调， T(S4，S5)极大协调。 三种系统的关系 若∑├TA，则∑├S4A。 若∑├S4A，则∑├S5A。 逆命题不成立。 证明：若A├TB，则LA├TLB。 证： (1) A├TB (已知) (2) Ф├T A→B (→+)(1) (3) Ф├T L(A→B) (L+)(2) (4) LA├T L(A→B) (+)(3) (5) LA├T LA (Ref) (6) LA├T LB (→-(L))(4)(5) 证明A├TMA。 证： (1) L?A├T L?A (Ref) (2) L?A├T ?A (L-)(1) (3) A，L?A├T ?A (+)(2) (4) A，L?A├T A (∈) (5) A├T ?L?A (?+)(3)(4) 证明L?A├T ?MA。 证： (1) L?A，MA ├T L?A (∈) (2) L?A ，MA ├T ?L?A (∈) (3) L?A├T ?MA (?+)(1)(2) 证明 ?MA ├T L?A 。 证： (1) ?L?A， ?MA ├T ? ? L?A (∈) (2) ?L?A， ?MA ├T ?L?A (∈) (3) ?MA ├T L?A (?-)(1)(2) 证明L(A→B)， L(B→A)├TLA →LB 。 证： (1) L(A→B)， L(B→A)，LA├TLA (∈) (2) L(A→B)， L(B→A)，LA├TL(A→B) (∈) (3) L(A→B)， L(B→A)，LA├TLB (→-(L))(1)(2) (4) L(A→B)， L(B→A)├TLA →LB (→+)(3) 证明MMA├S4MA。 证： (1) ?MA ├S4 L?A (已证) (2) L?A ├S4 LL?