単語＠
!のdef1 … all #x all #y\,(@ #P #x #y xr #x = #y)
代入を表現する \(@\) があります。さらに\(@\)を含んで良いものとして #@Form を定義します。
・\({\tt P}\)が#@Form, \({\tt x}\)が#var, \({\tt T}\)が#@Set ⇒ \(@{\tt PxT}\)が#@Form？
・\({\rm fvar}(@{\tt PxT})={\rm fvar}({\tt P})\cup{\rm fvar}({\tt T})\setminus\{\tt x\}\) if \({\tt w}\)が#var
また\(@\)は同値類の代入として計算されます。
prover形
普通は( )が大量に付きます。要らないものもありますが…
varのprover表記はx,y,z,u,v,wで始まるものになります。
arityが2のconn, =, \ne はinfixにされます。
例 【\(\top\&{\perp}\)】→ $T & $F
\negと上記以外のwordはordinaryタイプとされます。
例 \sin【prover : sin】という arity : 1 のwordがあるとき \sin x【prover : sin(x)】
私たちのシステムでは、down形の計算をphpに、一階論理の計算をProverに任せ定理の証明を探します。なお、Maceでは有限モデルによる反例(定理の否定の証明)を探すことができます。
syntax処理
entity→decent→prefix→down と処理されていきます。
右に行くほど、使用できる単語が減り人間は見たくないものになります。
\, \; \! は entity→decent の際に無視されます。
prefixとdownは入れ子配列になります。
Propに対してはdown形は一階言語であり、各wordをprover単語に変換するとprover入力用の文字列になります。例 【\(\neg ⊤\)】→ - $T
「var以外の単語と$単語」の列を $列 と言います。
その中でも「{ で始まり } で終わり、$Varの直後に$単語が続かない」ものを $列* と言います。
新しいword？
新しいwordを作る関数 - を用意します。
同値Prop \(\Phi\) に対し - \(\Phi\) はtex表記やgramなどの基本データが\(\Phi[1][0]\)と同じwordとします。
- により作られるwordは、定理の証明内で良く使用されます。
def …
これを使うと例えば次のように計算できます。
【\(x = y\)】≃【\(\forall z \, ( z \in x \Leftrightarrow z \in y )\)】
\({\tt w}\)で始まるdefが無いword \({\tt w}\) に対して 、tex表記やgramなどの基本データが同じword \({\tt w}\)* を作り、\({\tt w}\)*で始まるdefを与えることがあります。
\({\tt w}\)* : からは \({\tt w}\). が自動で作られます。≃は \(=\)または\(\Longleftrightarrow\) に置き換えられます。
abbrの利用
abbrは次のように「紹介」されます。abbr …【\( \forall {\sf x} {\sf A} . {\sf P} \)】≈【\(\forall {\sf x} \, ( {\sf x} {\sf A} \Rightarrow ( {\sf P} ) )\)】
上のabbrについては次が付くべきです(が、明記されません)。
代入条件 \({\sf A}\) : p1断片, \({\sf P}\) : Prop
ただし\({\tt pT}\) (\({\tt p}\)がword(ss,p) or word(sc,p)、\({\tt T}\)がSet or Class)の形の単語列をp1断片と言います。
\({\sf A}\)を\({\sf p} {\sf T}\)などとした方が分かりやすいかもしれません。
{ } による塊が崩れないよう、内側から計算する方が良いでしょう。
入れ子列として表記するときには [ ] を使いスペースを区切りとします(一番外側の [ ] は略します)。tex表記はしません。例 \((\)x [y z]\()[1][0]=\) y