Prop
p-Formを指し示すPropというものを導入します。Propを紹介するときは、それが指し示すp-Formを右側に書きます。
「一階言語のwordの定義」と思えるPropには . が付きます。
\(=\) の定義は \(=\) の定義から自然に誘導されます。
\({=.}\)【\(X = Y \Longleftrightarrow X = Y\)】
次の \(\emptyset\) の定義で \({\perp}\) は \(x \neq x\) とされることが多いです。
\({\emptyset.}\)【\(\emptyset = \{ x \mid {\perp} \} \)】
\(\downarrow\) は次のように計算されます。正確には、左辺はPropでなくp-Formにするべきですが…
\(=.\) ≃【\(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)】
\(\emptyset.\) ≃【\(\forall x \, ( x \in \emptyset \Longleftrightarrow {\perp} )\)】
p-FormをPropとして扱いたいときには \('\) を使用します。p-Formのtxtと ' の間にスペースは入れません。例 \('\top'\)
Thm
p-Formに対しては \(\downarrow\) の結果は一階言語になります。
「推論可能かどうか」は \(\downarrow\) をした上で一階論理により判定されます。
なお、一階論理の（等号公理を含めた）公理・推論規則は既知とされます。
また、推論可能性は p-Form\(/{\stackrel{\rm v}=}\) に対しても自然に定義されます。
例 \('x \neq y'\,{\blacktriangleright}\,'{\perp}'\)
Propの列としては、空の列を \(\text{O}\)、列の要素の区切りは太コンマ \({\bf ,}\,\) にします。
例 \(\text{O}\,{\blacktriangleright}\,'x = x'\)
特別なProp列
\(\mathbb{D}.\) は \({\tt w}.\) (\({\tt w}\)はword) という形の全てのPropの列\({=}.{\bf ,}\,\emptyset.{\bf ,}\,\cdots\)
です。「\({\mathbb{D}.}\blacktriangleright{\tt P}\)」 は「定義を使って \({\tt P}\) が推論可能」と読めます。
分出公理を表現するためのword(c,p) \(\text{ax_s}\) というものがあります。
\(\text{Ax_s}\) は \(\text{ax_s}({\tt C})\) (\({\tt C}\)はc-Form) という形の全てのPropの列です。
これは無限の列です。しかし、\(\text{Ax_s}\blacktriangleright{\tt P}\) のとき、有限部分列 \(\mathcal{A}\) で \(\mathcal{A}\blacktriangleright{\tt P}\) となるものが存在します。
Propの列 \(\mathcal{P}\) から Prop \(\tt{P}\) だけ除いた列を \(\mathcal{P}\,\text{-}\,\tt{P}\) とします。
Thm付のProp
Propは紹介時に「どのPropから推論可能か」というThmが付くことがあります。例えば\(\emptyset0\)【\(x \notin \emptyset\)】\(\,{\blacktriangleleft}\,{\emptyset.}\)
具体的にどの定義を使うかを一々気にしたくないので、次のように書きたくなるでしょう。
\(\emptyset0\)【\(x \notin \emptyset\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
上式の右部分をクリックしたときに出てくるものは、証明のためのThmになります。\(\mathbb{D}.\)は大きすぎるので、具体的に\(\emptyset.\)を教えてあげる方が親切です。
難しいPropの場合には、証明のヒントなども記載されることがあります。
Thmの証明探索
私たちはThmの証明を機械に探索させます。それはいくつかのsoftwareを組み合わせて遂行します。
主要なものはphpとProverで、補助的にいくつかの計算softwareを使用します？
最終段階はProverに任し、Proverに渡す文字列はphpで作成します。
機械は証明があったときにのみ「あった」と答えてくれます。「そのThmは正しい」と言ってもらえると、安心します。
Proverによって出力された証明の中身はまだ利用できていません。
証明探索の効率を上げることが私たちにとって最重要の課題です。
Proverをいじるのは難しそうなので、phpを洗練していきます。人間にとって簡単でもProverには難しいことがあるので、まずはそこをphpで補助します。現状ではphpでは一定の規則に従った計算をするだけで探索と呼べる事はしていません。Proverとやりとりをしながら探索をする？