事情的前因後果比較複雜，目前的狀況是身上一堆沒看完的書和沒填完的坑，但還是處在開坑的狀態中
不過暑假還有一半不是嘛！

在這本書之前還看了一遍THU的《數理邏輯與集合論》。這書實在是太老了，在書上甚至還寫著費馬大定理仍然是open problem....這不搞笑嘛(掀桌)於是看完了那本又開始看這本

reasoning 推理
formalization 形式化
syntax 語法
semantic 語義的
propositional logic 命題邏輯
pre order 前序
in order 中序
material implication 實質蘊含
substitute A for B 用A替換B
tautology 重言式
deductive systems 推理系統
semantic tableaux 語義表
rules of inferences 推理規則

要區分清楚命題被證明和命題為真

我們主要關心邏輯系統(Logic System)的

1. consistency: 即一致性，命題和它的否定不能同時被證明
2. independence: 公理之間無法互相推出
3. soundness： 所有可被證明命題都為真
4. completeness： 所有真命題都可被證明

Hilbert希望證明數學可以被同時complete和consistent地公理化，但是Godel證明這是做不到的，即consistent的算術公理系統必然存在無法證明的真命題。

The system of logic that can be intepreted by values, functions and relations is called first-order logic(also called predicate logic or predicate calculus)

Modal Logic: 命題真值可以不是真和假，例如{T,F,M}表示一定真、假、可能真。當然也可以用概率來理解

Temporal Logic: Modal Logic的一種，{T,M,F}分別表示"always true","eventually true","false".這在互動式的程式中非常有用，例如OS

如何驗證程式的正確性：

1. 首先要形式化定義"正確"為一個命題
2. 然後形式化程式的語義(行為)
3. 在一個形式系統中進行推理，驗證程式滿足正確性

介紹一種邏輯通常從syntax和semantic層面來說
syntax: 哪些是公式
semantic: 公式的含義(真值如何計算)

這本書對命題公式的定義是從樹形結構的角度開始的，我覺得講得比較清楚

樹形結構變為公式的時候必然要損失結構資訊，因此書中給出了三種解決(模糊含義)的方案

1. 加括號，這裡通常認為所有連線命題的符號地位都是相等的
2. 規定優先順序和結合性(左結合/右結合)，即對不同符號的優先順序做出區分.奇怪的是書上說一般符號是右結合的

當然也可以用CFG(context free grammar)規定命題公式，就是遞迴定義~

Polish Notation

就是前序遍歷表示式樹(運算在元素前),求值就逆序遍歷

Structural Induction

由Formulas的結構可知，證明一些相關命題可以通過結構遞迴來證明其對所有Formula成立

1. 證明原子命題成立
2. 假設命題A成立，證明對\(\neg A\)成立
3. 假設A、B成立，證明A op B成立

Interpretations

一個Formula的Intepretation就是為其所有atoms賦予真值，即一個{all atoms}到{T,F}的函式

Formula F在Interpretation I下的真值叫the value of F under I

Partial Interpretaions

有時只需要帶入部分atom的真值，這就是partial的含義

Truth Table

也即真值表.若F有n個atoms，則列2^n列列舉所有Interpretations，計算每種情況下F的真值

Logical Equivalence

若Formula F1 F2在任意Interpretation I下都有I(F1)=I(F2)，則稱二者為Logical Equivalence，記作\(F_1\equiv F_2\)

舉例：\((p\rightarrow q)\equiv (\neg p\vee q)\)
這告訴我們在證明含變項的命題時需要證明它在任意解釋下都成立

\(\leftrightarrow\)和\(\equiv\)的區別

\(\leftrightarrow\)是二元運算元，用以連線兩個命題，構成一個新的大的命題
\(equiv\)是一個命題集合上的二元等價關係，兩側的命題看成是分開的兩個部分

定理：有 \(F_1\equiv F_2\)​ 當且僅當 \(F_1\leftrightarrow F_2\)​在任意解釋下為真
證明：
必要性:\(F_1\equiv F_2\)​，故在任意解釋I下 \(I(F_1)=I(F_2)\)​，即在任意解釋I下\(I(F_1)\leftrightarrow (F_2)\)​為真，即\(F_1\leftrightarrow F_2\)​在任意解釋下為真

充分性:考慮\(\leftrightarrow\)的真值表：\(F_1\leftrightarrow F_2\)為真當且僅當\(F_1=F_2\)，即在任意解釋下\(F_1=F_2\)，於是\(F_1\equiv F_2\)

