直覺主義邏輯

01-28

類型論驛站寫作目錄：類型論驛站寫作計劃

何為邏輯？斯坦福哲學百科全書的 Logic and Ontology 條目給出了邏輯的四種常見的概念：

對於人工形式語言的研究
對於形式有效的推理和邏輯結果的研究
對於邏輯真的研究
對於判斷的普遍特徵或形式的研究

這四種概念在特定的研究場景下表現出極強的一致性，在另一些場景下則表現出明顯的不同。

最為著名的「經典邏輯（classical logic）」是學習邏輯的一個起點，以及其他邏輯作為參照的標杆。經典邏輯側重「真值」，陳述的「真值」是其「絕對」特徵。一個無歧義的合式陳述（well-formed statement）或真或假。假即非真，真即非假，是為「排中律」（Law/principle of excluded middle, tertium non datur）。

基於經典邏輯，我們可以「非構造地」證明一個命題。例如：

$exists x, yin mathbb{R}?mathbb{Q} text{s.t} x^y in mathbb{Q}$ （存在兩個無理數 $x, y$ ，使得 $x^y$ 為有理數）。

證明：如果 $sqrt 2 ^sqrt 2$ 是有理數，那麼我們可以取 $x=y=sqrt 2$ ，否則可以取 $x = sqrt 2^sqrt 2, y=sqrt 2$ .

上面的證明雖然在經典邏輯里沒有問題，但我們仍無法確定究竟哪一種情況是正確的。除此之外，我們還可以做出一個構造性證明（constructive proof）：對於 $x=sqrt 2, y = 2 log_23$ ，我們有 $x^y=3inmathbb{Q}$ .

這種「構造式」的推理方式對應著「直覺主義邏輯」（intuitionistic logic）。直覺主義邏輯的哲學基礎是，不存在絕對真理，只存在理想化數學家（創造主體）的知識和直覺主義構建。邏輯判斷為真當且僅當創造主題可以核實它。所以，直覺主義邏輯不接受排中律。

BHK釋義（The BHK interpretation）

L. E. J. Brouwer, 1881 - 1966

А. Н. Колмогоров, 1903 - 1987

直覺主義命題邏輯，或稱直覺主義命題演算（Intuitionistic propositional calculus, IPC），的語言和經典命題邏輯的語言是一樣的。

定義1

假設一個命題變數（propositional variables，或譯為變項，為了保持邏輯、數學用語的一致性，類型論驛站中一般採用數學翻譯法）無限集合 $text{PV}$ ，我們定義邏輯式（formulas）的集合 $Phi$ 為滿足下列條件的最小集合：

所有謂詞變數和常量 $bot$ （謬）都是 $Phi$ 的元素；
如果 $phi, psi in Phi$ ，那麼 $(phitopsi), (phi vee psi), (phi wedge psi)in Phi.$

變數和常量被稱為原子式（atomic formulas）。子式（subformula）是一個邏輯式（不一定平凡）的構成邏輯式。

否定、等價和真（truth）定義如下：

$neg phiequiv_{df} phi to bot;$
$phi leftrightarrow psi equiv_{df} (phitopsi)wedge (psi to phi);$
$top equiv_{df} bot to bot.$

直覺主義邏輯里的語義不是通過真值表來判斷的，而是通過構建模式來解釋的。這就是著名的BHK釋義（Brouwer-Heyting-Kolmogorov interpretation）。Heyting 是 Brouwer的學生。Kolmogorov有個著名的學生叫Martin-L?f.

$phi_1 wedge phi_2$ 的構造（或證明）包含 $phi_1$ 的構造和 $phi_2$ 的構造；
$phi_1vee phi_2$ 的構造包含一個指數（indicator） $iin{1,2}$ 和一個 $phi_i$ 的構造；
$phi_1 tophi_2$ 的構造是一個把每一個 $phi_1$ 的構造都轉換為 $phi_2$ 的構造的函數（方法）；
不存在 $bot$ 的構造。

練習1：

證明下列命題：

