Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Elimination of constants and function symbols from set theory

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 ;;
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.