Official Zermelo-Fraenkel set theory only has the elementhood relation symbol ∈, and nothing else. Other constants, such as ∅, ⊆, ∩, ∪, f[x], etc. can be mechanically eliminated. The result of the elimination is a formula which is logically equivalent to the original, but is more complicated.
This program eliminates constants and function symbols, and generates LaTeX showing the formula before and after the elimination.
| (* Elimination of constant and function symbols from first-order logic and set theory. *) | |
| (* A variable name. *) | |
| type name = string * int | |
| (* A term, possibly with defined symbols *) | |
| type 'a term = | |
| | Var of 'a | |
| | EmptySet | |
| | BigUnion of 'a term | |
| | Couple of 'a term * 'a term (* unordered pair *) | |
| | Singleton of 'a term | |
| | Apply of 'a term * 'a term | |
| | Intersection of 'a term * 'a term | |
| | Union of 'a term * 'a term | |
| | Succ of 'a term | |
| (* Logical formulas. *) | |
| type 'a prop = | |
| | True | |
| | False | |
| | And of 'a prop * 'a prop | |
| | Or of 'a prop * 'a prop | |
| | Imply of 'a prop * 'a prop | |
| | Iff of 'a prop * 'a prop | |
| | Not of 'a prop | |
| | Exists of ('a -> 'a prop) | |
| | Forall of ('a -> 'a prop) | |
| | Elem of 'a term * 'a term | |
| | Equal of 'a term * 'a term | |
| (* Bounded quantifiers *) | |
| let forall_in t p = Forall (fun x -> Imply (Elem (Var x, t), p x)) | |
| let exists_in t p = Exists (fun x -> And (Elem (Var x, t), p x)) | |
| (* Various abbreviations *) | |
| let pair x y = Couple (Singleton x, Couple (x, y)) | |
| let subset u t = forall_in u (fun x -> Elem (Var x, t)) | |
| let inhabited u = Exists (fun x -> Elem (Var x, u)) | |
| let empty u = Forall (fun x -> Not (Elem (Var x, u))) | |
| (* Convenience functions which optimize formulas a bit *) | |
| let mk_and p q = | |
| match p, q with | |
| | True, q -> q | |
| | p, True -> p | |
| | False, _ -> False | |
| | _, False -> False | |
| | p, q -> And (p, q) | |
| let mk_or p q = | |
| match p, q with | |
| | True, _ -> True | |
| | _, True -> True | |
| | False, q -> q | |
| | p, False -> p | |
| | p, q -> Or (p, q) | |
| let mk_imply p q = | |
| match p, q with | |
| | True, p -> p | |
| | _, True -> True | |
| | False, _ -> True | |
| | p, False -> Not p | |
| | p, q -> Imply (p, q) | |
| let mk_iff p q = | |
| match p, q with | |
| | True, q -> q | |
| | p, True -> p | |
| | False, q -> Not q | |
| | p, False -> Not p | |
| | p, q -> Iff (p, q) | |
| let mk_not p = | |
| match p with | |
| | True -> False | |
| | False -> True | |
| | Not q -> q | |
| | q -> Not q | |
| (* Eliminate all defined symbols from a formula. *) | |
| let rec elim = function | |
| | True -> True | |
| | False -> False | |
| | And (p, q) -> mk_and (elim p) (elim q) | |
| | Or (p, q) -> mk_or (elim p) (elim q) | |
| | Imply (p, q) -> mk_imply (elim p) (elim q) | |
| | Iff (p, q) -> mk_iff (elim p) (elim q) | |
| | Not p -> mk_not (elim p) | |
| | Exists p -> Exists (fun x -> elim (p x)) | |
| | Forall p -> Forall (fun x -> elim (p x)) | |
| | Elem (s, t) -> | |
| elimTerm s (fun s -> elimTerm t (fun t -> Elem (s, t))) | |
| | Equal (s, t) -> | |
| elimTerm s (fun s -> elimTerm t (fun t -> Equal (s, t))) | |
| (* Eliminate all defined symbols from a term *) | |
| and elimTerm t = | |
| match t with | |
| | Var x -> (fun k -> k (Var x)) | |
| | EmptySet -> nullary (fun z -> False) | |
| | BigUnion t -> | |
| unary t | |
| (fun x t -> | |
| Exists (fun y -> mk_and (Elem (Var x, Var y)) (Elem (Var y, t)))) | |
| | Singleton t -> | |
| unary t | |
| (fun x t -> Equal (Var x, t)) | |
| | Couple (t1, t2) -> | |
| binary t1 t2 | |
| (fun x t1 t2 -> mk_or (Equal (Var x, t1)) (Equal (Var x, t2))) | |
| | Apply (f, x) -> | |
| binary f x | |
| (fun z f x -> | |
| Exists (fun y -> | |
| mk_and (Elem (pair x (Var y), f)) | |
| (mk_and (Elem (Var z, Var y)) | |
| (Forall (fun y' -> | |
| mk_imply | |
| (Elem (pair x (Var y'), f)) | |
| (Equal (Var y, Var y'))))))) | |
| | Intersection (t1, t2) -> | |
| binary t1 t2 | |
| (fun x t1 t2 -> mk_and (Elem (Var x, t1)) (Elem (Var x, t2))) | |
| | Union (t1, t2) -> | |
| binary t1 t2 | |
| (fun x t1 t2 -> mk_or (Elem (Var x, t1)) (Elem (Var x, t2))) | |
| | Succ t -> | |
| unary t | |
| (fun x t -> mk_or (Elem (Var x, t)) (Equal (Var x, t))) | |
| and nullary p k = | |
| elim | |
| (Exists (fun x -> mk_and (Forall (fun y -> mk_iff (Elem (Var y, Var x)) (p x))) (k (Var x)))) | |
| and unary t p k = | |
| elimTerm t (fun t -> | |
| elim | |
| (Exists (fun x -> | |
| mk_and (Forall (fun y -> mk_iff (Elem (Var y, Var x)) (p y t))) (k (Var x))))) | |
| and binary t1 t2 p k = | |
| elimTerm t1 (fun t1 -> | |
| elimTerm t2 (fun t2 -> | |
| elim | |
| (Exists (fun x -> | |
| mk_and (Forall (fun y -> mk_iff (Elem (Var y, Var x)) (p y t1 t2))) (k (Var x)))))) | |
| (** Production of LaTeX expressions *) | |
| (* Generate a fresh name, avoid forbidden ones *) | |
| let rec fresh forbidden = | |
| let names = [|"x"; "y"; "z"; "a"; "b"; "c"; "r"; "s"; "t"; "u"; "v"; "w" ; | |
| "p"; "q"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n" |] in | |
| let mk_name k = names.(k mod (Array.length names)), k / (Array.length names) in | |
| let rec search k = | |
| let x = mk_name k in | |
| if List.mem x forbidden | |
| then search (k+1) | |
| else x | |
| in | |
| search 0 | |
| let rec latexTerm t ppt = | |
| match t with | |
| | Var (x, 0) -> Format.fprintf ppt "%s" x | |
| | Var (x, k) -> Format.fprintf ppt "%s_{%d}" x k | |
| | EmptySet -> Format.fprintf ppt "\\emptyset" | |
| | BigUnion t -> Format.fprintf ppt "\\bigcup (%t)" (latexTerm t) | |
| | Couple (t1, t2) -> Format.fprintf ppt "\\{%t, %t\\}" (latexTerm t1) (latexTerm t2) | |
| | Singleton t -> Format.fprintf ppt "\\{%t\\}" (latexTerm t) | |
| | Apply (t1, t2) -> Format.fprintf ppt "%t [%t]" (latexTerm t1) (latexTerm t2) | |
| | Intersection (t1, t2) -> Format.fprintf ppt "(%t) \\cap (%t)" (latexTerm t1) (latexTerm t2) | |
| | Union (t1, t2) -> Format.fprintf ppt "(%t) \\cup (%t)" (latexTerm t1) (latexTerm t2) | |
| | Succ t -> Format.fprintf ppt "(%t)^{+}" (latexTerm t) | |
| let rec latex ?(max_level=9999) xs p ppt = | |
| let at_level, fmt = | |
| match p with | |
| | True -> 0, fun ppt -> Format.fprintf ppt "\\top" | |
| | False -> 0, fun ppt -> Format.fprintf ppt "\\bot" | |
| | Elem (s, t) -> | |
| 40, fun ppt -> Format.fprintf ppt "%t@ \\in@ %t" | |
| (latexTerm s) | |
| (latexTerm t) | |
| | Not (Elem (s, t)) -> | |
| 40, fun ppt -> Format.fprintf ppt "%t@ \\not\\in@ %t" | |
| (latexTerm s) | |
| (latexTerm t) | |
| | Equal (s, t) -> | |
| 40, fun ppt -> Format.fprintf ppt "%t@ =@ %t" | |
| (latexTerm s) | |
| (latexTerm t) | |
| | Not (Equal (s, t)) -> | |
| 40, fun ppt -> Format.fprintf ppt "%t@ \\neq@ %t" | |
| (latexTerm s) | |
| (latexTerm t) | |
| | Not p -> | |
| 30, fun ppt -> Format.fprintf ppt "\\lnot@ %t" | |
| (latex ~max_level:29 xs p) | |
| | And (p, q) -> | |
| 50, fun ppt -> Format.fprintf ppt "%t@ \\land@ %t" | |
| (latex ~max_level:50 xs p) | |
| (latex ~max_level:50 xs q) | |
| | Or (p, q) -> | |
| 60, fun ppt -> Format.fprintf ppt "%t \\lor %t" | |
| (latex ~max_level:60 xs p) | |
| (latex ~max_level:60 xs q) | |
| | Imply (p, q) -> | |
| 70, fun ppt -> Format.fprintf ppt "%t@ \\Rightarrow@ %t" | |
| (latex ~max_level:69 xs p) | |
| (latex ~max_level:70 xs q) | |
| | Iff (p, q) -> | |
| 70, fun ppt -> Format.fprintf ppt "%t@ \\Leftrightarrow@ %t" | |
| (latex ~max_level:69 xs p) | |
| (latex ~max_level:69 xs q) | |
| | Exists p -> | |
| let x = fresh xs in | |
| let xs = x :: xs in | |
| 80, fun ppt -> Format.fprintf ppt "\\exists %t \\,.\\,@ %t" | |
| (latexTerm (Var x)) | |
| (latex ~max_level:80 xs (p x)) | |
| | Forall p -> | |
| let x = fresh xs in | |
| let xs = x :: xs in | |
| 80, fun ppt -> Format.fprintf ppt "\\forall %t \\,.\\,@ %t" | |
| (latexTerm (Var x)) | |
| (latex ~max_level:80 xs (p x)) | |
| in | |
| if at_level > max_level | |
| then Format.fprintf ppt "(%t)" fmt | |
| else fmt ppt | |
| (* Print a formula p before and after elimination. *) | |
| let eliminate t p = | |
| Format.printf "%s:@\n@\n" t ; | |
| Format.printf "* before elimination: $%t$@\n" (latex [] p) ; | |
| Format.printf "* after elimination: $%t$@\n@." (latex [] (elim p)) | |
| (* Examples. *) | |
| (* {z, z} = {z} *) | |
| let couple_singleton = | |
| Forall (fun z -> Equal (Couple (Var z, Var z), Singleton (Var z))) ;; | |
| eliminate | |
| "The couple $\\{z,z\\}$ equals the singleton $\\{z\\}$" | |
| couple_singleton ;; | |
| (* {x, y} = {y, x} *) | |
| let couple_commutes = | |
| Forall (fun x -> | |
| Forall (fun y -> | |
| Equal (Couple (Var x, Var y), Couple (Var y, Var x)))) ;; | |
| eliminate | |
| "Couple commutes" | |
| couple_commutes ;; | |
| (* the union of {x, x} is x *) | |
| let union_couple = | |
| Forall (fun x -> Equal (BigUnion (Couple (Var x, Var x)), Var x)) ;; | |
| eliminate | |
| "The union of $\\{x,x\\}$" | |
| union_couple ;; | |
| (* Function application: empty set applied to anything is empty set *) | |
| let apply_emptyset = | |
| Forall (fun x -> Equal (Apply (EmptySet, Var x), EmptySet)) ;; | |
| eliminate | |
| "Application of the empty set" | |
| apply_emptyset ;; | |
| (* Axiom of choice *) | |
| let ac = | |
| Forall (fun x -> | |
| mk_imply | |
| (forall_in (Var x) (fun y -> inhabited (Var y))) | |
| (Exists (fun f -> | |
| forall_in (Var x) (fun y -> Elem (Apply (Var f, Var y), Var y))))) ;; | |
| eliminate | |
| "The axiom of choice" | |
| ac ;; | |
| (* Axiom of regularity *) | |
| let reg = | |
| Forall (fun x -> | |
| mk_imply (inhabited (Var x)) | |
| (exists_in (Var x) (fun y -> empty (Intersection (Var x, Var y))))) ;; | |
| eliminate | |
| "The axiom of regularity" | |
| reg ;; | |
| (* Axiom of infinity *) | |
| let inf = | |
| Exists (fun w -> | |
| mk_and (Elem (EmptySet, Var w)) | |
| (forall_in (Var w) (fun x -> Elem (Succ (Var x), Var w)))) ;; | |
| eliminate | |
| "The axiom of infinity" | |
| inf ;; | |