Theorem bot_to_p: False -> P.nnTheorem neglect_Q: P->Q->P.nnTheorem pqr: (P->Q->R)->(P->Q)->P->R.nnTheorem doub_neg: P->~~P.nnTheorem doub_neg_elim: ~~~P->~P.nnTheorem contra_imp:(P->Q)->(~Q->~P).nnTheorem vee_distr: ~(P/Q) <-> (~P/~Q).nnTheorem sum_arrow:((P/Q)->R)<->(P->(Q->R)).nnTheorem ex_mid_doub_neg: ~~(P/~P).nnTheorem ex_mid_impl: (P/~P)->~~P->P.n

參考答案（使用 Coq）：

Section BHK_interpretable.nnHypotheses P Q R:Prop.nnTheorem bot_to_p: False -> P.nProof.nintros.nelim H.nQed.nnTheorem neglect_Q: P->Q->P.nProof.nauto.nQed.nnTheorem pqr: (P->Q->R)->(P->Q)->P->R.nProof.nauto.nQed.nnTheorem doub_neg: P->~~P.nProof.nauto.nQed.nnTheorem doub_neg_elim: ~~~P->~P.nProof.nauto.nQed.nnTheorem contra_impP->Q)->(~Q->~P).nProof.nauto.nQed.nnTheorem vee_distr: ~(P/Q) <-> (~P/~Q).nProof.nunfold iff.nunfold not.nsplit.nintros. (*left implies right*)nrefine (conj _ _);auto.nintros (*right implies left*).nelim H0;apply H.nQed.nnTheorem sum_arrow:((P/Q)->R)<->(P->(Q->R)).nProof.nunfold iff.nsplit.nintros.napply H.nsplit; [apply H0 | apply H1].nintros;apply H; apply H0.nQed.nnTheorem ex_mid_doub_neg: ~~(P/~P).nProof.nunfold not.nauto.nQed.nnTheorem ex_mid_impl: (P/~P)->~~P->P.nProof.nunfold not.nintros.nelim H.ntrivial.nintros.ndestruct H.nassumption.nelim H0.nexact H.nQed.nnPrint bot_to_p. (*查看構造*)nPrint ex_mid_impl.nnEnd BHK_interpretable.n

下列邏輯式在經典邏輯里是重言式（tautology），但在直覺主義邏輯里卻沒有構造。

$((pto q)to p)to p$ （Peirce 定律）
$pvee neg p$ （排中律）
$negneg pto p$ （雙重否定消除）
$(neg qto neg p)to(pto q)$ （反證法）
$neg(pwedge q) leftrightarrow (neg pvee neg q)$ （De Morgan定律）
$(pto q)to(neg p to q)to q$
$((pleftrightarrow q)leftrightarrow r)leftrightarrow(pleftrightarrow (q leftrightarrow r) )$
$(pto q)leftrightarrow (neg pvee q)$ （經典邏輯中蘊含的定義）
$(pvee qto p)vee (pvee qto q)$
$(negneg pto p)to p vee neg p$

自然演繹（natural deduction）

直覺主義邏輯的一個證明系統是自然演繹系統 $text{NJ}(to,bot,wedge, vee)$ 。其中J代表直覺主義邏輯。NK是經典邏輯的自然演繹系統。

定義2

自然演繹里的判斷（judgement）是一個對子，寫作 $Gammavdashphi$ ，讀作「Gamma證明phi」，包括一個有限邏輯式集合 $Gamma$ 和一個邏輯式 $phi$ .
${phi_1, phi_2 }vdash psi$ 簡寫為 $phi_1,phi_2vdash psi$ ； $GammacupDelta$ 簡寫為 $Gamma,Delta$ ； $Gamma cup{phi}$ 簡寫為 $Gamma, phi$ ； $varnothing vdash phi$ 簡寫為 $vdash phi$ .
$Gammavdashphi$ 的形式證明（proof）或推導（derivation）是一個滿足下列條件的有限判斷樹：

根標記為 $Gammavdashphi$ ；
所有的葉子都是公理（公設，axioms），即形如 $Gamma, phi vdashphi$ 的判斷；
其他節點的符號都可以從子節點藉助下述法則得到：

(Ax) $Gamma,phivdash phi$

