公理系の定義

公理系の定義を試みます。

その前に、準備。
閉項全体をClosedTermとします。
閉論理式全体をClosedFormとします。
自由変数をn個含む項の全体をOpneTerm(n)とします。
自由変数をn個含む論理式の全体をOpneForm(n)とします。

P[x]を自由変数xを含む論理式ならば、"P[x]"∈OpenForm(1)
P[x,y]を自由変数x,yを含む論理式ならば、"P[x,y]"∈OpenForm(2)

記号列はそれを強調するために「"」で囲むことにします。

"a"∈ClosedTerm、"P[x]"∈OpenForm(1)ならば、"P[a]"∈ClosedForm
"a"∈ClosedTerm、"P[x,y]"∈OpenForm(2)ならば、"P[a,y]"∈OpenForm(1)
"F[z,w]"∈OpenTerm(2)、"P[x,y]"∈OpenForm(2)ならば、"P[x,F[z,w]]"∈OpenForm(3)
このような感じで代入を表わすことにします。
その際、内部の束縛変数は上手く立ち回っているとします。

genSystem := { ((U,A),Z) | U⊂ClosedTerm ∧ A,Z⊂ClosedForm ∧ Intersect({ X | A⊂X⊂ClosedForm
∧ ∀p∀q(("p"∈X ∧ "q"∈ClosedForm ∧ "(p⇒q)"∈X) ⇒ "q"∈X)
∧ ∀p((∃a("a"∈U ∧ "p[a]"∈X)) ⇒ "∃v(p[v])"∈X)
 ∧ ∀p("∀v(p[v])"∈X ⇒ ∀a("a"∈U ⇒ "p[a]"∈X))
 ∧ ∀p(∀a("a"∈U ⇒ "p[a]"∈X) ⇒ "∀v(p[v])"∈X)
})=Z }

genSystem(U,A)は(U,A)で生成される公理系
これが（私が勝手に考える）公理系の定義です。

説明
「∀p∀q(("p"∈X ∧ "q"∈ClosedForm ∧ "(p⇒q)"∈X) ⇒ "q"∈X)」
これは閉論理式qを公理系に取り込む規則を表わしています。

「∀p((∃a("a"∈U ∧ "p[a]"∈X)) ⇒ "∃v(p[v])"∈X)」　　･･･(A)
これは形式"∃v(p[v])"を公理系に取り込む規則を表わしています。

「∀p("∀v(p[v])"∈X ⇒ ∀a("a"∈U ⇒ "p[a]"∈X))」　　･･･(B)
これは形式"∀v(p[v])"をすべての"a"∈Uで"p[a]"の形に分解して公理系に取り込む規則を表わしています。

「∀p(∀a("a"∈U ⇒ "p[a]"∈X) ⇒ "∀v(p[v])"∈X)」　　･･･(C)
これはすべての"a"∈Uで"p[a]"が公理系に含まれていたら形式"∀v(p[v])"を公理系に取り込む規則を表わしています。

※(A)(B)(C)は形式的には生煮えです。束縛変数の扱いが曖昧になっています。とくに束縛変数vをどのように選んでいるかなど。内部的な束縛変数の置き換えによる同値性を利用するような仕掛け（そういう同値類のこと）が必要かも知れません。

"p[a]"の形のものが公理系にあれば、"∃v(p[v])"が必ず公理系にあることになります。
"∃v(p[v])"∈X ⇔ {v|v∈U∧p[v]}≠∅なので、"p[a]"がどのくらい公理系にあるかで{v|v∈U∧p[v]}のボリュームが測れます。
もしすべての"a"∈Uで"p[a]"の形のものが公理系にあれば、"∀v(p[v])"も公理系にあるということになります。
"∀v(p[v])"∈X ⇔ {v|v∈U∧p[v]}=U
もちろん、"∃v(p[v])"そのものが公理のとき、"∃v(p[v])"が公理系にあるにもかかわらず、"p[a]"の形のものが公理系にない可能性もあります。

negSystem := { (A,Z) | A,Z⊂ClosedForm ∧ { "￢p" | "p"∈A }=Z }
否定系とでもしておきます。

(U,A)は無矛盾な公理系 :⇔ Cap(genSystem(U,A),negSystem(genSystem(U,A)))=∅

※Cap(X,Y):=(X∩Y)、Cup(X,Y):=(X∪Y)とします。
※今後、∩や∪より、CapやCupの方を頻繁に使うかもしれません。

次の性質を予想します。というかそうなってほしいという希望ですね。
①∀U∀A∀B(A⊂B⊂genSystem(U,A) ⇒ genSystem(U,B)=genSystem(U,A))
②∀U∀A((U,A)は無矛盾な公理系 ⇒ (ClosedForm＼Cup(genSystem(U,A),negSystem(genSystem(U,A))))≠∅)
③∀U∀A(￢((U,A)は無矛盾な公理系) ⇒ genSystem(U,A)=ClosedForm)

②の意図していることは、無矛盾な公理系には否定系との隙間に必ず何らかの論理式が入り込むというものです。

公理系のボリュームを変えないで、極小となるようなUとAを求めるのが公理系の理論の目的かもしれません。

興味深い公理について考えて見ます。

任意の"P[x]"∈OpenForm(1)に対して、"∀y(y∈{x|P[x]} ⇔ P[y])"は公理か？あるいは公理にすべきではないか？

"P"は論理式で束縛変数uは含んでいて束縛変数vは含んでいないとき、"Q"は"P"の中のuをvに置き換えた記号列のとき、"(P⇔Q)"は公理か？あるいは公理にすべきではないか？

などなど。