Substitution

logical equivalent是為了substitution做準備
首先要定義Subformula

Subformula

考慮Formula的樹形結構，F'是F的Subformula當且僅當F'是F的子樹
若F'!=F，則稱為Proper Subformula

記A是一個formula，B是A的subformula，C是任意一個formula
則把操作\(A\left\{B\leftarrow C\right\}\)記為 substitute C for B in A,含義是用C換掉A中的B(注意順序)

定理：對於substitution \(A'=A\left\{B\leftarrow C\right\}\)​，若 \(B\equiv C\)​，則有\(A\equiv A'\)​
證明：對錶達式樹的深度作歸納即可，base case是A中所有的B

substitution通常用於簡化求值某些複雜formulas

Equivalences

常見的等價有很多，這裡就不放了

Operators

重要性質：是否adequate，即是否能表示出所有可能的運算子號
n元運算op實際上可以看成是\({T,F}^n\mapsto {T,F}\)的函式，故n元運算總共有\(2^{2^n}\)種

我們稱二元運算\(\circ\)由運算集\(S=\left\{\circ_1,\ldots,\circ_n\right\}\)定義當且僅當
任意形如\(A_1\circ A_2\)的公式都存在\(A\)可由\(A_1,A_2\)經\(S\)中的運算得到，且\(A\equiv A_1\circ A_2\)。

事實上定義的符號是冗餘的，例：
\(A\leftrightarrow B=(A\leftarrow B)\wedge(B\leftarrow A)\)
\(A\leftarrow B\equiv\neg A\vee B\)
\(A\wedge B=\neg(\neg A\vee \neg B)\)
\(A\uparrow T=\neg(A\wedge T)=\neg A\)
\(\neg A\uparrow\neg B=\neg(\neg A\wedge\neg B)=A\vee B\)
於是實際上只需要與非(nand)、或非(nor)的其中一個就可以表示出所有的符號

定理：若二元運算\(\circ\)​可表示出所有的二元運算和\(\neg\)​，則\(\circ\)​只能為\(\uparrow\)​或\(\downarrow\)​

想了挺久，書上給的提示2沒有看懂，自己搗鼓了一下

不妨取\(A=T\)，則根據符號可被表示的定義有\(F=\neg A\equiv A\circ A\circ\ldots\circ A=\left(A\circ A\circ\ldots\circ A\right)\circ A\)
我們claim對於\(\circ\)運算必有\(T\circ T=F\)
反證：假設\(T\circ T=T\)，則上述式子根據左結合性有\(F=T\)，矛盾。故\(T\circ T=F\)

同理可證\(F\circ F=T\)​。這說明\(\circ\)​只可能是\(\uparrow\)​、\(\downarrow\)​、\(A\circ B=\neg A\)​、\(A\circ B=\neg B\)​

考慮一個任意的二元運算op，則根據符號可被表示的定義有\(A op B\equiv C_1\circ C_2\circ\ldots\circ C_n\)，其中\(C_i=A\)或\(C_i=B\)。而根據投影的定義，必然有\(C_i\circ C_j=\neg C_i\)或\(C_i\circ C_j=\neg C_j\)，這說明\(A op B=A\)或\(A op B=B\)或\(A op B=\neg A\)或\(A op B=\neg B\)，即\(op\)也是投影。這與op的任意性矛盾。

因此能表示出所有二元運算和\(\neg\)的二元運算只能是\(\uparrow\)和\(\downarrow\)

Formula Semantics

A is a Formula

1. A is satisfiable iff \(\exists I\), I(A)=T.此時稱I是F的一個model
2. A is unsatisfiable iff \(\forall I\), I(A)=F
3. A is valid iff \(\forall I\)，I(A)=T,valid formula也叫做tautology,記作\(\models A\)
4. A is falsifiable iff \(\exists I\),I(A)=F,記作\(\not\models A\)

類似可以定義formula sets的語義(可滿足/不可滿足/永真/永假)

給定一個公式集合F的子集U，判斷命題\(A\in U\)的真假的演算法被稱為decision procedure for U
利用真值表很容易寫出satisfiability的一個decision procedure，並且可以用它來判斷上述四種情況

Logical Consequnce

U是公式集，A是公式，若在任意使得U成立的解釋I下都有I(A)=T(U的model都是A的model)，則稱A是U的logical consequence,記作\(U\models A\)