( $to$ I) $frac{Gamma,phivdash psi}{Gammavdash phitopsi}$

( $to$ E) $frac{Gamma,phivdash phito psiphantom{two}Gammavdash phi }{Gammavdashpsi}$

( $wedge$ I) $frac{Gammavdashphiphantom{tw}Gammavdash psi}{Gammavdash phi wedge psi}$

( $wedge$ E) $frac{Gammavdash phiwedgepsi}{Gammavdashphi}$ ; $frac{Gammavdash phiwedgepsi}{Gammavdashpsi}$

( $vee$ I) $frac{Gammavdash phi}{Gammavdashphiveepsi}$ ; $frac{Gammavdash psi}{Gammavdashphiveepsi}$

( $vee$ E) $frac{Gamma,phivdash thetaphantom{tw}Gamma,psivdashthetaphantom{tw}Gammavdash phivee psi}{Gammavdash theta}$

( $bot$ E) $frac{Gammavdash bot}{Gammavdash phi}$

4. 如果 $vdashphi$ ，那麼我們稱 $phi$ 是一個定理（theorem）。

弱化（Weakening）和替換（Substitution）

$frac{Gammavdashphi}{Gamma,psivdash phi}$ ; $frac{Gammavdashphi}{Gamma[p:=psi]vdashphi[p:=psi]}$

經典邏輯的代數語義學

定義3（格，lattice）

格是一個偏序 $langle A,le rangle$ ，其中 $A$ 的每一個雙元素子集 ${a,b}$ 都有一個最小上限（least upper bound）和一個最大下限（greatest lower bound）。
$sup _A {a,b}$ 記為 $a sqcup b$ ； $inf_A {a,b}$ 記為 $asqcap b$ .
一個格中的頂端元素通常記為 $1$ ，底端元素通常記為 $0$ .

定義4（分配格，補）

格 $A$ 是分配的（distributive），當且僅當：

$(a sqcup b)sqcap c = (a sqcap c)sqcup(bsqcap c )$ ； $(a sqcap b)sqcup c = (a sqcup c)sqcap(bsqcup c )$

設格 $A$ 頂端元素為 $1$ ，底端元素為 $0$ ，那麼我們稱 $b$ 是 $a$ 的補，當且僅當 $asqcup b=1$ 且 $asqcap b=0.$

定義5（布爾代數）

布爾代數（Boolean algebra）是有頂端和底端元素的分配格 $B$ ， $B$ 中的每一個元素 $a$ 都有一個補（記為 $-a$ ）。
布爾代數通常記為 $mathcal{B}=langle B,sqcup, sqcap, -0,1rangle$ ，其中 $ale b iff asqcap b = a$ .

定義6（賦值）

布爾代數 $mathcal{B}=langle B,sqcup, sqcap, -0,1rangle$ 的一個賦值（valuation）是任意一個從集合 $text{PV}$ 到 $B$ 的映射。邏輯式 $phi$ 在 $mathcal{B}$ 中的值（value）歸納地定義如下：

$[[p]]_v = v(p), text{for} pin text{PV}; [[bot]]_v = 0; [[phivee psi]]_v=[[phi]]_v sqcup [[psi]]_v; [[phiwedge psi]]_v=[[phi]]_vsqcap[[psi]]_v; [[phitopsi]]_v=-[[phi]]_vsqcup[[psi]]-v.$

當 $[[phi]]_v=1$ 時，我們記作 $mathcal{B},vvDash phi$ ；當對於所有 $v$ ， $mathcal{B},vvDash phi$ 時，我們記作 $mathcal{B}vdashphi$ .

定理7

命題邏輯式 $phi$ 是經典邏輯重言式（classical tautology）當且僅當對於所有布爾代數 $mathcal{B}$ ， $mathcal{B}vDash phi.$

海廷代數（Heyting algebra）

布爾代數是經典邏輯的一種語義詮釋，而海廷代數則是直覺主義邏輯的代數語義學。在直覺主義邏輯里，我們關注的首要問題是「可證明性」（provability），而非「真值」。

可證明的蘊含關係具備自反性和傳遞性：

