不完全性定理は、構築してきた記号列の幾つかと表現定理を、
述語論理で許される論理式の式変形により、証明されます。
この際に、さらに概念の説明から論理式を導く事もあります。
GALによるこの概念の説明の記述は式変形としての、
メタ記述のルールを導出する事ができます。
その際、通常のGALはSALとして、(今回にあたり)拡張された表記を
用いる事になります。
ならば例として、以下の記号から以下の説明を示すメタ記述について、
考えていきましょう。
Sgn :Q(x,y)⇔DF:¬xPrv(<y>→(y.\y1))
Xpln:Q(x,y)≡[x≠(<y>→(y.\y1))."FmtvPrf"]Prdct
こうして、上記を見比べますと、いかにも単純な変形により、
記号からその概念の解釈としての説明が導出されます。
以下がその手順(ルール)だとします。
�（儿牾鞠阿鮴擇蟒个后�
�∪擇蟒个気譴進儿牾鞠阿鯤未竜�号に置換し、再び該当の変項概念とする。
�Ｊ儿牾鞠阿僚亳十腓鯑�れ替える。
�て�力概念を一般化する。
�ッ峇昂欧鯑浬个垢襦�
SALにおいて、上記をλ世界表記の拡張として記述します。
その際の拡張記述は以下の記号です。
・(Sgn→Xpln)
・2つ目の｢@｣現況記号
・型記号｢IN:｣
・<<>>表記
・型記号｢OT:｣
では、上記例へ、具体的に� 銑い亮蟒腓鯏�用して見ます。
@(Sgn→Xpln)λPRV@⊃
IN:#1<<Q(x,y)>>⇔DF:#2<<¬>>#3<<x>>#4<<Prv>>#5<<(<y>→(y.\y1))>>
(#2="") ⇒sub(#2→｢= ｣)==#2
(#2=｢¬｣)⇒sub(#2→｢≠｣)==#2
sub(#4→"FmtvPrf")==#4
OT:#1≡[#3#2#5.#4]Prdct
拡張記述の各記号について、上記PRV関数を例として説明します。
・λ世界表記に、｢(Sgn→Xpln)｣と記述し、該当表記が、
記号から説明への変形になることを示します。
・2つ目の｢@｣現況記号は、切り出される変項概念に対し、
λxyz...と記述するところを、#1〜の順序記号で代用することを意味します。
・型記号｢IN:｣は入力を示します。つまり、以下です。
λPRV(Q(x,y)⇔DF:¬xPrv(<y>→(y.\y1)))
とすればこの場合、｢Q(x,y)≡[x≠(<y>→(y.\y1))."FmtvPrf"]Prdct｣を示します。
この際に示される記号列が、型記号｢OT:｣で表示される記号列です。
・型記号｢IN:｣で示される記号列から、変項概念を切り出し、｢<<〜>>｣で括ります。
その際に、各変項概念を示すように、｢#｣記号を使用します。
ここで付けられる番号には重複することもありえます。
・��,�△魴个進儼舛気譴慎�号を、型記号｢OT:｣にて並べ替えます。
さらに、この例をより一般的に表記するために、型記号｢IN:｣で切り出された
入力の変項概念を型記号でより一般化します。
IN:#1<<[2]TmLogFrm>>⇔DF:#2<<""/¬>>#3<<Var:>>#4<<Prv>>#5<<Gnum:>>
そして、これで� 銑い痢△茲螳貳姪�なメタ記述が完成しました。
@(Sgn→Xpln)λPRV@⊃
IN:#1<<[2]TmLogFrm>>⇔DF:#2<<""/¬>>#3<<Var:>>#4<<Prv>>#5<<Gnum:>>
(#2="") ⇒sub(#2→｢= ｣)==#2
(#2=｢¬｣)⇒sub(#2→｢≠｣)==#2
sub(#4→"FmtvPrf")==#4
OT:#1≡[#3#2#5.#4]Prdct
つまり上記は、例えば｢Prv｣なる文字列が存在する記号列は、
条件が整えば、ある種の概念の説明に変形できる事を意味しています。
さらにλPRV関数は、�イ箸靴董△茲蟯蔽韻肪峇昂欧里茲Δ奮鞠阿農睫世任�ます。
λPRV{<1,2,3,4,5>
<1,3,2,5,4>}
これは、証明に関する記号とその概念の説明に対し、
変項概念は5つに切り出され、その記号を直感的な記号の置換を経て、
上記のように並び替えれば、記号から説明、説明から記号を
出力させることができる事を示しています。
今度はこの例で(Xpln→Sgn)の変形を考えて見ます。
@(Xpln→Sgn)λPRV@⊃
IN:#1<<Q(x,y)>>≡[#2<<x>>#3<<≠>>(#4<<<y>→(y.\y1)>>).#5<<"FmtvPrf">>]Prdct
(#3=｢≠｣)⇒sub(#3→｢¬｣)==#3
(#3="") ⇒sub(#3→｢｣) ==#3
sub(#5→｢Prv｣)==#5
OT:#1⇔DF:#3#2#5(#4)
さらに、この例をより一般的に表記するために、型記号｢IN:｣で切り出された
入力の変項概念を型記号でより一般化します。
IN:#1<<[2]TmLogFrm>>≡[#2<<Var:>>#3<<=/≠>>(#4<<Gnum:>>).#5<<"FmtvPrf">>]Prdct
そして、これで� 銑い痢△茲螳貳姪�なメタ記述が完成しました。
@(Xpln→Sgn)λPRV@⊃
IN:#1<<[2]TmLogFrm>>≡[#2<<Var:>>#3<<=/≠>>(#4<<Gnum:>>).#5<<"FmtvPrf">>]Prdct
(#3=｢≠｣)⇒sub(#3→｢¬｣)==#3
(#3="") ⇒sub(#3→｢｣) ==#3
sub(#5→｢Prv｣)==#5
OT:#1⇔DF:#3#2#5(#4)
この置換群が群の性質(あみだくじの性質)から、上下の行を入れ替えたものになります。
つまり上記は、例えば｢"FmtvPrf"｣なる文字列が存在するGALの記号列は、
条件が整えば、特に｢x=｣としての記号列があれば、
ある種の不完全定理上の記号列にできる事を意味しています。
まとめると、λPRV関数は以下のようになります。
@λPRV@⊃
(Sgn→Xpln)⊃
IN:#1<<[2]TmLogFrm>>⇔DF:#2<<""/¬>>#3<<Var:>>#4<<Prv>>#5<<Gnum:>>
(#2="") ⇒sub(#2→｢= ｣)==#2
(#2=｢¬｣)⇒sub(#2→｢≠｣)==#2
sub(#4→"FmtvPrf")==#4
OT:#1≡[#3#2#5.#4]Prdct
(Xpln→Sgn)⊃
IN:#1<<[2]TmLogFrm>>≡[#2<<Var:>>#3<<=/≠>>(#4<<Gnum:>>).#5<<"FmtvPrf">>]Prdct
(#3=｢≠｣)⇒sub(#3→｢¬｣)==#3
(#3="") ⇒sub(#3→｢｣) ==#3
sub(#5→｢Prv｣)==#5
OT:#1⇔DF:#3#2#5(#4)
λPRV{Sgn <1,2,3,4,5>
Xpln<1,3,2,5,4>}
同様に、以下の例を考えていきます。
Sgn :@Prvbl(~¬q<m,n>~)
Xpln:∃.(~¬q<m,n>~."FmtvPrf")
ここで説明に対し、GALによる書き換えを行います。
(∃.(~¬q<m,n>~."FmtvPrf")) ≡ (~¬q<m,n>~.∃."FmtvPrf")
そこで具体的なλPRB関数は以下のようになります。
@λPRB@⊃
(Sgn→Xpln)⊃
IN:#1<<>>#2<<@Prvbl>>(#3<<~¬q<m,n>~>>)
sub(#2→｢∃."FmtvPrf"｣)==#2
OT:(#3.#1#2)
(Xpln→Sgn)⊃
IN:(#1<<~¬q<m,n>~>>.#2<<>>#3<<∃."FmtvPrf">>)
sub(#3→｢@Prvbl｣)==#3
OT:#2#3(#1)
入力の変項概念を型記号でより一般化し、置換群を示します。
まとめると、λPRB関数は以下のようになります。
@λPRB@⊃
(Sgn→Xpln)⊃
IN:#1<<""/¬>>#2<<@Prvbl>>(#3<<Gnum:>>)
sub(#2→｢∃."FmtvPrf"｣)==#2
OT:(#3.#1#2)
(Xpln→Sgn)⊃
IN:(#1<<Gnum:>>.#2<<""/¬>>#3<<∃."FmtvPrf">>)
sub(#3→｢@Prvbl｣)==#3
OT:#2#3(#1)
λPRB{Sgn <1,2,3>
Xpln<3,1,2>}
同様に以下の例を考えていきます。
Sgn :<y>→(y.\y1)
Xpln:y.Diagnl_iz
そこで具体的なλDGR関数は以下のようになります。
@λDGR@⊃
(Sgn→Xpln)⊃
IN:<#1<<y>>>→(#1<<y>>.\y1)
OT:<#1>.Diagnl_iz
(Xpln→Sgn)⊃
IN:#1<<y>>.Diagnl_iz
OT:<#1>→(#1.\y1)
入力の変項概念を型記号でより一般化します。
まとめると、λDGR関数は以下のようになります。
@λDGR@⊃
(Sgn→Xpln)⊃
IN:<#1<<GNum:>>>→(#1<<GNum:>>.\y1)
OT:#1.Diagnl_iz
(Xpln→Sgn)⊃
IN:#1<<GNum:>>.Diagnl_iz
OT:<#1>→(#1.\y1)
同様に以下の例を考えていきます。
Sgn :y<y>
Xpln:y.Diagnl_iz
そこで具体的なλDGO関数は以下のようになります。
@λDGO@⊃
(Sgn→Xpln)⊃
IN:#1<<y>><#1<<y>>>
OT:#1.Diagnl_iz
(Xpln→Sgn)⊃
IN:#1<<y>>.Diagnl_iz
OT:#1<#1>
入力の変項概念を型記号でより一般化します。
まとめると、λDGO関数は以下のようになります。
@λDGO@⊃
(Sgn→Xpln)⊃
IN:#1<<GNum:>><#1<<GNum:>>>
OT:#1.Diagnl_iz
(Xpln→Sgn)⊃
IN:#1<<GNum:>>.Diagnl_iz
OT:#1<#1>
上記のSALを適用する箇所を、以下に｢【関数】｣として示します。
<<ε>>Dcsn_¬abl.Sttr
<<ζ>>第2(¬Cmplt)Thrm