この記事はMathematical Logic Advent Calendar 2019の8日目の記事です。 もともと「C[0,1]の中の微分可能関数全体がΠ^1_1完全なこと」という記事を書く予定でしたが、予定変更です。
集合論の言語の有限構造がZFCの各公理を満たすか判定するプログラムをOCamlで書きました。 ただし、分出公理図式と置換公理図式はそれぞれ無限個公理があるわけですが、それらについてはそのすべてのインスタンスを満たすことを判定します。
たとえば、Kunenの"The Foundations of Mathematics"に載っている7つの有限モデルについて各公理を確かめてみます。
図は邦訳『キューネン数学基礎論講義』(訳: 藤田博司)より抜粋です。 ノードxからノードyに辺が貼ってあったら、x∈yの意味です。
ついでに次のモデルも追加しておきます。
| 外延 | 基礎 | 分出 | 対 | 和 | 置換 | 無限 | べき | 選択 | |
|---|---|---|---|---|---|---|---|---|---|
| モデル1 | 1 | 1 | 1 | 0 | 1 | 1 | 0 | 0 | 1 |
| モデル2 | 1 | 0 | 0 | 1 | 1 | 1 | 0 | 1 | 1 |
| モデル3 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 1 | 1 |
| モデル4 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 |
| モデル5 | 0 | 1 | 1 | 0 | 1 | 0 | 0 | 0 | 1 |
| モデル6 | 1 | 1 | 0 | 0 | 1 | 0 | 0 | 0 | 1 |
| モデル7 | 1 | 1 | 1 | 0 | 1 | 0 | 0 | 0 | 1 |
| モデル8 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
0がfalse、1がtrueを意味しています。
なお、確かめるのがナンセンスなものも含まれていることに注意してください。たとえば、無限公理は後続者の一意存在、選択公理は二つの集合の共通部分の一意存在がないと意味があるとはいいづらいです。
分出公理と置換公理をどう確かめているか
分出公理と置換公理はそれぞれ無限個の公理からなるので素朴に考えたら有限時間で判定できるか怪しいです。 ですが、できます。 まず、分出公理 \begin{align} \forall Z \forall \vec{p} \exists Y \forall x (x \in Y \iff x \in Z \land \varphi(x, z, \vec{p})) \end{align} はパラメータ$\vec{p}$を使えることを考えれば、どんなオブジェクト$Z$についてもその部分集合の候補というのは論理式で定義可能になっています。 たとえば、$Z$の子供が$x_1, \dots, x_n$ならば$x = x_1 \lor x = x_3$によって$\{ x_1, x_3 \}$が定義可能になっています。 したがって、どんなノード$Z$についてもその子供たちの任意の選び方$y_1, \dots, y_i$について子供がぴったり$y_1, \dots, y_i$なノードがあるか探せば分出公理が成り立っているか確かめられます。
置換公理は、これもパラメータが使えるので、任意のマッピングが定義可能になっています。 よって、すべてのノード$x$にわたる$x$の子供の数の最大値$n$をとり、ノードの$n$個の任意の集まりについて、それらをすべて子供にするノードの存在を確かめればよいのです。
以上より分出公理も置換公理も有限時間で判定できます。
なお、この方法は数学基礎論若手の会2019にてyさんとkさんの助言により得られることができました。
ソースコード
type variable = string type formula = Equal of variable * variable | Epsilon of variable * variable | Imply of formula * formula | Not of formula | And of formula * formula | Or of formula * formula | Forall of variable * formula | Exists of variable * formula type model = int * ((bool list) list) type assignment = (variable, int) Hashtbl.t let subst asgn var value = (let asgn' = Hashtbl.copy asgn in Hashtbl.add asgn' var value; asgn');; let rec forall n fn = if n = 0 then true else (fn (n-1)) && (forall (n-1) fn);; let rec exists n fn = if n = 0 then false else (fn (n-1)) || (exists (n-1) fn);; (* モデルmdlが論理式fmlを割り当てasgnで満たすかどうか *) let rec satisfies mdl fml asgn = let (numelems, graph) = mdl in match fml with Equal (var1, var2) -> (Hashtbl.find asgn var1) = (Hashtbl.find asgn var2) | Epsilon (var1, var2) -> let a = (Hashtbl.find asgn var1) in let b = (Hashtbl.find asgn var2) in List.nth (List.nth graph b) a | Imply (fml1, fml2) -> (not (satisfies mdl fml1 asgn)) || (satisfies mdl fml2 asgn) | Not fml -> not (satisfies mdl fml asgn) | And (fml1, fml2) -> (satisfies mdl fml1 asgn) && (satisfies mdl fml2 asgn) | Or (fml1, fml2) -> (satisfies mdl fml1 asgn) || (satisfies mdl fml2 asgn) | Forall (var, fml) -> forall numelems (fun x -> satisfies mdl fml (subst asgn var x)) | Exists (var, fml) -> exists numelems (fun x -> satisfies mdl fml (subst asgn var x));; (* リスト [0; 1; 2; …; n - 1]を返す *) let range n = List.init n (fun x -> x);; (* range nとrange mの直積を返す *) let range2 n m = List.init (n*m) (fun x -> (x / m, x mod m));; (* モデルmdlの元xに対してy∈xとなっているy全体のリストを返す *) let children mdl x = let (numelems, graph) = mdl in List.filter (fun y -> List.nth (List.nth graph x) y) (range numelems);; (* リストlistのすべての部分リストのリストを返す *) let rec all_subsets list = match list with [] -> [[]] | x :: tail -> all_subsets tail @ List.map (fun y -> x :: y) (all_subsets tail);; (* リストlistの部分リストで大きさkのもの全体のリストを返す *) let rec all_combinations list n = match list with [] -> (if n = 0 then [[]] else []) | x :: tail -> (all_combinations tail n) @ List.map (fun y -> x :: y) (all_combinations tail (n - 1));; (* 昇順に並んだ二つのリストx, yについてxがyの部分リストか判定する *) let rec is_sublist x y = match x with [] -> true | a :: tail -> (match y with [] -> false | b :: tail' -> (if (a = b) then (is_sublist tail tail') else (if (b < a) then (is_sublist (a::tail) tail') else false)));; (* 分出公理をすべて満たすか *) let sat_all_comprehension mdl = let (numelems, graph) = mdl in forall numelems (fun x -> List.for_all (fun subset -> exists numelems (fun y -> children mdl y = subset) ) (all_subsets (children mdl x)));; (* 置換公理をすべて満たすか *) let sat_all_replacement mdl = let (numelems, graph) = mdl in let maxchildren = List.fold_left max 0 (List.map (fun x -> List.length (children mdl x)) (range numelems)) in let combinations = all_combinations (range numelems) maxchildren in List.for_all (fun subset -> exists numelems (fun y -> is_sublist subset (children mdl y)) ) combinations;; let model_to_pairs mdl = let (numelems, graph) = mdl in List.filter (fun (x, y) -> List.nth (List.nth graph y) x) (range2 numelems numelems);; let model_to_string mdl = "{" ^ (String.concat ", " (List.map (fun (x, y) -> "(" ^ (string_of_int x) ^ ", " ^ (string_of_int y) ^ ")") (model_to_pairs mdl))) ^ "}";; let iff fml1 fml2 = And (Imply (fml1, fml2), Imply (fml2, fml1));; let bforall x y fml = Forall (x, Imply (Epsilon (x, y), fml));; let bexists x y fml = Exists (x, And (Epsilon (x, y), fml));; (* x=∅ (using z as a bounded variable) *) let emptyset x z = Forall (z, Not (Epsilon (z, x)));; (* ∅∈x (using y, z as bounded variables) *) let containsempty x y z = Exists (y, And (Epsilon (y, x), emptyset y z));; (* x⊆y (using z as a bounded variable) *) let contains x y z = bforall z x (Epsilon (z, y));; (* y=x∪{x} using z as a bounded variable *) let successor x y z = Forall (z, (iff (Epsilon (z, y)) (Or (Epsilon (z, x), (Equal (z, x))))));; (* w=x∩y using z as a bounded variable *) let intersection x y w z = Forall (z, iff (Epsilon (z, w)) (And (Epsilon (z, x), Epsilon (z, y))));; (* x∩y=∅ *) let disjoint x y z = bforall z x (Not (Epsilon (z, y)));; (* xが一点集合 using y, z as bounded variables *) let singleton x y z = bexists y x (bforall z x (Equal (z, y)));; (* 外延性公理 *) let extensionality = Forall ("x", Forall ("y", Imply (Forall ("z", iff (Epsilon ("z", "x")) (Epsilon ("z", "y"))), Equal ("x", "y"))));; (* 基礎の公理 *) let foundation = Forall ("x", Imply (Exists ("y", Epsilon ("y", "x")), Exists ("y", And (Epsilon ("y", "x"), Not (Exists ("z", And (Epsilon ("z", "x"), Epsilon ("z", "y"))))))));; (* 対の公理 *) let pairing = Forall ("x", Forall ("y", Exists ("z", (And (Epsilon ("x", "z"), Epsilon ("y", "z"))))));; (* 和集合公理 *) let union = Forall ("F", Exists ("A", Forall ("Y", Forall ("x", Imply (And (Epsilon ("x", "Y"), Epsilon ("Y", "F")), Epsilon ("x", "A"))))));; (* 無限公理 *) let infinity = Exists ("x", (And (containsempty "x" "y" "z", bforall "y" "x" (bexists "z" "x" (successor "z" "y" "w")))));; (* べき集合公理 *) let powerset = Forall ("x", Exists ("y", Forall ("z", Imply (contains "z" "x" "w", Epsilon ("z", "y")))));; (* 選択公理 *) let choice = Forall ("F", Imply ( And (Not (containsempty "F" "y" "z"), bforall "x" "F" (bforall "y" "F" (Or (Equal ("x", "y"), disjoint "x" "y" "z")))), Exists ("c", bforall "x" "F" (Exists ("d", And (intersection "c" "x" "d" "y", singleton "d" "y" "z"))))));; let models = [ (1, [[false]]); (1, [[true]]); (2, [[false; true]; [true; false]]); (3, [[false; true; false]; [true; false; false]; [true; true; false]]); (3, [[false; false; false]; [true; false; false]; [true; false; false]]); (4, [[false; false; false; false]; [true; false; false; false]; [true; true; false; false]; [true; true; true; false]]); (3, [[false; false; false]; [true; false; false]; [false; true; false]]); (5, [[false; true; false; false; false]; [true; false; false; false; false]; [true; false; false; false; false]; [false; true; false; false; false]; [false; false; true; true; false]]) ];; List.iter (fun mdl -> let (numelems, graph) = mdl in let asgn = Hashtbl.create 0 in print_endline ("In the model=(" ^ string_of_int numelems ^ ", " ^ (model_to_string mdl) ^ ")"); print_endline (String.concat " " (List.map (fun x -> (if x then "1" else "0")) [ satisfies mdl extensionality asgn; satisfies mdl foundation asgn; sat_all_comprehension mdl; satisfies mdl pairing asgn; satisfies mdl union asgn; sat_all_replacement mdl; satisfies mdl infinity asgn; satisfies mdl powerset asgn; satisfies mdl choice asgn; ])); ) models;;