Section Heyting_algebra.nnHypotheses phi psi theta: Prop.nnTheorem reflexivity: phi -> phi.nProof.n trivial.nQed.nnTheorem transitivity: ((phi -> psi) / (psi -> theta))-> psi -> theta.nProof.n intros H psi.n elim H.n intros.n auto.nQed.n

下面我們看等價關係。首先我們定義 $phisim_Gamma psi iff Gamma vdashphitopsi 且 Gammavdashpsitophi.$ 省略下標，我們有 $[bot]_sim = { phi mid Gamma vdash negphi}$ ， $[top]_sim = { phi mid Gamma vdash phi}$ . 設 $mathcal{L}_Gamma = Phi/_sim = {[phi] mid phi in Phi}$ ，那麼 $[phi]_sim le_Gamma [psi]_sim iff Gammavdash phi to psi.$ 等價關係定義為 $[phi]_sim =_Gamma [psi]_sim iff [phi]_sim le [psi]_sim 且 [psi]_sim le [phi]_sim.$ 然後我們會發現 $langle mathcal{L}_Gamma, le rangle$ 是一個格。

定義8（偽補，pseudo-complement）

在一個格中， $c$ 被稱為 $a$ 對於 $b$ 的關係偽補（relative pseudo-complement）當且僅當 $c$ 是使得 $asqcap cle b$ 的最大元素。關係偽補如果存在，用 $aRightarrow b$ 標記。我們將 $aRightarrow0$ 標記為 $-a$ 。

定義9（海廷代數）

海廷代數是有最高和最低元素的分配格 $H$ ，其中所有 $a,bin H$ 都有關係偽補 $aRightarrow b$ . 海廷代數的結構是 $mathcal{H} = langle H, sqcup,sqcap,Rightarrow, -,0,1rangle$ .

定義10（海廷代數的賦值）

設 $mathcal{H} = langle H, sqcup,sqcap,Rightarrow, -,0,1rangle$ 是一個海廷代數， $mathcal{H}$ 上的一個賦值（valuation）是映射 $v:text{PV}to H$ . 我們定義邏輯式 $phi$ 的值（value） $[[phi]]_v$ （或記為 $[[phi]]_v^mathcal{H}$ ）如下：

$[[p]]_v = v(p), text{for} pin text{PV}; [[bot]]_v = 0; [[phivee psi]]_v=[[phi]]_v sqcup [[psi]]_v; [[phiwedge psi]]_v=[[phi]]_vsqcap[[psi]]_v; [[phitopsi]]_v=[[phi]]_vRightarrow[[psi]].$

在海廷代數里，我們使用下述標記：

$[[phi]]_v = 1$ 記為 $mathcal{H},vvDash phi$ ；
對於所有 $v$ ， $H, vvDash phi$ ，記為 $mathcal{H}vDash phi$ ；
對於所有 $phi inGamma$ ， $H, vvDash phi$ ，記為 $mathcal{H}vDash Gamma$ ；
對於所有 $v$ ， $H, vvDash Gamma$ ，記為 $mathcal{H}vDash Gamma$ ；
對於所有 $mathcal{H},v$ ， $H, vvDash Gamma$ ，記為 $vDash Gamma$ ；
對於所有 $mathcal{H},v$ ，如果 $H, vvDash Gamma$ 蘊含 $H, vvDash phi$ ，記為 $GammavDash phi$ （直覺主義重言式）.

海廷代數具備完全性（completeness）和健全性（soundness），即 $Gammavdash phi iff Gamma vDash phi$ 。

克里普克語義（Kripke semantics）

除了海廷代數語義之外，我們還可以為直覺主義邏輯提供可能世界語義學的詮釋，即克里普克語義。

定義11（克里普克模型，Kripke model）

克里普克模型是三元組 $mathcal{C}=langle C,le, Vdashrangle$ ，其中 $C$ 是一個非空集合，其元素被稱為狀態（states）或可能世界（possible worlds）， $le$ 是 $C$ 上的一個偏序， $Vdash$ 是 $C$ 中的元素和命題變數之間的二元關係。 $Vdash$ （讀如「迫使」，forces）必須滿足下列單調性條件（monotonicity condition）：