Index src

strict provable sort wff;

pure sort set;

strict sort class;

term neg (A: wff): wff;
prefix neg: $\neg$ prec 50;

term imp (A B: wff): wff;
infixr imp: $\imp$ prec 20;

def or (A B: wff): wff = $ \neg A \imp B $;
infixl or: $\or$ prec 30;

def and (A B: wff): wff = $ \neg (A \imp \neg B) $;
infixl and: $\and$ prec 30;

def iff (A B: wff): wff = $ (A \imp B) \and (B \imp A) $;
infixr iff: $\iff$ prec 10;

term eq (x y: set): wff;
infixr eq: $=$ prec 60;

term in (x y: set): wff;
infixr in: $\in$ prec 60;

def cont (x y: set): wff = $ y \in x $;
infixr cont: $\cont$ prec 60;

def neq (x y: set): wff = $ \neg x = y $;
infixr neq: $\neq$ prec 60;

def nin (x y: set): wff = $ \neg x \in y $;
infixr nin: $\nin$ prec 60;

def ncont (x y: set): wff = $ \neg x \cont y $;
infixr ncont: $\ncont$ prec 60;

term fo {x: set} (P: wff x): wff;
prefix fo: $\fo$ prec 50;

def ex {x: set} (P: wff x): wff = $ \neg \fo x \neg P $;
prefix ex: $\ex$ prec 50;

def nex {x: set} (P: wff x): wff = $ \neg \ex x P $;
prefix nex: $\nex$ prec 50;

def exu {x: set} (P: wff x): wff = $ \ex y \fo x (x = y \iff P) $;
prefix exu: $\exu$ prec 50;

def foin {x: set} (y: set) (P: wff x): wff = $ \fo x (x \in y \imp P) $;
notation foin {x: set} (y: set) (P: wff x): wff = ($\foin{$:50) x ($}{$:0) y ($}$:0) P;

def exin {x: set} (y: set) (P: wff x): wff = $ \ex x (x \in y \and P) $;
notation exin {x: set} (y: set) (P: wff x): wff = ($\exin{$:50) x ($}{$:0) y ($}$:0) P;

def nexin {x: set} (y: set) (P: wff x): wff = $ \neg \exin{x}{y} P $;
notation nexin {x: set} (y: set) (P: wff x): wff = ($\nexin{$:50) x ($}{$:0) y ($}$:0) P;

def exuin {x: set} (y: set) (P: wff x): wff = $ \exu x (x \in y \and P) $;
notation exuin {x: set} (y: set) (P: wff x): wff = ($\exuin{$:50) x ($}{$:0) y ($}$:0) P;

def true: wff = $ \fo x x = x \imp \fo x x = x $;
prefix true: $\true$ prec 50;

def false: wff = $ \neg \true $;
prefix false: $\false$ prec 50;

def rep (y: set) {x: set} (P: wff x): wff = $ \fo t (t = y \imp \fo x (x = t \imp P)) $;
notation rep (y: set) {x: set} (P: wff x): wff = ($\rep{$:50) y ($}{$:0) x ($}$:0) P;

axiom ax_mp (A B: wff): $ A \imp B $ > $ A $ > $ B $;

axiom ax_p1 (A B: wff): $ A \imp B \imp A $;

axiom ax_p2 (A B C: wff): $ (A \imp B \imp C) \imp (A \imp B) \imp A \imp C $;

axiom ax_p3 (A B: wff): $ (\neg A \imp \neg B) \imp B \imp A $;

axiom ax_f1 (A: wff) {x: set} (y: set): $ \fo x A \imp \rep{y}{x} A $;

axiom ax_f2 (A B: wff) {x: set}: $ \fo x (A \imp B) \imp \fo x A \imp \fo x B $;

axiom ax_f3 (A: wff) {x: set}: $ A \imp \fo x A $;

axiom ax_e1 {x: set}: $ \fo x x = x $;

axiom ax_e2 {x y: set}: $ \fo x \fo y (x = y \imp y = x) $;

axiom ax_e3 {x y z: set}: $ \fo x \fo y \fo z (x = y \and y = z \imp x = z) $;

axiom ax_e4 {x y: set} (P: wff x y): $ \fo x \fo y (x = y \imp (P \iff \rep{y}{x} P)) $;

axiom ax_ext {x y z: set}: $ \fo x \fo y (x = y \iff \fo z (z \in x \iff z \in y)) $;

