ノート: 情報科学における論理①

小野寛晰『情報科学における論理』の読書ノート。なるべく練習問題も解いてく。

2021-11-07 読み返してて気になる点があったので一部を訂正

第1章命題論理

古典命題論理の形式体系LK

式

式（sequent）は次の形式によって表現される。

$A_1 , \cdots , A_i \vdash B_1 , \cdots , B_j$

ここで $A_i , B_j$ は論理式を表す。

上の式は直感的には $A_1 \land \cdots \land A_i$ を仮定すると $B_1 \lor \cdots \lor B_j$ が導かれることを意味する。なお $\vdash B_1 , \cdots , B_j$ は仮定なしで $B_1 \lor \cdots \lor B_j$ が導かれること、 $A_1 , \cdots , A_i \vdash$ は $A_1 \land \cdots \land A_i$ を仮定すると矛盾が導かれることをそれぞれ意味する。

推論規則

前提となるいくつかの命題から別の命題を導き出す為の規則を推論規則（inference rule）という。

LKは式から式を導き出す推論規則として以下を備える。なお $A , B$ は論理式、 $\Gamma , \Delta , \Pi , \Sigma$ は長さ0以上の論理式の列を表す。

Weakening Left (WL): $\cfrac { \Gamma \vdash \Delta } { A , \Gamma \vdash \Delta }$
Weakening Right (WR): $\cfrac { \Gamma \vdash \Delta } { \Gamma \vdash \Delta , A }$
Contraction Left (CL): $\cfrac { A , A , \Gamma \vdash \Delta } { A , \Gamma \vdash \Delta }$
Contraction Right (CR): $\cfrac { \Gamma \vdash \Delta , A , A } { \Gamma \vdash \Delta , A }$
Exchange Left (XL): $\cfrac { \Gamma , A , B , \Pi \vdash \Delta } { \Gamma , B , A , \Pi \vdash \Delta }$
Exchange Right (XR): $\cfrac { \Gamma \vdash \Delta , A , B , \Pi } { \Gamma \vdash \Delta , B , A , \Pi }$
Cut: $\cfrac { \Gamma \vdash \Delta , A \;\;\; A , \Pi \vdash \Sigma } { \Gamma , \Pi \vdash \Delta , \Sigma }$
※直感的には三段論法と同じ（ $\Delta$ と $\Pi$ が空の場合で考えると分かりやすい）
∧ Left 1 (∧L1): $\cfrac { A , \Gamma \vdash \Delta } { A \land B , \Gamma \vdash \Delta }$
∧ Left 2 (∧L2): $\cfrac { B , \Gamma \vdash \Delta } { A \land B , \Gamma \vdash \Delta }$
∧ Right (∧R): $\cfrac { \Gamma \vdash \Delta , A \;\;\; \Gamma \vdash \Delta , B } { \Gamma \vdash \Delta , A \land B }$
∨ Left (∨L): $\cfrac { A , \Gamma \vdash \Delta \;\;\; B , \Gamma \vdash \Delta } { A \lor B , \Gamma \vdash \Delta }$
∨ Right 1 (∨R1): $\cfrac { \Gamma \vdash \Delta , A } { \Gamma \vdash \Delta , A \lor B }$
∨ Right 2 (∨R2): $\cfrac { \Gamma \vdash \Delta , B } { \Gamma \vdash \Delta , A \lor B }$
→ Left (→L): $\cfrac { \Gamma \vdash \Delta , A \ \ \ \ B , \Pi \vdash \Sigma } { A \rightarrow B , \Gamma , \Pi \vdash \Delta , \Sigma }$
→ Right (→R): $\cfrac { A , \Gamma \vdash \Delta , B } { \Gamma \vdash \Delta , A \rightarrow B }$
¬ Left (¬L): $\cfrac { \Gamma \vdash \Delta , A } { \lnot A , \Gamma \vdash \Delta }$
¬ Right (¬R): $\cfrac { A , \Gamma \vdash \Delta } { \Gamma \vdash \Delta , \lnot A }$

推論規則の上下の式をそれぞれ上式、下式という。

証明図

