Index src

strict provable sort wff;

pure sort set;

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 $;
infixr or: $\or$ prec 30;

def and (A B: wff): wff = $ \neg (A \imp \neg B) $;
infixr 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: $\eq$ prec 60;

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

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

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

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

def nni (x y: set): wff = $ \neg x \cont y $;
infixr nni: $\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 \eq 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 t: wff = $ \fo x x \eq x \imp \fo x x \eq x $;
prefix t: $\t$ prec 50;

def f: wff = $ \neg \t $;
prefix f: $\f$ prec 50;

def rep (y: set) {x: set} (P: wff x): wff = $ \fo t (t \eq y \imp \fo x (x \eq 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 \eq x $;

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

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

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

axiom ax_ext {x y z: set}: $ \fo x \fo y (x \eq 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 \eq x \or z \eq 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 \eq 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 ili (A B: wff): $ A \imp B \imp A $;

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

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

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

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

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

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