ルール④

メタ論理

「推論可能かどうか」はdown形にした上で一階論理により判定されます。
Propの列 \(\mathcal{A}\) とProp \({\tt P}\) に対し「\(\mathcal{A}\) から\({\tt P}\)が推論可能である」ことを \(\mathcal{A}\) ▶ \({\tt P}\) と表します。
\(\mathcal{A}\) はAssumptions、\({\tt P}\) はGoalと呼ばれます。
空の列をOとします。Assumptions無しで O ▶ \({\tt P}\) となる \({\tt P}\) は恒真と言われます。例　O ▶ \(\top\)
Prop/\(\stackrel{\rm v}=\) の列 \(\mathcal{A}\) と元 \({\tt P}\) に対しても \(\mathcal{A}\) ▶ \({\tt P}\) が自然に定義されます。

私たちのシステムでは、down形の計算をphpに、一階論理の計算をProverに任せ ▶ の証明を探します。
なお、Maceでは有限モデルによる反例(▶の否定の証明)を探すことができます。

slash(PropによるProp変形)

次を満たすProp \(\Phi\) に対して、Prop変形の規則 \({\rm rule}(\Phi)\) が作られます。
　\(\Phi[0]={\Leftrightarrow},\;{\rm fvar}(\Phi[1])={\rm fvar}(\Phi[2])\)
例　自然数論で \(\Phi\) =【\(x < y \Longleftrightarrow \exists a\,(x + a = y)\)】とすると
　\({\rm rule}(\Phi)\) = 【\({\sf X} < {\sf Y}\) ⇒ \(\exists{\sf a}\,({\sf X}+{\sf a}={\sf Y})\)】

Prop \({\tt P}\) を \({\rm rule}(\Phi)\) で変形した結果を \({\tt P}\)/\(\Phi\) とします。
例　【\(0<1\)】/\(\Phi\) =【\(\exists a\,(0+a=1)\)】
内部の計算においてはprefix形で一度試行して、ダメならdown形でも試行します？
変形できるsub Propをすべて変形します。

次に注意しましょう。　\(\Phi\) ▶ \({\tt P}\Leftrightarrow{\tt P}\)/\(\Phi\)

Thm

Propの中でも真とみなされるものはThmと言われ、それもDBに蓄積されていきます。
Thmには名前が与えられます。Thmは文法的にはword(,p)とみなすことができます。

wordは通常、導入されたすぐ後に定義と思えるThmが与えられ、その名前には . が付きます。
Thmは「どのThmから推論可能か」というデータも込みで登録されることが多いです。
数学(1)の3行目の式の右側は O ▶ \({=}{.}{.}\) /\({\subset.}\) /\({=.}\) を表しています。
念の為、途中式　\({=}{.}{.}\) /\({\subset.}\) =【\(X=Y \Longleftrightarrow (\forall x\in X.x\in Y)\mathrel\&(\forall x\in Y.x\in X)\)】
一般にassumptionsは少ない方が良いので、DBへの登録は \({\subset.},{=.}\) ▶ \({=}{.}{.}\) にしません。