axiom ax_emp {x y: set}: $ \ex x \fo y y \nin x $;

axiom ax_pow {w x y z: set}: $ \fo x \ex y \fo z (z \in y \iff \fo w (w \in z \imp w \in x)) $;

axiom ax_sub {x y z: set} (P: wff z): $ \fo x \ex y \fo z (z \in y \iff z \in x \and P) $;

axiom ax_pai {u x y z: set}: $ \fo x \fo y \ex u \fo z (z \in u \iff z = x \or z = y) $;

axiom ax_uni {u x y z: set}: $ \fo x \ex y \fo z (z \in y \iff \ex u (u \in x \and z \in u)) $;

axiom ax_inf {w x y z: set}: $ \fo x \ex y (x \in y \and \fo z (z \in y \imp \ex w (z \in w \and w \in y))) $;

axiom ax_rep {u v x y: set} (P: wff x y): $ \fo u (\fo x \ex y \fo v (P \imp y = v) \imp \ex v \fo y (y \in v \iff \exin{x}{u} P)) $;

axiom ax_reg {x y z: set}: $ \fo x (\ex y y \in x \imp \ex y (y \in x \and \fo z (z \in y \imp \neg z \in x))) $;

axiom ax_cho {u w x y z: set}: $ \fo x \ex y \fo z (z \in x \and \ex u u \in z \imp \exu u (u \in z \and \exin{w}{y} (z \in w \and u \in w))) $;

theorem mp (A B: wff): $ A \imp B $ > $ A $ > $ B $;

theorem imp_left_intro (A B: wff): $ A \imp B \imp A $;

theorem imp_for_imp_left_insert (A B C: wff): $ (A \imp B \imp C) \imp (A \imp B) \imp A \imp C $;

theorem imp_reflect (A: wff): $ A \imp A $;

theorem imp_for_imp_left_intro (A B C: wff): $ (B \imp C) \imp (A \imp B) \imp A \imp C $;

theorem imp_for_imp_left_permute (A B C: wff): $ (A \imp B \imp C) \imp B \imp A \imp C $;

theorem imp_for_imp_right_reverse_intro (A B C: wff): $ (A \imp B) \imp (B \imp C) \imp A \imp C $;

theorem imp_trans_curried (A B C: wff): $ (A \imp B) \imp (B \imp C) \imp A \imp C $;

theorem imp_for_imp_right_left_intro (A B C: wff): $ (A \imp B) \imp A \imp C \imp B $;

theorem mp_curried (A B: wff): $ (A \imp B) \imp A \imp B $;

theorem mp_imp_left_intro (A B C D: wff): $ (A \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C $;

theorem imp_for_imp_left_extract (A B C: wff): $ ((A \imp B) \imp A \imp C) \imp A \imp B \imp C $;

theorem imp_for_imp_right_insert (A B C: wff): $ ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C $;

theorem neg_in_imp_reverse_elim (A B: wff): $ (\neg A \imp \neg B) \imp B \imp A $;

theorem neg_elim_with_imp (A B: wff): $ \neg A \imp A \imp B $;

theorem neg_intro_with_imp (A B: wff): $ A \imp \neg A \imp B $;

theorem neg_neg_elim (A: wff): $ \neg \neg A \imp A $;

theorem neg_neg_intro (A: wff): $ A \imp \neg \neg A $;

theorem imp_left_neg_permute (A B: wff): $ (\neg A \imp B) \imp \neg B \imp A $;

theorem imp_right_neg_permute (A B: wff): $ (A \imp \neg B) \imp B \imp \neg A $;

theorem neg_in_imp_reverse_intro (A B: wff): $ (A \imp B) \imp \neg B \imp \neg A $;

theorem imp_left_neg_imp_same (A: wff): $ (\neg A \imp A) \imp A $;

theorem imp_right_neg_imp_neg_same (A: wff): $ (A \imp \neg A) \imp \neg A $;

theorem imp_left_merge_neg_imp (A B C: wff): $ (A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C $;

theorem imp_left_have_neg_merge (A B C: wff): $ (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp C $;

theorem contradiction (A: wff): $ \neg (A \and \neg A) $;

theorem and_compound (A B: wff): $ A \imp B \imp A \and B $;

theorem and_left_split (A B: wff): $ A \and B \imp A $;

theorem and_right_split (A B: wff): $ A \and B \imp B $;