命题逻辑完备性定理证明

10/18 07:15
阅读数 4

参考:《数学家的逻辑》

命题逻辑中包含了对字符串的一系列操作,命题逻辑的完备性是指在逻辑语义上任意重言式(即定理)一定可以被字符串的操作表示出来。

定义

  1. 字符集: { ¬ , → , ( , ) , p 1 , p 2 , p 3 , ⋯   } \{\neg,\rightarrow,(,),p_1,p_2,p_3,\cdots\} { ¬,,(,),p1,p2,p3,}

    1. 字符集是无穷集
  2. w f . ( well-formed formula ) wf.(\text{well-formed formula}) wf.(well-formed formula)集合:所有合法字符串集。合法的字符串满足如下性质:

    1. ∀ i , p i ∈ w f . \forall i,p_i \in wf. i,piwf.
    2. ∀ A , B \forall A,B A,B ( ¬ A ) ∈ w f . , ( A → B ) ∈ w f . (\neg A) \in wf.,(A\rightarrow B) \in wf. (¬A)wf.,(AB)wf.
    3. 所有的 w f . wf. wf.均由1. 2.两条性质产生。
  3. 公理模式:

    1. ( L 1 ) (L_1) (L1) ( A → ( B → A ) ) (A\rightarrow (B\rightarrow A)) (A(BA))
    2. ( L 2 ) (L_2) (L2) ( ( A → ( B → C ) ) → ( ( A → B ) → ( A → C ) ) ) ((A \rightarrow(B \rightarrow C))\rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))) ((A(BC))((AB)(AC)))
    3. ( L 3 ) (L_3) (L3) ( ( ( ¬ A ) → ( ¬ B ) ) → ( B → A ) ) (((\neg A) \rightarrow (\neg B)) \rightarrow (B \rightarrow A)) (((¬A)(¬B))(BA))
    4. 上述三条为公理模式,带入任意 w f . wf. wf.中字符串形成一条公理,因此公理有无数条。不妨将所有公理构成的集合记为 S 0 S_0 S0
  4. 演绎规则:若 A , ( A → B ) A ,(A\rightarrow B) A,(AB),则 B B B.

    1. 上面四条定义构成了形式系统 L L L S 0 S_0 S0是该形式系统内的公理集合。
  5. 证明:一个 w f . wf. wf.中序列: A 1 , A 2 , ⋯   , A n A_1,A_2,\cdots,A_n A1,A2,,An。满足如下条件:

    1. 有限长。
    2. ∀ i , A i ∈ S 0 \forall i, A_i \in S_0 i,AiS0,或 ∃ j , k < i \exists j,k < i j,k<i, A j = B → A i , A k = B A_j=B\rightarrow A_i,A_k=B Aj=BAi,Ak=B。(即 A n A_n An是通过演绎规则所得)。
    3. 将满足条件的 A n A_n An称为 L L L中的定理,所有定理构成的集合记为 S S S,显然 S 0 ⊂ S S_0 \subset S S0S。如果 A A A L L L的定理,则记为 ⊢ L A \vdash_LA LA
  6. 推演:将证明中的第二条件改为 ∀ i , A i ∈ S 0 ∪ Γ , Γ ⊂ w f . \forall i,A_i \in S_0 \cup \Gamma, \Gamma \subset wf. i,AiS0Γ,Γwf.,记为 Γ ⊢ L A \Gamma \vdash_L A ΓLA

  7. 赋值: v : w f . ↦ { T , F } v:wf. \mapsto\{T,F\} v:wf.{ T,F},满足如下两个条件:

    1. ∀ A ∈ w f . , v ( A ) ≠ v ( ¬ A ) \forall A \in wf., v(A)\neq v(\neg A) Awf.,v(A)=v(¬A)
    2. ∀ A , B ∈ w f . , v ( A → B ) = F ⇔ v ( A ) = T , v ( B ) = F \forall A,B \in wf., v(A \rightarrow B)=F \Leftrightarrow v(A)=T,v(B)=F A,Bwf.,v(AB)=Fv(A)=T,v(B)=F
  8. 重言式: ∀ \forall 赋值 v v v, v ( A ) = T v(A)=T v(A)=T,则称 A A A是重言式。

推导

  1. { A , ( B → ( A → C ) ) } ⊢ L ( B → C ) \{A,(B\rightarrow (A \rightarrow C))\} \vdash_L (B \rightarrow C) { A,(B(AC))}L(BC)
    在这里插入图片描述

  2. 演绎定理: Γ ∪ { A } ⊢ L B ⇔ Γ ⊢ L ( A → B ) \Gamma \cup \{A\} \vdash_L B \Leftrightarrow \Gamma \vdash_L (A \rightarrow B) Γ{ A}LBΓL(AB)
    证明: 对推演序列的长度用归纳法,详见P43.

  3. 假言三段论: ∀ A , B , C ∈ w f . , { ( A → B ) , ( B → C ) } ⊢ L ( A → C ) \forall A,B,C \in wf., \{(A\rightarrow B),(B \rightarrow C)\} \vdash_L (A \rightarrow C) A,B,Cwf.,{ (AB),(BC)}L(AC)
    证明:利用演绎定理。

  4. ⊢ L ( ¬ B → ( B → A ) ) , ⊢ L ( ( ¬ A → A ) → A ) \vdash_L (\neg B \rightarrow (B \rightarrow A)),\vdash_L((\neg A \rightarrow A) \rightarrow A) L(¬B(BA))L((¬AA)A)
    证明:见P47.