同樣，\(\rightarrow\)​是公式的二元運算元，用以連線兩個公式得到新的公式
而\(\models\)​是元語言中的一個概念的符號(a symbol for a concept in the metalanguage)，是用來描述一階語言的"語言用詞"

類似\(A\equiv B\)​​當且僅當\(A\leftrightarrow B\)​​是永真式
定理：\(A\models B\)​​當且僅當\((\wedge A_i)\rightarrow B\)​​是永真式，即\(A\models B\)​​當且僅當\(\models ((\wedge A_i)\rightarrow B)\)​​

證明充分性：右側永真，因此在任意解釋下為真，因此在所有使得\((\wedge A_i)\)為真的解釋下\(B\)都為真，這恰好就是\(A\models B\)的定義
必要性：由反證法，假設右側不是永真式，則存在解釋I'使得\(I'(\wedge A_i)=T\)而\(I'(B)=F\)，這與logical consequence的定義矛盾。故右側永真

與簡單的imply符號相比，logical consequence更復雜也更貼合實際(以若干定理/公理為真作為前提出發，得到若干定理)

Theory

若公式集F在logical consequence運算下滿足封閉性，則稱F為一個theory，F中的公式為theorem

若存在F的子集U使得\(F=\left\{\;A\mid U\models A\;\right\}\)，則稱F是axiomatizable的，且U是F的axioms。若U有限，則F是finitely axiomatizable
書上33頁有一句暫時看不懂的話，先放著

Semantic Tableaux

首先介紹complementary pair(互補對)的概念
literal是原子或原子的否定。對原子p而言，\(p\)是positive literal,\(\neg p\)是negative literal
對於命題A而言，\(A\)與\(\neg A\)互為互補對

semantic tableaux的出發點就是把公式A拆成A中的literals，即討論哪些literals為真時A可滿足，然後檢查這些literals是否存在complementary pair

定理：公式可滿足當且僅當不存在complementary pairs的literals set：
存在cp->任意解釋都不滿足literals set中的literals為T->公式不可滿足，矛盾;
不存在cp->則令ls中的literals為T->這個解釋是well defined的->A為T可滿足;

流程

說白了一個tableau就是從公式A開始，每次取出優先順序最低的運算op把A分成A1和A2
若op是\(\wedge\)，則A1和A2都要為真(才能保證A可滿足)，此時把A拆分成A1和A2
若op是\(\vee\)，則A1或A2有一個為真就行了，此時造兩個分支兒子分別討論A1為真/A2為真
這樣造出來的樹形結構就是一個tableau，樹上的葉子就是一個literal set，A可滿足當且僅當存在沒有complementary pair的葉子。並且若A的所有葉子都有compelmentary pair，則稱A是close的，否則就是open的。就這麼簡單

有限性

演算法的有限性證明要用到勢能函式W(x)=3b(x)+n(x)，b和n分別為表示式x中二元符號和\(\neg\)的數量。只需要證明隨著深度遞增，勢函式單調遞減，且葉子的勢函式為0或2即可
或者先把A化成\(\wedge\)正規化，那麼隨著深度遞增符號數量就是單調遞減的了，這樣也可以證明

正確性

正確性的證明包括兩步:

1. soundness:所有closed formula都是不可滿足的
2. completeness:所有不可滿足的公式的任意一種tableau都是close的

1的證明可以對樹高進行歸納，用上closed formula的所有子樹都是closed formula->所有子樹都不可滿足，然後分類討論\(\wedge\)和\(or\)兩種情況

2的證明可以化為證明 若公式存在open tableau，則公式可滿足.把open leaf到根的路徑上的節點並起來得到集合S,用結構歸納法證明S在葉子的所有literals為真的解釋下為真(因此可滿足)，且A也在S中，因此A可滿足.

Deductive Proofs

也就是演繹證明.在之前的定理有\(U\models A\)當且僅當\(\models (\wedge U_i)\rightarrow A\)，因此我們似乎可以利用decision procedures來判斷這個等價命題的真值來證明公理U下的一個命題A，但是我們很少直接這麼做，因為：

1. U可能是無窮集,對於formulas with infinite terms的真值還沒有做出定義
2. 並非所有邏輯都像命題邏輯一樣存在decision procedures(並非所有邏輯都能判斷一個命題是否可滿足)
3. 有時推理過程中出現的intermediate results(中間結果)無法被認識，因為decision procedures只會給出最後的真值
4. 認識推理過程有利於我們認識公理和定理的關係，從而提出猜想

這一段寫得蠻好，算是解決了俺之前看別的書的一大疑問，好評！

Deductive Systems

一個deductive system是一個二元組(U,R)，分別表示set of axioms(公理集合)和inference rules(推理規則)

A Proof

一個Proof是A Sequence Of Formulas(一段公式的有限有序序列)，其中每個公式要麼是公理，要麼可以由序列中它之前的所有公式(或某些公式)推出

對於長度為n的proof P，我們稱An(最後一個公式)為theorem，P是An的一個proof，並且稱An is provable，記作\(\vdash A_n\)​

有關\(\vdash\)和\(\models\)的區別可以看這個寫得很好的回答

引入proof可以解決上面提到的四個問題：

1. Proof序列長度有限，雖然公理可以有無窮多個，但是隻有有限多的公理能出現在一個證明中。
2. 雖然可能沒有decision procedure，但是我們可以check(檢查)一段給定的Proof是否正確
3. Proof顯式地說明了每一條公理、定理的作用
4. 已被證明的定理可以用於後續證明

Gentzen System

axioms: a set of literals containing a complementary pair.
inference rules:

在Gentzen System中，從axioms出發證明命題A的過程可以看成是倒過來的樹形結構，並且和對A造出的Semantic Tableau形態是一樣的。

在ST中，每個節點內的子公式都是\(\wedge\)的關係(即都為真->根才可滿足)

而在GS中，每個節點內的子公式都是\(\vee\)​​​​的關係(即每個節點的公式集取否定後就變成了ST)，因此axioms是永真的(包含互補對)

下面\(\vdash\)的討論都限定在Gentzen System中

定理：\(\vdash A\)​則\(\models A\)​

也即是GS soundness的證明。我們同樣可以對樹形結構進行歸納得到：

顯然只需要證明\(\neg,\wedge,\vee\)三種運算子的規律即可

\(\alpha\)​規則就是\(\vee\)​對\(\wedge\)​的逆分配律。由於兩個子公式\(A_1\vee\left(\vee U_1\right)\)​和\(A_2\vee\left(\vee U_2\right)\)​都為真，所以\((A_1\vee\left(\vee U_1\right))\wedge (A_2\vee\left(\vee U_2\right))\)​仍然為真，經逆分配律就得到\((A_1\wedge A_2)\vee(\vee U_1)\vee(\vee U_2)\)為真

\(\beta\)​規則就是\(\vee\)​的結合律。由於\(A_1\vee A_2\vee U\)為真，因此\((A_1\vee A_2)\vee U=A\vee U\)​為真

定理：\(\models A\)則\(\vdash A\)

也即是GS completeness的證明。

由\(\models A\)，\(\neg A\)不可滿足。構造\(\neg A\)的semantic tableau T，T一定是closed tableau

將T的每一節點取反，這樣就得到了在GS中對\(A\)的proof。

why?

1. T的每個葉子都close，因此都存在complementary pair，取反後仍然存在CP，滿足axiom的定義
2. 仔細比對即可發現對應的拆分法則在取反意義下是相等的。

綜上就有\(\vdash A\iff \models A\)​

擴充套件到公式集\(S\)​上，易得\(\vdash S\iff (\forall x\in S)(\vdash x)\iff(\forall x\in S)(\models x)\iff \models S\)

這就為下面的定理做了鋪墊

定理：\(\vdash A\)​​當且僅當\(\neg A\)​​存在一個closed tableau

\(\vdash A\)當且僅當\(\models A\)當且僅當\(\neg A\)不可滿足當且僅當\(\neg A\)存在closed tableau

更進一步地，定理：\(\vdash S\)​當且僅當\(\overline S\)​存在closed tableu。這裡\(S\)​是公式集

記\(P(x)\)表示\(x\)存在closed tableau

\(\vdash S\iff\models S\iff(\forall x\in S)(\models x)\iff(\forall x\in S)(P(\neg x))\iff(\forall x\in\overline S)(P(x))\)

那麼只需要把\(\overline S\)中的所有元素的closed tableau取出來，兩兩合併回去就得到\(\overline S\)的closed tableau了

書上給的流程是先用歸納法證明最後一個定理，然後直接用closed tableau得到\(\vdash A\)和\(\models\)的關係。這裡的證明是自己寫的，希望沒有什麼大問題吧....