lean4-logicでの様相論理および直観主義論理についての形式化された事実のリスト
更新記録
はじめに
Summary
例えば主に次の事実が形式化されています.
算術に関する議論はおそらく無い.多分初だろうと思われる.
詳細や,実際の定義などは以下のBookから参照してください.
特にゴールもなく細かな事実を散発的に形式化しているので色々散らかった結果になっている.
このリストでは私が形式化した事実をいくつか説明していくことにする.
私が英語を書くのが面倒なのと,下書きの意味を込めて適当に書いていく.
このリストはいずれちゃんとしたドキュメントに纏める.
留意
わざわざ書くのが面倒なので,以下の断りをいれておきます.
様相論理も同様に命題論理のものとする.
字体と記号の用法
$ \TeXで普通に数学的対象として書くときは
公理は$ \sf K, 4, 5, LEMなどのSans-Serifの太字で\sfで書く.
論理は$ \bf K,S4,S5, Int, ClなどSerif体の太字で\bfで書く.
Lean 4上での公理と論理もそれに従いコード内では下のように書く. 公理は𝗞のように
論理は𝐈𝐧𝐭のように
フォントの問題でどっちも同じように表示される場合は文脈で適当に補ってほしい.
論理式$ A,B,C,...として$ \TeXでは書くが,Lean 4上ではp, qなどを使っているので適当に解釈し直してほしい. 命題論理の言語$ \mathscr{L}_\mathrm{P}は全て$ \lnot,\to,\land,\lorの記号を持っているとし,その上に最小論理をHilbert流演繹体系を定義し,追加で公理(図式)を入れるという方法で演繹体系を定めている. 論理をどう定義するかは面倒な議論がある
一般的には証明体系または意味論のどちらかによって,証明できる / 正しい論理式の集合を論理とすることが多い.
この集合が証明体系側と意味論側で一致することを健全性・完全性と定義すればよい
が,扱いづらいので,今回我々の形式化では演繹体系自体をそのまま論理と呼ぶことにする.
大雑把に言えば次:ここで$ \frak HはHilbert流を意味する
Def
$ \mathfrak{H}(\mathsf{Basic}) = \mathbf{Min}:最小論理 $ \mathfrak{H}(\mathsf{Basic} + \mathsf{EFQ}) = \mathbf{Int}:直観主義命題論理 $ \mathfrak{H}(\mathsf{Basic} + \mathsf{LEM}) = \mathbf{Cl}:古典命題論理 $ \sf Basicは基本的な公理で,
例えば$ \landの除去$ A \land B \to Aや$ \toの公理(公理S)$ A \to B \to Bなど
一つ注意が必要なのが否定に関する同値性で,$ \lnot A \leftrightarrow A \to \botを導入している.
言語自体ではこれを略記で導入していないことに注意せよ.
$ \sf EFQは爆発律,$ \sf LEMは排中律である. 二重否定除去$ \sf DNEなどは排中律から導かれることなどは下のHilbert流の証明の書き下しなどを見よ. $ \sf Basicは今後入っているものとして省略する.
Def: Kripke意味論
今回は台集合/あるいは世界$ Wを集合ではなく型によって定義している.
フレーム$ F = \lang W, \prec \rangに関する制約は反射的(Reflexive),推移的(Transitive),逆反射性?(Antisymmetric)を要請する. モデル$ M = \lang W, \prec, V\rangでは付値$ Vに遺伝性を要請する. $ x \prec yで,$ V(x,a) = 1 \implies V(y,a) = 1
memo
Def: フレームクラスの定義性
公理によるフレームクラスの定義性
様相論理と同じように,「公理がフレームクラスを定義する.」という概念を定義する.
例えば
爆発律$ \sf EFQは全てのフレームクラスを定義する.すなわち $ F \vDash \mathsf{EFQ}
弱排中律$ \sf wLEMは合流的なフレームのクラスを定義する. $ F \vDash \mathsf{wLEM}$ \iff$ Fは合流的
公理$ \sf Axによって定義されるフレームクラスを$ \mathbb{F}(\mathsf{Ax})と書くことにする.
$ \mathfrak{H}(\mathsf{Ax}) \vdash A \implies \mathbb{F}(\mathsf{Ax}) \vDash A
$ \mathsf{Ax}がカノニカルなら,$ \mathbb{F}(\mathsf{Ax}) \vDash A \implies \mathfrak{H}(\mathsf{Ax}) \vdash A
ただし$ \mathsf{Ax}がカノニカルとは,$ \mathsf{Ax}のカノニカルモデル$ \mathcal{M}^+_\mathsf{Ax}について$ \mathcal{M}^+_\mathsf{Ax} \vDash \mathsf{Ax}となることを指す. 特に$ \sf EFQはカノニカルなので,$ \bf IntはKripke完全.
rmk
メモ
論理式の集合のペア(タブロー)を考えたほうが遥かに簡単に済む
Lean 3での証明があるが,これは↑の方法で,今回の形式化のほうが洗練されている(と思う). Main Thm
すなわち,排中律は$ \bf Intでトートロジーではない. すなわち,何らかの論理式$ Aがあって,$ \mathbf{Int} \nvdash A \lor \lnot Aが成り立つ.
証明のスケッチ
Cor
前者は排中律が証明できる(公理として持つ)から.
メモ
証明体系$ \mathcal{S},任意の論理式$ A,Bについて
$ \mathcal{S} \vdash A \lor Bのとき$ \mathcal{S} \vdash Aまたは$ \mathcal{S} \vdash Bが言えるなら,選言特性を持つという. memo
ここで我々の形式化では$ \mathcal{S}として論理$ \Lambdaを取ったり理論$ Tを取ったりすることが出来る.
Thm
$ \bf Intは選言特性を持つ.
証明のスケッチ
対偶を取り,$ A \lor Bが成り立たないKripkeモデルを$ Aと$ Bが成り立たないモデルから実際に構成する.完全性より従う. メモ
これに基づいて形式化した.若干間違っているかもしれない
$ \mathbf{Int} \vdash \lnot \lnot A \iff \mathbf{Cl} \vdash A
Cor
$ \mathbf{Int} \vdash \lnot A \iff \mathbf{Cl} \vdash \lnot A
これはそのうち書き換わる.
命題論理の言語$ \mathscr{L}_\mathrm{P}に$ \Box,\Diamondを追加した言語をStandradr Modal Logicの言語$ \mathscr{L}_\mathrm{M}とし,更に次の略記を定義する.
$ \Diamond A \equiv \lnot \Box \lnot A
memo
ただし直観主義様相論理ではこの略記は必ずしも必要なく,またそもそも$ \Diamondすらないものもある. そのため現在公理$ \Diamond A \leftrightarrow \lnot \Box \lnot Aとして導入するように定義を書き直している
memo
Sect. 様相論理の公理たち
よく知られている公理を並べていく
$ \mathsf{K} \equiv \Box(p \to q) \to \Box p \to \Box q
$ \mathsf{4} \equiv \Box p \to \Box \Box p
TODO: 様相論理についてまだ書いてないこと
以下はそのうちちゃんと書く
TODO