logic 設計

logic パッケージは、カーネルの等号計算を命題論理に変える。結合子をカーネルの定義として定義し、10 個の基本規則から自然演繹の規則を導出し、証明スクリプトが引用できる定理名のカタログを保持する。このページでは定義を示し、規則を導出し、このパッケージが信頼されなくてもこれらを実現できる理由を説明する。

設計目標

カーネルが知っているのは等号と選択だけである。ユーザーは $\top$、$\bot$、$\wedge$、$\Rightarrow$、$\neg$、$\vee$ を通常の規則とともに使いたい。目標は、新たな権限を一切与えずにこれらを提供することである。すべての結合子は DefOK ゲートが受理する定義であり、すべての規則はカーネル規則を呼び出す MoonBit 関数である。このパッケージは何かを証明し損なうという意味では誤りうるが、偽の命題を証明することはできない。

数学的背景

定義としての結合子

QED は HOL Light の定義に従い、すべての結合子を等号に還元する。¹1 J. Harrison, HOL Light Tutorial, 論理定数の節。これらの定義は Andrews の型理論 Q0 に遡る。QED の選言は HOL Light のものと異なる。後述を参照。 $t$ を真を表す項 $(\lambda x.\,x) = (\lambda x.\,x)$ とする。プレリュードは次を定義する。

