4 一階邏輯：證明論
4.4 前束范式和子句范式
12\(\vdash\)之第一組
- Q: 記憶第一組。\(x_i\)不在\(\mathscr{ A}\)中自由出現，則根據K（）（填編號）可以幫助記憶，寫出：（）。
A: 6
\(\vdash (\forall x_i)(\mathscr{ A}\to\mathscr{B})\leftrightarrow (\mathscr{A}\to\forall x_i\mathscr{B})\).
\(\vdash (\exists x_i)(\mathscr{ A}\to\mathscr{B})\leftrightarrow (\mathscr{A}\to\exists x_i\mathscr{B})\). - Q: 證明第一組第一式。第一式正向就是K6，反向可以發現整個右邊都不自由出現（），所以由果到因知道最后一步估計是演繹定理，倒數第二步估計是\((\mathscr{A}\to(\forall x_i)\mathscr{B})\vdash\)（）。這就簡單了。
A: \(x_i\)，\(\mathscr{A}\to\mathscr{B}\) - Q: 證明第一組第二式。左推右：我們發現“\(\sim\)在最外層的”太多了，所以設法減少這種情況。先把待證式抽象成\(\mathscr L_0\)中表達式\(\sim\mathscr{C}\to(\mathscr{A}\to\sim\mathscr{D})\)，再寫成外層不含\(\sim\)的等價形式（）。所以只用考察證明（）即可。
A: \(\mathscr{A}\to(\mathscr{D}\to\mathscr{C})\)，\(\mathscr{A},\forall x_i\sim\mathscr{B}\vdash \forall x_i\sim(\mathscr{A}\to\mathscr{B})\)
注：\(\mathscr{A}\)和\(\forall x_i\sim\mathscr{B}\)中都不含自由的\(x_i\)，這就提示演繹定理。 - Q: 接上，右推左：\((\mathscr{A}\to\sim\mathscr{D})\to\sim\mathscr{C}\)等價於\((\sim\mathscr{A}\vee\sim\mathscr{D})\to\sim\mathscr{C}\)，這提示我們只需證明\(\vdash\sim\mathscr{A}\to(\exists x_i)(\mathscr{ A}\to\mathscr{B})\)（顯然）和\(\vdash \exists x_i\mathscr{B}\to(\exists x_i)(\mathscr{ A}\to\mathscr{B})\)（證明方法（）），再通過重言式（）即可證明。
A: 使用K6'和K3
\((\sim \mathscr{A}\to\sim\mathscr{C})\to((\sim \mathscr{D}\to\sim\mathscr{C})\to((\sim\mathscr{A}\vee\sim\mathscr{D})\to\sim\mathscr{C}))\)
12\(\vdash\)之第二組
- Q: 第二組相比第一組考察的是（）不在（）中自由出現的情況，此時\(\forall x_i(\mathscr{A}\to\mathscr{B})\leftrightarrow(\exists x_i \mathscr{A}\to\mathscr{B})\)的直觀含義是什么？用自然語言說明。
A: \(x_i\)，\(\mathscr{B}\)
比如：“任何時候，做了這個就是得罪我”等價於……
注意這里“得罪我”的“我”在不同時刻是同一個我（\(x_i\)不在\(\mathscr B\)自由出現） - Q: 證明第二組第一式。左推右：\(x_i\)不在\(\mathscr{B}\)自由出現，也不在\(\forall x_i(\mathscr{A}\to \mathscr{B})\)自由出現，那自然就把這倆都丟左邊，最后（）定理就可以用。那為了\(\mathscr B\)能丟左邊，需要把原式轉化成（）
右推左：前件再次出現了\(\sim\mathscr{C}\to\mathscr{B}\)這種結構，那自然可以利用連接符（）改寫。類似於上節。
A: 演繹，\(\vdash \forall x_i(\mathscr{A}\to\mathscr{B})\to(\sim\mathscr{B}\to\forall x_i\sim\mathscr{A})\)，\(\vee\) - Q: 證明第二組第二式。左推右：前件有否定（存在量詞最外層是否定），那就改寫成（）去掉否定。
右推左：前件又是“復合命題”，直接用連接符（）改寫成（）即可。
A: \(\forall x_i \mathscr{ A},\sim\mathscr{B}\vdash \forall x_i\sim(\mathscr{A}\to\mathscr{B})\)
\(\vee\)，\(\vdash(\sim\forall x_i\mathscr{A}\vee \mathscr{B})\to\exists x_i(\mathscr{A}\to\mathscr{B})\)
12\(\vdash\)之第三組及總結
-
Q: 第三組把\(\exists\)寫開，就看起來像\(\mathscr{A}\)簡單換成了（）。而這顯然只需考慮重言式和K（）（填編號1-6或6'）
當然直接對\(\mathscr{A}\leftrightarrow \sim\sim\mathscr A\)替換定理也可。
A: \(\sim\sim\mathscr{A}\)，6'（注意K6'並不需要任何“不自由出現”條件） -
Q: 這12條\(\vdash\)中，如果使用（）的一側，可以造出前束范式。前束范式從形式上可以分成兩部分：前面是（），后面是（）。如果前面內部有（）結構稱為斯科倫前束范式，如果后面內部有（）結構稱為（）。
A: 把量詞放到整體前面（例如\(\forall x_i \mathscr{A}\to\mathscr{B}\)變成\(\exists x_i(\mathscr{A}\to\mathscr{B})\)）
量詞\((Q_1x_{i_1}\cdots Q_kx_{i_k})\)其中每個\(Q_i\)是\(\forall\)或\(\exists\)，不帶量詞的公式\(\mathscr{D}\)
存在量詞都在全稱量詞前（注：顯然這時所有斯科倫函項都退化成斯科倫常元）
是合取范式或析取范式，前束合取范式或前束析取范式 -
Q: 用這3組，（）個可證等價，共12個\(\vdash\)，證明任何公式都有（）等價的前束范式：
- 公式最外層\(\sim\)，進行此步歸納使用第（）組。
- 公式最外層\(\to\)，則需首先進行換名，使得\(Q_1x_{i_1}\cdots Q_kx_{i_k}\mathscr{C}_2\to R_1 x_{j_1}\cdots R_l x_{j_l}\mathscr{D}_2\)滿足（）條件，再不斷使用（）
- 公式最外層\(\forall\)則非常簡單，只需根據意義寫出一次替換（或用一次K6'）即可得到\(\vdash (\forall x_i)\mathscr C\leftrightarrow\)（）
替換定理在證明中用到了哪里？
A: 6，可證，三
各\(x_i,x_j\)不重名且它們還都和\(\mathscr{C}_2,\mathscr{D}_2\)中自由變元不重名（都是約束變元，你完全可以變元換名都換成新名）（其實就是去除變量遮蔽(shadow)）
一和二組（其中一組針對把\(R\)提前，二組針對把\(Q\)提前）
\((\forall x_i)(Q_1x_{i_1})\cdots(Q_kx_{i_k})\mathscr D\)
所有的“歸納”過程中，“歸納假設”只是說更短的公式有前束范式，你把更短的公式替換成其前束范式的過程中要保持可證等價，所以需要用替換定理。 -
Q: 上題只表示了前束范式可計算性、存在性。那唯一性和計算復雜性如何？
A: 顯然不唯一。注：之后求子句范式時，這種不唯一性進一步可能導致各種可能的斯科倫式之間不邏輯等價（但一定弱等價）
計算復雜性：提示：可以看到每個連接符都使得該連接符涉及的所有量詞引起\(\Theta(1)\)的計算量。深處的量詞被提出來時計算次數更多。 -
Q: 2.證明中，前件寫成前束范式，量詞用\(Q_i\)表示，后件寫成前束范式，量詞用\(R_j\)表示。則如果歸納出了\(Q_i^*\cdots R_j(前件\to 后件)\)，則星號意為（）。這里是先提取前件中的量詞還是后件中的？
A: 存在和任意互換。注意提取前件中的需要互換，提取后件中的不需要。
先提取了前件中的。總之，先提取的在前（常見錯誤：對於\(\forall x(\mathscr A\to\forall y\mathscr B)\)，提取\(y\)時錯誤放到了\(\forall x\)的前面） -
Q: 如何理解“復雜程度與量詞的交叉次數有關”？
A: 在實際執行計算時，出現“交叉”（就是從前往后看“切換”了多少次，例如\(\forall x\forall y\exists z\forall w\forall u\)就是“切換”或說交叉兩次）會影響計算復雜性。\(\Pi\)和\(\Sigma\)式的計算復雜性也可能不同。
注：數理邏輯是計算復雜性理論的“根”，\(\Sigma_n,\Pi_n\)式在其中起了重要作用。
更具體的東西在此處略去。
弱等價性定理
- Q: 記\(\mathscr A^s\)是\(\mathscr A\)的斯科倫式，則（）\(\vdash\)（）。應該對（）結構歸納。其中用到R4和Gen恢復量詞等等。（具體過程較難，省略）
A: \(\mathscr A^s\)，\(\mathscr A\)，\(\mathscr A\)
注：直觀（模型論？）上看倒是很顯然 - Q: 公理的斯科倫式是什么意思？之前學的公理系統中公理沒有存在量詞啊？
A: 公理模式沒有，公理可能有。
總之，\(K^s\)引入了一些新的公理（但沒有改變規則） - Q: 由0.，可以得到\(\vdash_{K^s}\mathscr A\)是\(\vdash_K\mathscr A\)的（）條件。
A: 必要
注：\(\mathscr A^s\)能推出\(\mathscr A\). 所以從這個角度，\(K^s\)推理能力“更強”，能推出更多的定理。所以是“必要條件”（后面還會證明是充要條件）。 - Q: 對於已知\(\mathscr A\)是\(K\)中公式，即不含新引入的斯科倫函項和斯科倫常元，可以證明上題的反向。
證明過程：課件中需要用（）定理。即若\(\mathscr{A}\)在\(K\)的每個可數模型\(M\)為真，則（）。
“每個可數模型”太難考察，那怎么辦？
A: 完全性（注：也就是純從證明論角度比較麻煩，要通過“模型為真”的關系架橋過渡）
\(\vdash_K \mathscr A\)
可數論域可同構於正整數集。而非空正整數集子集總有最小元，方便了考察。 - Q: 接上，具體證明過程是
\(\vdash_{K^s}\mathscr A\)
\(\vdash_{K^s}\mathscr C_i^s\)
\(\vdash_K \mathscr C_i\)
\(\mathscr C_i\)對\(M\)為真
\(\mathscr C_i^s\)對\(M^s\)為真
\(\mathscr A\)對\(M^s\)為真
\(\mathscr A\)對\(M\)為真
\(\vdash_K\mathscr A\)
解說每一步的依據和其中的“架橋”思想。
A:
根據演繹過程找到有限條\(K^s\)中用到的公理
根據\(K^s\)和\(K\)的定義找到對應的\(K\)中的公理
\(K\)的可靠性定理（\(M\)是任取的，論域為正整數集）
設法構造擴展模型（用到了正整數集的性質，如上題所述）
類似於可靠性定理，進行歸納（使用的規則還是MP和Gen. 參考題1.）
已知\(\mathscr A\)是\(K\)的公式，即不含新引入的斯科倫函項和斯科倫常元
\(K\)的完全性定理
架橋思想：最外層架橋是1678（用模型論架橋）
中間層架橋是1256（對一般的定理用公理架橋）
最內層架橋是2345（用舊系統公理的可靠性找模型） - Q: 上述事實為什么推出\(K\)和\(K^s\)的一致性是等價的？
A: 一方面\(K^s\)是“擴充”（回憶\(\mathscr A^s\vdash\mathscr A\)），\(K^s\)一致則\(K\)一致。
另一方面如果\(K^s\)不一致則能演繹出\(K\)中的矛盾式（因為矛盾能演繹出一切）。所以（根據之前結論）\(K\)也能演繹出\(K\)中的矛盾式。從而\(K\)不一致。 - Q: 上述事實（證明論中的弱等價）和模型論中的弱等價有何聯系？
A: \(\mathscr A\)和\(\mathscr A^s\)同時不一致。根據模型論和證明論聯系，不一致等價於矛盾式
總之，兩者同時為矛盾式，但不一定同時為有效式
注：所以課件上“當且僅當為真”其實不是完全好。可以寫成“\(\mathscr A\)存在為真的模型當且僅當\(\mathscr A^s\)存在為真的模型”
子句范式
- Q: 求子句范式過程中把（）（填等價類型）等價的前束范式（）化（這一步不是可證等價而是（）等價），又刪除所有全稱量詞，最后把原子都看成命題符進行命題邏輯中的演算即可。
A: 可證，斯科倫，弱 - Q: 斯科倫化是弱等價（矛盾等價於矛盾，有效不一定等價於有效），那刪除全稱量詞是弱等價嘛？
A: 是。而且既是邏輯等價，又是弱等價。（有效等價於有效，矛盾等價於矛盾）
- 注：它們的區別只有在賦值一層才能體現。在解釋一層就沒有區別了，真等價於真。“有效等價於有效，矛盾等價於矛盾”就是從這來的。
- 總之有三層：對賦值，對解釋，對整個一階語言。低層等價推出高層等價。
- 可證等價，邏輯等價，弱等價都是在最高層考察。即“大打包”，必須所有解釋都……，才去考察……
- “真等價於真”在解釋層考察，對所有賦值打了包（所以說\(\forall x_i\mathscr A\)和\(\mathscr A\)“拆包”到賦值層就不等價了）
- 注：回憶形式記號：能互相\(\models\)，或說能互相\(\vdash\)，就是邏輯等價，記為\(\equiv\)
勘誤集
ml-4_2.pdf
- p82 量詞的交叉在之前沒有給出定義，不容易理解
- p84 斯科倫寫成斯科林了
- p85 \(\exists x_4\)寫成\(\exists y_x\)了
- p86 \(\vdash_{K^s}\mathscr B\)推出\(\mathscr B\)在\(M^s\)中為真沒有詳細說明，不太容易看懂。其實類似可靠性定理證明