Zermelo Frankel

This case study is an encoding of Zermelo Frankel (ZFC) set theory.

%% ZFC
%% by Daniel C. Wang
%% Transliterated from AUTOMATH definition
%% http://www.cs.ru.nl/~freek/zfc-etc/zfc.aut
%sort prop %.
%sort pf {_ prop} %.
%sort set %.
%% First Order Logic
%term false prop %.
%term imp %pi prop %-> prop %-> prop %.
%term all %pi (%pi set %-> prop) %-> prop %.
%term eq %pi set %-> set %-> prop %.
%term in %pi set %-> set %-> prop %.
%define not (%pi prop %-> prop) [a] imp a false %.
%define and (%pi prop %-> prop %-> prop) [a] [b] not (imp a (not b)) %.
%define or (%pi prop %-> prop %-> prop) [a] [b] imp (not a) b %.
%define iff (%pi prop %-> prop %-> prop) [a] [b] and (imp a b) (imp b a) %.
%define ex (%pi (%pi set %-> prop) %-> prop) [p] not (all ([z] not (p z))) %.
%define unique (%pi (%pi set %-> prop) %-> prop) [p] all ([z] imp (p z) (all ([z'] imp (p z') (eq z z')))) %.
%define ex_unique (%pi (%pi set %-> prop) %-> prop) [p] and (ex p) (unique p) %.
%term imp_i %pi (%pi (pf A) %-> (pf B)) %-> (pf (imp A B)) %.
%term imp_e %pi (pf (imp A B)) %-> (pf A) %-> (pf B) %.
%term all_i %pi ({z} pf (P z)) %-> (pf (all P)) %.
%term all_e %pi (pf (all P)) %-> ({z} pf (P z)) %.
%term classical %pi (pf (not (not A))) %-> (pf A) %.
%term eq_i pf (eq A A) %.
%term eq_e %pi (pf (eq A B)) %-> ({s %pi set %-> prop} %pi (pf (s A)) %-> (pf (s B))) %.
%term if %pi prop %-> set %-> set %-> set %.
%term if_then %pi (pf P) %-> (pf (eq (if P X Y) X)) %.
%term if_else %pi (pf (not P)) %-> (pf (eq (if P X Y) Y)) %.
%% Set Theory theory
%term empty set %.
%term double %pi set %-> set %-> set %.
% {x,y}
%term unions %pi set %-> set %.
% union sets in sets
%term powerset %pi set %-> set %.
%term replace %pi set %-> (%pi set %-> set) %-> set %.
%term omega set %.
%define single (%pi set %-> set) [x] double x x %.
%define restrict (%pi set %-> (%pi set %-> prop) %-> set) [x] [q] unions (replace x ([z] if (q z) (single z) empty)) %.
%define inter (%pi set %-> set %-> set) [x] [y] restrict x ([z] in z y) %.
%define union (%pi set %-> set %-> set) [x] [y] unions (double x y) %.
%define zero set empty %.
%define succ (%pi set %-> set) [x] union x (single x) %.
%define subset (%pi set %-> set %-> prop) [x] [y] all ([z] imp (in z x) (in z y)) %.
%define disjoint (%pi set %-> set %-> prop) [x] [y] eq (inter x y) empty %.
%define omega_closed (%pi set %-> prop) [x] and (in empty x) (all ([n] imp (in n x) (in (succ n) x))) %.
%% Axioms ZF
%term extensionality pf (iff (eq X Y) (all ([z] iff (in z X) (in z Y)))) %.
%term foundation pf (ex ([z] and (in z X) (disjoint z X))) %.
%term emtpy_ax pf (not (in X empty)) %.
%term double_ax pf (iff (in Z (double X Y)) (or (in Z X) (in Z Y))) %.
%term union_ax pf (iff (in Z (unions X)) (ex ([y] and (in Z y) (in y X)))) %.
%term powerset_ax pf (iff (in Z (powerset X)) (subset Z X)) %.
%term replace_ax pf (iff (in Z (replace X F)) (ex ([y] and (in y X) (eq Z (F y))))) %.
%term omega_ax pf (and (omega_closed omega) (all ([o] imp (omega_closed o) (subset omega o)))) %.
%% C
%term choice_ax pf (imp (all ([y1] imp (in y1 X) (all ([y2] imp (in y2 X) (disjoint y1 y2))))) (ex ([x'] all ([y] imp (in y X) (ex_unique ([y'] and (in y' x') (in y' y))))))) %.

Category:STELF code