公理となる式に推論規則を0回以上適用して式 $S$ にまで達したとき、 $S$ は証明可能（provable）であるといい、その過程を記したものを $S$ に到る証明図（proof figure）という。公理となる式をこの証明図の始式（initial sequent）といい、また $S$ をこの証明図の終式（end sequent）という。

LKは始式として $A \vdash A$ を採用する。

例）ド・モルガンの法則 $\lnot ( A \lor B ) \vdash \lnot A \land \lnot B$ の証明

f:id:sciencesakura:20190823010412p:plain

トートロジーな式

論理式に対する性質であるトートロジーを式にも適用できるよう拡張する。

論理式の列 $\Gamma = A_1 , \cdots , A_i$ に対して論理式 $\Gamma^{ \ast } , \Gamma_{ \ast }$ を次のように定める。

$\Gamma^{ \ast } = \left\{ \begin{array}{l} A_1 \lor \cdots \lor A_i \;\;\; ( i > 0 ) \\ \bot \;\;\; ( i = 0 ) \end{array} \right. \\ \Gamma_{ \ast} = \left\{ \begin{array}{l} A_1 \land \cdots \land A_i \;\;\; ( i > 0 ) \\ \top \;\;\; ( i = 0 ) \end{array} \right.$

式 $\Gamma \vdash \Delta$ がトートロジーであることと、論理式 $\Gamma_{ \ast } \rightarrow \Delta^{ \ast }$ がトートロジーであることは同じであるとする。

健全性と完全性

LKは健全かつ完全。すなわちLKで証明可能な任意の式はトートロジーであり、任意のトートロジーな式はLKで証明可能。

Cut除去定理

LKで証明可能な式について、推論規則Cutを一度も使わずに証明する証明図が存在する。

~~Cutが除去できると何が嬉しいのかいまいち分からない……。~~

終式から証明図を上に辿っていく場合、Cutが含まれていると新しい論理式が突如登場することになる。これは推論規則Cutによる上式が一意に定まらないということであり、機械的操作で証明を行うのが難しい。幸いLKはCutを使わずとも証明能力が変わらない。

練習問題

問1.1

不正。付値 $v_1 ( A ) = 1, v_2 ( A ) = 0$ を仮定すれば $v_2 ( A \rightarrow B ) = 1$ となり $B$ が充足不可能でも設問の前提を満たす。
正。 $B$ が充足不可能であると仮定する。設問よりすべての付値 $v$ に対して $v ( A \rightarrow B ) = 1$ であるがこれを満たすには $v ( A ) = 0$ でなくてはならない。これは $A$ が充足可能であるという前提に反する。よって $B$ は充足可能。

問1.2

$v( ( ( p \lor q ) \rightarrow r ) \lor ( p \land q ) ) = 0 \\ \Longleftrightarrow \left\{ \begin{array}{l} v ( ( p \lor q ) \rightarrow r ) = 0 \\ v ( p \land q ) = 0 \end{array} \right. \\ \Longleftrightarrow \left\{ \begin{array}{l} v ( p \lor q ) = 1 \\ v ( r ) = 0 \\ v ( p \land q ) = 0 \end{array} \right. \\ \therefore ( v ( p ) , v ( q ) , v ( r ) ) = ( 1 , 0 , 0 ) , ( 0 , 1 , 0 )$

問1.3

論理結合子として $\rightarrow , \land$ のみを含む論理式をBNFで表すと次の通り。ここで $proposition$ は任意の命題変数を表すものとする。

$formula = proposition \; | \; ( formula \rightarrow formula ) \; | \; ( formula \land formula )$

論理式 $A , B$ がともに真のとき論理式 $A \rightarrow B , A \land B$ はいずれも真。従って $proposition$ によって表現されるすべての命題変数が真のとき論理式 $formula$ はあきらかに真となる。よって充足可能。

問1.5

$v ( A \leftrightarrow B ) \\ = v ( ( A \rightarrow B ) \land ( B \rightarrow A ) ) \\ = v ( ( \lnot A \lor B ) \land ( \lnot B \lor A ) ) \\ = v ( ( \lnot A \land \lnot B ) \lor ( \lnot A \land A ) \lor ( B \land \lnot B ) \lor ( B \land A ) ) \\ = v ( ( A \land B ) \lor ( \lnot A \land \lnot B ) )$

問1.7

■ $C = D \lor E$ の場合

$v_1 ( D_A \lor E_A ) = 1 \\ \Longleftrightarrow v_1 ( D_A ) = 1 \mathrm{ \ or\ } v_1 ( E_A ) = 1 \\ \mathrm{ if\ } v_1 ( D_A ) = 1 , \mathrm{ \ then\ } v_1 ( D_B ) = 1 \Longrightarrow v_1 ( D_B \lor E_B ) = 1 \\ \mathrm{ else\ if\ } v_1 ( E_A ) = 1 , \mathrm{ \ then\ } v_1 ( E_B ) = 1 \Longrightarrow v_1 ( D_B \lor E_B ) = 1 \\ \therefore v_1 ( D_A \lor E_A ) = 1 \Longrightarrow v_1 ( D_B \lor E_B ) = 1$

また

$v_2 ( D_A \lor E_A ) = 0 \\ \Longleftrightarrow v_2 ( D_A ) = v_2 ( E_A ) = 0 \\ \Longleftrightarrow v_2 ( D_B ) = v_2 ( E_B ) = 0 \\ \Longleftrightarrow v_2 ( D_B \lor E_B ) = 0$

よって任意の付値 $v$ について $v ( D_A \lor E_A ) = v ( D_B \lor E_B )$ が成り立つ。

■ $C = D \rightarrow E$ の場合

$v_1 ( D_A \rightarrow E_A ) = 1 \\ \Longleftrightarrow v_1 ( D_A ) = v_1 ( E_A ) = 1 \mathrm{ \ or\ } v_1 ( D_A ) = 0 \\ \mathrm{ if\ } v_1 ( D_A ) = v_1 ( E_A ) = 1 , \mathrm{ \ then\ } v_1 ( D_B ) = v_1 ( E_B ) = 1 \Longrightarrow v_1 ( D_B \rightarrow E_B ) = 1 \\ \mathrm{ else\ if\ } v_1 ( D_A ) = 0 , \mathrm{ \ then\ } v_1 ( D_B ) = 0 \Longrightarrow v_1 ( D_B \rightarrow E_B ) = 1 \\ \therefore v_1 ( D_A \rightarrow E_A ) = 1 \Longrightarrow v_1 ( D_B \rightarrow E_B ) = 1$

また

$v_2 ( D_A \rightarrow E_A ) = 0 \\ \Longleftrightarrow v_2 ( D_A ) = 1 \mathrm{ \ and\ } v_2 ( E_A ) = 0 \\ \Longleftrightarrow v_2 ( D_B ) = 1 \mathrm{ \ and\ } v_2 ( E_B ) = 0 \\ \Longleftrightarrow v_2 ( D_A \rightarrow E_A ) = 0$

よって任意の付値 $v$ について $v ( D_A \rightarrow E_A ) = v ( D_B \rightarrow E_B )$ が成り立つ。

■ $C = \lnot D$ の場合

$v_1 ( \lnot D_A ) = 1 \\ \Longleftrightarrow v_1 ( D_A ) = 0 \\ \Longleftrightarrow v_1 ( D_B ) = 0 \\ \Longleftrightarrow v_1 ( \lnot D_B ) = 1$

同様にして $v_2 ( \lnot D_A ) = 0 \Longleftrightarrow v_2 ( \lnot D_B ) = 0$

よって任意の付値 $v$ について $v ( \lnot D_A ) = v ( \lnot D_B )$ が成り立つ。

問1.8

$p \rightarrow ( q \rightarrow r ) \\ \sim \lnot p \lor \lnot q \lor r \\ \sim \lnot ( p \land q ) \lor r \\ \sim ( p \land q ) \rightarrow r$

問1.10

面倒臭いので積和形だけ。

$( p \land q ) \lor ( p \land \lnot q ) \lor ( \lnot p \land q ) \lor ( \lnot p \land \lnot q )$
$( p \land \lnot q ) \lor ( \lnot p \land q ) \lor ( \lnot p \land \lnot q )$
$( p \land \lnot q \land r \land s ) \lor ( p \land \lnot q \land r \lnot s ) \lor ( p \land \lnot q \land \lnot r \land \lnot s )$