完备性证明

可靠性定理

∀ A ∈ S , A 是 重 言 式 \forall A \in S,A是重言式 AS,A

证:对 A ∈ S 0 A \in S_0 AS0,用真值表验证。对 ( B → A ) , B ⊢ L A (B \rightarrow A),B \vdash_L A (BA),BLA,由前两个公式是重言式可推导出 A A A也是重言式(用赋值的条件2)。

L L L的扩张、相容扩张、相容完全扩张

S 0 S_0 S0中添加新的公理,得到 L L L的扩张 L ∗ L^* L,相应的定理集为 S ∗ S^* S

说扩张 L ∗ L* L是相容的,指 ∀ A ∈ w f . \forall A\in wf. Awf., A , ¬ A A,\neg A A,¬A不同时属于 S ∗ S^* S

说扩张 L ∗ L^* L是完全的,指 ∀ A ∈ w f . \forall A \in wf. Awf. A , ¬ A A,\neg A A,¬A必有一者属于 S ∗ S^* S

相容完全:相容且完全

定理: L L L是相容的。
证明: 否则存在 A A A, ⊢ L A , ⊢ L ¬ A \vdash_LA,\vdash_L \neg A LA,L¬A,由可靠性定理 A , ¬ A A,\neg A A,¬A均是重言式,与赋值的定义矛盾。

定理:若 L ∗ L^* L不相容,则 ∀ A ∈ w f . , ⊢ L ∗ A \forall A\in wf., \vdash_{L^*}A Awf.,LA
证明:设 ⊢ L ∗ B , ⊢ L ∗ ¬ B \vdash_{L^*}B,\vdash_{L^*}\neg B LB,L¬B,由推导4, ⊢ L ( ¬ B → ( B → A ) ) \vdash_L (\neg B \rightarrow (B \rightarrow A)) L(¬B(BA)),运用两次演绎规则可得 A A A.

相容扩张的合法性

定理:设 L ∗ L^* L L L L的相容扩张, ∀ A ∈ w f . , A ∉ S ∗ \forall A \in wf., A \not \in S^* Awf.,AS,将 ¬ A \neg A ¬A加入 L ∗ L^* L的公理集合得到的扩张 L ∗ ∗ L^{**} L是相容的。
证明:如果不相容,则有 ⊢ L ∗ ∗ A \vdash_{L^{**}}A LA,即 ( ¬ A ) ⊢ L ∗ A ⇔ ⊢ L ∗ ( ¬ A → A ) (\neg A)\vdash_{L^*}A \Leftrightarrow \vdash_{L^*}(\neg A \rightarrow A) (¬A)LAL(¬AA),结合前面定理可知 ⊢ L ∗ A \vdash_{L^*}A LA,矛盾。

相容完全扩张的存在性

定理: 设 L ∗ L^* L L L L的相容扩张,则存在 L ∗ L^* L的相容完全扩张。
证明:
首先证明 w f . wf. wf.可列,这是因为长度固定的 w f . wf. wf.的数目是可数的。不妨设该序列为 A 1 , A 2 , ⋯   , A n , ⋯ A_1,A_2,\cdots,A_n,\cdots A1,A2,,An,。依次判断 A i A_i Ai是否为 L ∗ L^* L定理,如果不是,得到新的扩张 L ∗ ∗ L^{**} L,依次执行上述过程得到 L ∗ , L ∗ ∗ , L ∗ ∗ ∗ , ⋯ L^*,L^{**},L^{***},\cdots L,L,L,,不妨记为 L L L序列 J 0 , J 1 , J 2 , . . . J_0,J_1,J_2,... J0,J1,J2,...。 设 J J J的公理集是 J 0 , J 1 , J 2 , . . . J_0,J_1,J_2,... J0,J1,J2,...的并集,往证 J J J是相容完全的。
可以很容易的将判断相容性转移到判断某个 A n A_n An是否相容的问题,由相容扩张的合法性知其是相容的。完全性可由构造的方法来判断。


定理:若 L ∗ L^* L L L L的相容扩张,则存在一个赋值,在这个赋值中, L ∗ L^* L的所有定理取值 T T T
证:
v ( A ) = { T , ⊢ J A F , o t h e r w i s e v(A)=\begin{cases}T , \vdash_J A \\ F, otherwise \end{cases} v(A)={ T,JAF,otherwise
只需验证 v v v的是否是赋值。由 J J J是相容的,可知 v ( A ) , v ( ¬ A ) v(A),v(\neg A) v(A),v(¬A)有且只有一个为T。
v v v的第二条性质也比较容易证明,详见P57.



命题逻辑的完备性证明

A A A L L L w f . wf. wf.并且 A A A是重言式,则 ⊢ L A \vdash_L A LA

证明:否则用 ¬ A \neg A ¬A扩充 L L L J J J,存在赋值 v v v使得 v ( A ) = F v(A)=F v(A)=F,与 A A A是重言式矛盾。

注意这里的赋值可以定义为命题逻辑的变量赋值,也可以不采取命题逻辑变量赋值,只要满足赋值的两条要求即可。 ¬ , → \neg ,\rightarrow ¬,也是纯形式上的,与是否给予命题逻辑的内涵无关。

任意满足公理为真,推导逻辑的前两项为真,则后件为真的含义都可以用该形式系统来证明其完备性。

展开阅读全文
打赏
0
0 收藏
分享
加载中
更多评论
打赏
0 评论
0 收藏
0
分享
返回顶部
顶部