1
p-Formに対しては翻訳の結果は一階言語になるので一階論理を利用できます。なお、一階論理の（等号公理を含めた）公理・推論規則は既知とされます。
Prop
何度も使用されるp-Formに名前を与えるためにPropというものを導入します。
Propを紹介するときは、それが指し示すp-Formを右側に書きます。
word(,s)に \(\emptyset\) があります。次の定義で \({\perp}\) は \(x \neq x\) とされることが多いです。
\0.【\(\emptyset = \{ x \mid {\perp} \}\)】
convertは次のように計算されます。正確には、左辺はPropでなくp-Formにされるべき？
\0. ≃【\(\forall x \, ( x \in \emptyset \Longleftrightarrow {\perp} )\)】
p-FormをPropとして扱いたいときには ` ` を使用します。p-Formのtxtと`の間にスペースは入れません。
例 `true`
` はFormやPropのtxtで使用できません。
Thm
「推論可能かどうか」は翻訳をした上で一階論理により判定されます。
なお推論可能性はp-Formの同値類に対しても自然に定義されます。
Prop \({\tt P}\) と Propの列 \(\mathcal{A}\) に対し「\({\tt P}\) が \(\mathcal{A}\) から推論可能である」ことを \({\tt P}\) < \(\mathcal{A}\) と表し、この形の式をThmと呼びます。\({\tt P}\) はgoal、\(\mathcal{A}\) はsosと呼ばれます。
Propの空列を O とします。例 `x = x` < O
列の要素の区切りは ， にします。txtにおいて前後のスペースは略せます。例 `false` < \0.，`x in \0`
＜ を使っていたけど < でよくね？区切り , でよくね？
特別なProp列
\({\tt w}.\) (\({\tt w}\)はword) という形の全てのPropの列 \0.，… を W. とします。
「\({\tt P}\) < W.」は「定義を使って \({\tt P}\) が推論可能」と読めます。
W. は無限の列ですが、\({\tt P}\) < W. のとき有限部分列 \(\mathcal{W}\) で \({\tt P}\) < \(\mathcal{W}\) となるものが存在します。
aliasを導入する利点に W. を大きくできることがあります。
Propの列 \(\mathcal{P}\) から Prop \({\tt P}\) だけ除いた列を \(\mathcal{P}\,\text{-}\,{\tt P}\) とします。Prop \({\tt P}\), \({\tt Q}\) を除いた列は \(\mathcal{P}\,\text{-}\,{\tt P}\,\text{-}\,{\tt Q}\)
p-Form,Propの紹介①
「数学の教科書」には多くのp-Formが載ります。
その際、公理と呼ばれるもの以外は、他のPropからの推論が付きます。
【\(x \notin \emptyset\)】\(\blacktriangleleft\)
具体的にどの定義を使うかを一々気にしたくないので、次のように書きたくなるでしょう。
【\(x \notin \emptyset\)】\(\blacktriangleleft\)
しかしproverには無限長のsosを入力できません。
2
Thm証明の最終計算はproverに任せますが、その前にphpでもFormの変換をします。
そのためにProp関数が導入されます。/ や &l などがProp関数となります。それらはPropとして使用できません。
/
prop関数の中でも最もよく使用されるものが2項関数の / です。\({\tt P}\) \({\tt =}\) \({\tt X}_1 * {\tt X}_2\) (\(*\) は \(=\) か \(\Leftrightarrow\) またはそれらのalias) のとき「\({\tt X}_1\) を \({\tt X}_2\) に変形するという規則」を rule(\({\tt P}\)) とします。
rule(\(\forall {\tt xP}\)) = rule(\({\tt P}\)) とします。
Prop \({\tt A}\) に対し、rule(\({\tt P}\)) を適用した結果を \({\tt A}\) / \({\tt P}\) とします。例 【\(a \notin \emptyset\)】/ \0. ≃【\(\neg {\perp}\)】
変換できる部分Formはすべて変換します。
/ の後にはPropの列も入ります。Propの列 \(\mathcal{P}\) に対し / \(\mathcal{P}\) は
rule(\({\tt P}\)) (\({\tt P}\)は\(\mathcal{P}\)に含まれる)
で変換できる部分Formをすべて変換します。
/ の類似物
部分Formに対してruleを適用したいことがあります。convertをしたときの場所で指定できます。例えば \([{\tt n}]\) の部分Formに対して / を適用することを /\({\tt n}\) と書き、【\(a \notin \emptyset\)】/1 \0. ≃【\(\neg {\perp}\)】 となります。
\([{\tt m}][{\tt n}]\) の部分Formに対して / を適用することを /\({\tt mn}\) と書きます。この規則だと9までしか…
// \({\tt P}\) は / \({\tt P}\) を継時的にできる限り行います。
例 【\(\emptyset \subset X\)】// W. ≅ 【\(\forall x ( x \in \emptyset \Rightarrow x \in X )\)】/ W. ≅ 【\(\forall x ( {\perp} \Rightarrow x \in X )\)】
/ や /\({\tt n}\) などはL結合とされます。例 \({\tt P}\) / \({\tt Q}\) / \({\tt R}\) = (\({\tt P}\) / \({\tt Q}\)) / \({\tt R}\)
p-Form,Propの紹介②
次に注意しましょう。 \({\tt P}\Leftrightarrow\) (\({\tt P}\) / \({\tt Q}\)) < \({\tt Q}\)\({\tt P}\) / \({\tt Q}\) < \(\mathcal{A}\) なら \({\tt P}\) < \({\tt Q}\) , \(\mathcal{A}\) となります。
一般にsosは少ない方が証明が簡単になります。/ を積極的に使用し、上のp-Form紹介は次のものにした方が良いです。
【\(x \notin \emptyset\)】\(\blacktriangleleft\)
/ W. は高速に計算できるので、実際の「数学の教科書」では次のように記述されています。
【\(x \notin \emptyset\)】\(\blacktriangleleft\)
Propの2分割
難しいThmの証明は何段階かに分けるために、分割関数 &l, &r, <=, => があります。1項Prop関数です。
\({\tt P}\) \({\tt =}\) \({\tt Q}_1\) and \({\tt Q}_2\) のとき \({\tt P}\) &l \({\tt =}\) \({\tt Q}_1\) , \({\tt P}\) &r \({\tt =}\) \({\tt Q}_2\)
\({\tt P}\) \({\tt =}\) \({\tt Q}_1\) <=> \({\tt Q}_2\) のとき \({\tt P}\) <= \({\tt =}\) \({\tt Q}_2\) => \({\tt Q}_1\) , \({\tt P}\) => \({\tt =}\) \({\tt Q}_1\) => \({\tt Q}_2\)
2段書きにしたい
さらに分割関数 \(*\) に対し
(\({\tt P}\Rightarrow{\tt Q}\)) \(*\) \({\tt =}\) \({\tt P}\Rightarrow\) (\({\tt Q}\) \(*\))
(\(\forall{\tt xP}\)) \(*\) \({\tt =}\) \(\forall{\tt x}\)(\({\tt P}\) \(*\))
Thmの分割
次に注意しましょう。 \({\tt P}\Longleftrightarrow {\tt P}\) &l \(, {\tt P}\) &r < O
\({\tt P}\) < \(\mathcal{A}\) を \({\tt P}\) &l, \({\tt P}\) &r < \(\mathcal{A}\) と分割して証明させることが行われます。
分配則みたいに \({\tt PX}\) < \(\mathcal{A}\), \({\tt PY}\) < \(\mathcal{B}\) を \({\tt P}\) [ \({\tt X}\) < \(\mathcal{A}\) | \({\tt Y}\) < \(\mathcal{B}\) ] と表し、このような式を SepThm と言います。
入れ子にできます。\({\tt P}\) が \({\tt Q}\Longleftrightarrow{\tt R}_1,{\tt R}_2\) の形なら、\({\tt P}\) を示すのに \({\tt P}\) [<= < \(\mathcal{A}\) | => [&l < \(\mathcal{B}\) | &r < \(\mathcal{C}\)]] と3分割できます。
分割関数 \(*\) に対し \(*\) < O は略せます。\({\tt P}\) [&r < \(\mathcal{A}\)] は \({\tt P}\) [&l < O | &r < \(\mathcal{A}\)] の略です。
3
p-Form,Propの2形
教科書ではきれいな形で紹介され、それとは別の「実用形」を持つことがあります。例えばCap._【\(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)】
を教科書形とし、実用形は次のものにすることができます。
Cap.【\(x \in \bigcap \mathcal{X} \Longleftrightarrow \begin{cases} X \neq \emptyset \Rightarrow \forall X \in \mathcal{X} . x \in X \\ X = \emptyset \Rightarrow x \in \bigcap \mathcal{X} \end{cases}\)】\(\blacktriangleleft\)
\({\tt P} \Longrightarrow {\tt A} \Leftrightarrow {\tt B}\) と \({\tt A} \Longleftrightarrow \begin{cases} {\tt P} \Rightarrow {\tt B} \\ \neg {\tt P} \Rightarrow {\tt A} \end{cases}\) が論理同値であることに注意しましょう。
実用形は推論で使用するのに適した形が選ばれ、補足のページに載ります。
/ Cap._ は定義されていませんが / Cap. ならあります。
また / W. がnon-stopになるのを防ぐために Cap. の右辺では Cap ではなく Cap_a が使われています。
Train
一般には証明は長くなり、 \(\blacktriangleleft\) の注釈には色々なデータの列が記述されます。
それは Train と呼ばれます。各データは vehicle と呼ばれ ;; で区切られます。
通常、Trainの先頭のvehicleはThmになります。
:= で代入を作る式がvehicleになることもあります。
補題はよく使用されますが、次のような形になります。
prop ＜ le ;; le ＜ O ;; le := `form`
論理同値
!で始まるPropはp-FormでないFormを指示します。例えば!OA【\(( P \mathbin{\rm o\!r} Q ) \Rightarrow R \Longleftrightarrow P \Rightarrow R , Q \Rightarrow R\)】
これらは論理同値な変形を行うためにあります。
例 【\(( x \in A \mathbin{\rm o\!r} x \in B ) \Rightarrow x \in C\)】 / !OA ≅ 【\(x \in A \Rightarrow x \in C , x \in B \Rightarrow x \in C\)】
// は / を継時的に適用します。今は / になっているので要変更。
例 【\(( P \mathbin{\rm o\!r} Q \mathbin{\rm o\!r} R ) \Rightarrow S\)】 // !OA ≅ 【\(P \Rightarrow S , Q \Rightarrow S , R \Rightarrow S\)】
一旦【\(( P \mathbin{\rm o\!r} Q ) \Rightarrow S , R \Rightarrow S\)】と変形されてもう一度変形されます。