$$\begin{aligned} \top &:= t \\ \bot &:= (\lambda p.\,p) = (\lambda p.\,t) \\ \mathit{and} &:= \lambda p\,q.\;(\lambda f.\,f\,p\,q) = (\lambda f.\,f\,t\,t) \\ \mathit{imp} &:= \lambda p\,q.\;\mathit{and}'\,p\,q = p \\ \mathit{not} &:= \lambda p.\;\mathit{imp}'\,p\,\bot' \\ \mathit{or} &:= \lambda p\,q.\;\mathit{imp}'\,(\mathit{not}'\,p)\,q \end{aligned}$$

ここでプライム付きの名前は定義本体を展開済みのものを表し、各右辺が $=$ のみの閉項になるようにしている。各定義の読み方は次のとおりである。

• $t$ は REFL のインスタンスであるから真である。
• $\bot$ は、ブール値上の恒等述語が常に真の述語に等しいことを述べる。すなわち $\forall P := (P = \lambda x.\,t)$ としたときの $\forall p.\,p$ である。$\bot$ 自身が真でなければならなくなるため、標準モデルでは偽である。
• $p \wedge q$ は、対 $(p, q)$ がどのような関数 $f$ によっても $(t, t)$ と区別できないことを述べる。これは $p$ と $q$ がともに真であるときに限り成り立つ。
• $p \Rightarrow q$ は $(p \wedge q) = p$ である。$p$ に $q$ を加えても何も変わらない。
• $\neg p$ は $p \Rightarrow \bot$ である。
• $p \vee q$ は $\neg p \Rightarrow q$ である。

基底項

prop_mk_and とその仲間は、定数の適用 $\mathit{and}\,p\,q$ ではなく、展開済みの右辺である基底形を返す。以下の規則は基底形に対して働く。カーネル規則が直接作用できるのは基底形だけだからである。定数が存在するのは、定義が記録され、引用でき、ユーザーが書く項の中で認識できるようにするためである。

設計判断

仮定せず導出する

このパッケージのすべての規則は導出である。以下の導出はコードが実際に行うものであり、各行がカーネル規則である。

真。 定義 $\vdash \top = t$ から対称律で $\vdash t = \top$ を得る。$\vdash t$ は REFL であるから、EQ_MP により $\vdash \top$ が得られる(logic_prop_truth_const_thm)。対称律自体も導出される。

$$\begin{aligned} &\vdash (=) = (=) && \textsf{REFL} \\ &\Gamma \vdash (=)\,s = (=)\,t && \textsf{MK\_COMB}(\cdot,\ \Gamma \vdash s = t) \\ &\Gamma \vdash (s = s) = (t = s) && \textsf{MK\_COMB}(\cdot,\ \vdash s = s) \\ &\Gamma \vdash t = s && \textsf{EQ\_MP}(\cdot,\ \vdash s = s) \end{aligned}$$

証明から真との等式へ。 $\Gamma \vdash p$ と $\vdash t$ から、DEDUCT_ANTISYM_RULE により $\Gamma \setminus \{t\} \vdash p = t$ が得られる。$t$ 自身が仮定である場合を除いて $\Gamma \setminus \{t\} = \Gamma$ であり、仮定である場合も $t$ は証明可能なので取り除いても問題ない。この「EQT_INTRO」ステップによって命題が項の中に置かれる。

連言導入。 $\Gamma \vdash p$ と $\Delta \vdash q$ から $\Gamma \vdash p = t$ と $\Delta \vdash q = t$ を得る。新しい変数 $f$ に対して、

$$\begin{aligned} &\vdash f = f && \textsf{REFL} \\ &\Gamma \vdash f\,p = f\,t && \textsf{MK\_COMB} \\ &\Gamma \cup \Delta \vdash f\,p\,q = f\,t\,t && \textsf{MK\_COMB} \\ &\Gamma \cup \Delta \vdash (\lambda f.\,f\,p\,q) = (\lambda f.\,f\,t\,t) && \textsf{ABS},\ f \notin \mathrm{FV}(\Gamma \cup \Delta) \end{aligned}$$

最後の行が $p \wedge q$ である。ABS が適用できるのは $f$ が新しいからである。

連言除去。 $\Gamma \vdash (\lambda f.\,f\,p\,q) = (\lambda f.\,f\,t\,t)$ の両辺に、MK_COMB と REFL で選択子 $\lambda x\,y.\,x$ を適用し、BETA と TRANS で両辺を簡約する。

$$\Gamma \vdash (\lambda x\,y.\,x)\,p\,q = (\lambda x\,y.\,x)\,t\,t \quad\leadsto\quad \Gamma \vdash p = t$$

対称律と、$\vdash t$ を用いた EQ_MP により $\Gamma \vdash p$ が得られる。選択子 $\lambda x\,y.\,y$ を使うと $q$ が得られる。

含意除去。 $\Gamma \vdash (p \wedge q) = p$ と $\Delta \vdash p$ から、対称律により $\Gamma \vdash p = (p \wedge q)$、EQ_MP により $\Gamma \cup \Delta \vdash p \wedge q$ を得て、連言除去により $q$ を得る。

含意導入。 $p \in \Gamma$ である $\Gamma \vdash q$ から、$\{p\} \vdash p$ との連言導入により $\Gamma \vdash p \wedge q$ を得る。また仮定からの除去により $\{p \wedge q\} \vdash p$ を得る。すると

$$\frac{\Gamma \vdash p \wedge q \qquad \{p \wedge q\} \vdash p}{(\Gamma \setminus \{p\}) \cup (\{p \wedge q\} \setminus \{p \wedge q\}) \vdash (p \wedge q) = p}\;\textsf{DEDUCT\_ANTISYM\_RULE}$$

となり、仮定集合は $\Gamma \setminus \{p\}$ である。結論は定義により $p \Rightarrow q$ である。logic_prop_imp_intro_thm は $p \in \Gamma$ を要求する。存在しない仮定を解消するには、先に弱化が必要になる。

ex falso。 $\Gamma \vdash (\lambda p.\,p) = (\lambda p.\,t)$ と任意の命題 $q$ に対し、$\vdash q = q$ との MK_COMB と 2 回の BETA により $\Gamma \vdash q = t$、したがって $\Gamma \vdash q$ を得る。否定除去は、結論を $\bot$ とする含意除去である。

選言導入。 $\Gamma \vdash p$ から、$\neg p$ を仮定し、これを $p$ に対して除去して $\bot$ を得、ex falso により $q$ を導き、$\neg p$ を解消する。

$$\Gamma \vdash \neg p \Rightarrow q \;=\; p \vee q.$$

$\Delta \vdash q$ からの右導入は、$\neg p$ を $q$ と連言にしたうえで、使われていない $\neg p$ を解消する。

選言除去は無い

プレリュードは $p \vee q$ を $\neg p \Rightarrow q$ として定義する。導入は示したとおり導出できる。除去、すなわち $p \vee q$、$p \Rightarrow r$、$q \Rightarrow r$ から $r$ を推論することはできない。これには $p$ についての場合分け、つまり排中律 $p \vee \neg p$ が必要になる。HOL では排中律は選択公理と外延性から従う(Diaconescu の定理)²2 R. Diaconescu, “Axiom of choice and complementation”, Proc. AMS 51, 1975. HOL Light は class.ml でこの方法により EXCLUDED_MIDDLE を導出している。 が、カーネルは選択公理の定理を公開しておらず、このパッケージも排中律を導出しない。正当化できない規則を提供する代わりに、カタログには or_intro_l と or_intro_r があるが or_elim は無く、タクティク層には left と right があるが場合分けは無い。

結合子定数の信頼できる認識

問題。 ユーザーは別の意味を持つ and という名前の定数を宣言できる。prop_dest_and が and という定数のどんな適用も認識するなら、タクティクが任意の項を連言として扱ってしまいうる。

選択。 デストラクタは、構造的に検査される基底形を受け付ける。結合子定数の適用は、状態がその定数の正準な定義定理を(現在の同一性で)保持しているときに限り受け付ける。install_prop_prelude は、名前と型が正しいが定義を持たないプレースホルダ定数の上へのインストールを拒否する。

理由。 認識の誤りは健全性を損なわない。すべての規則はカーネルを通じてリプレイされるからである。しかしその場合、タクティクでの明確な失敗ではなく、リプレイ時の分かりにくい失敗が生じる。また仕様は、結合子の認識が定義に裏付けられることを要求している。

1 つのカタログ、2 つのモード

問題。 exact th と apply th は意味が異なる。exact は結論がゴールである定理を必要とし、apply は帰結がゴールである含意を必要とし、その前件を新たなゴールとして残す。名前を誤ったモードで黙って使えるようにすると、失敗が遅れるか、さらに悪いことに exact が静かに apply のように振る舞ってしまう。

選択。 各カタログ項目は exact_class と apply_class を記録する。exact は前者だけを、apply は後者だけを参照する。存在はするがあるモードでは使えない名前は KnownButUnavailable に解決され、タクティク層がそれを形状または apply の不一致として報告する。ローカルな仮定名は常にカタログ名より優先され、カタログ名にフォールバックすることはない。

理由。 この表はタクティク層、prover のコーパス、対応表、ドキュメントの唯一の情報源であり、ユーザーが書ける定理名がこれらの間でずれることはない。

エラーはカーネルのみから

カーネルのエラーコンストラクタは、カーネルの外では読み取り専用である。このパッケージが返す LogicError と SigError の値は、必要な形で失敗することが分かっている小さなカーネル操作を実行して得る。これによりエラーの語彙はカーネルが所有し続ける。その代償として、エラーは具体性に欠け、多くの補助関数の失敗が TypeMismatch や AlphaMismatch として現れる。

正しさと不変条件

• 健全性。 このパッケージが返すすべての Thm はカーネル関数の結果であるから、カーネルの健全性の議論がそれをカバーする。上記の導出は、各規則が意図された用途について完全でもあることを示す。前提が規定の形をしていれば、必ず成功する。
• プレリュードの保存性。 6 つの定数は、閉じた右辺を持ち、型変数も循環も無い形で DefOK に受理される。したがってプレリュードは空の理論の保存拡大である。
• 冪等性。 install_prop_prelude(install_prop_prelude(s)) は install_prop_prelude(s) に等しい。既存の正準な定義はそのまま受理される。
• 正確なシーケント。 リプレイ補助関数は、仮定を α 同値を除いた集合として検査する。logic_prop_strengthen_to_hyps は仮定を追加するだけなので、ゴールが持たない仮定を必要とする定理は、余分な仮定付きで受理されるのではなく拒否される。
• β 正規化は証明を生成する。 logic_beta_normalize_eq と logic_normalize_prop_beta はカーネルの等式を段階的に構築する。項レベルの logic_beta_nf_* 関数は、そのような等式の右辺を返す。正規化は抽象の内部には入らず、上限がある(1 パスあたり 512 ステップ、深い形では 32 パス)。これは結合子のエンコーディングには十分である。

却下した代替案

• 結合子をカーネルのプリミティブにする。 カーネルとその健全性証明に規則が加わる。定義は信頼を一切増やさない。
• HOL Light の選言 $\forall r.\,(p \Rightarrow r) \Rightarrow (q \Rightarrow r) \Rightarrow r$。これを使うと排中律なしで除去が導出できるが、すべての選言の内部に命題上の全称量化子が入るという代償がある。プレリュードはより短いエンコーディングを使い、代わりにその限界を明示している。切り替えると、すべての選言項と、それらに基づくコーパスが変わる。
• モードを混在させたリゾルバ。 logic_prop_resolve_ref はモードを区別せずに名前を解決する。これはテスト用に残してあり、タクティク層はモード別のリゾルバを使う。

境界

• このパッケージが証明するのは命題の事実だけである。定理ヘッダの束縛子のためにタクティク層が構築するもの以外に、量化子の規則は持たない。
• 選言除去も、排中律も、古典推論も無い。
• ユーザーの定理を保存しない。カタログはソースに固定されており、名前を追加するにはコードとテストを追加する必要がある。
• 権限を追加しない。このパッケージへの変更は、健全性ではなく有用性についてレビューされる。
• 式の解析も出力も行わない。項は parser が構築し、カーネルの構造的プリンタが出力する。

Footnotes

1. J. Harrison, HOL Light Tutorial, 論理定数の節。これらの定義は Andrews の型理論 Q0 に遡る。QED の選言は HOL Light のものと異なる。後述を参照。 ↩

2. R. Diaconescu, “Axiom of choice and complementation”, Proc. AMS 51, 1975. HOL Light は class.ml でこの方法により EXCLUDED_MIDDLE を導出している。 ↩