var ph ps ch: wff*;
term wi (ph ps: wff): wff; infixr wi: -> 25;
term wn (ph: wff): wff; prefix wn: ~ 40;
axiom ax-1: << ph -> ps -> ph >>
(wi ph (wi ps ph));
axiom ax-2: << (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch >>
(wi (wi ph (wi ps ch)) (wi (wi ph ps) (wi ph ch)));
axiom ax-3: << (~ph -> ~ps) -> ps -> ph >>
(wi (wi (wn ph) (wn ps)) (wi ps ph));
axiom ax-mp:
<< ph >> ph ->
<< ph -> ps >> (wi ph ps) ->
<< ps >> ps;
theorem a1i: << ph >> ph -> << ps -> ph >> (wi ps ph);
def wb (ph ps: wff): wff :=
<< ~((ph -> ps) -> ~(ps -> ph)) >>
(wn (wi (wi ph ps) (wn (wi ps ph)))) {
infix wb: <-> 20;
theorem bi1: << (ph <-> ps) -> ph -> ps >>
(wi (wb ph ps) (wi ph ps));
theorem bi2: << (ph <-> ps) -> ps -> ph >>
(wi (wb ph ps) (wi ps ph));
theorem bi3: << (ph -> ps) -> (ps -> ph) -> (ph <-> ps) >>
(wi (wi ph ps) (wi (wi ps ph) (wb ph ps)));
}
def wa (ph ps: wff): wff := << ~(ph -> ~ps) >> (wn (wi ph (wn ps))) {
infix wa: /\ 20;
theorem df-an: << (ph /\ ps) <-> ~(ph -> ~ps) >>
(wi (wa ph ps) (wn (wi ph (wn ps))));
}
def wtru (bound p: wff): wff := << p <-> p >> (wb p p) {
notation wtru := << T. >>;
theorem df-tru: << T. <-> (ph <-> ph) >> (wb wtru (wb ph ph));
}
pure nonempty sort set;
bound x y z w: set;
term wal (x: set) (ph: wff x): wff; prefix wal: A. 30;
def wex (x: set) (ph: wff x): wff :=
<< ~A. x ~ph >> (wn (wal x (wn ph))) {
prefix wex: E. 30;
theorem df-ex: << E. x ph <-> ~A. x ~ph >>
(wb (wex x ph) (wn (wal x (wn ph))));
}
axiom ax-gen: << ph >> ph -> << A. x ph >> (wal x ph);
axiom ax-4: << A. x (ph -> ps) -> A. x ph -> A. x ps >>
(wi (wal x (wi ph ps)) (wi (wal x ph) (wal x ps)));
axiom ax-5 (ph: wff): << ph -> A. x ph >> (wi ph (wal x ph));
var a b c: set;
term weq (a b: set): wff;
term wel (a b: set): wff;
{
local infix weq: = 50;
local infix wel: e. 40;
def weu (x: set) (ph: wff x): wff :=
<< E. y A. x (ph <-> x = y) >>
(wex y (wal x (wb ph (weq x y)))) {
prefix wex: E! 30;
theorem df-ex: << E! x ph <-> E. y A. x (ph <-> x = y) >>
(wb (weu x ph) (wex y (wal x (wb ph (weq x y)))));
}
axiom ax-6: << E. x x = a >> (wex x (weq x a));
axiom ax-7: << a = b -> a = c -> b = c >>
(wi (weq a b) (wi (weq a c) (weq b c)));
axiom ax-8: << a = b -> a e. c -> b e. c >>
(wi (weq a b) (wi (wel a c) (wel b c)));
axiom ax-9: << a = b -> c e. a -> c e. b >>
(wi (weq a b) (wi (wel c a) (wel c b)));
axiom ax-10: << ~A. x ph -> A. x ~ A. x ph >>
(wi (wal x ph) (wal x (wn (wal x ph))));
axiom ax-11: << A. x A. y ph -> A. y A. x ph >>
(wi (wal x (wal y ph)) (wal y (wal x ph)));
axiom ax-12 (ph: wff y): << A. y ph -> A. x (x = y -> ph) >>
(wi (weq x y) (wi (wal y ph) (wal x (wi (weq x y) ph))));
axiom ax-ext: << A. x (x e. a <-> x e. b) -> a = b >>
(wi (wal x (wb (wel x a) (wel x b))) (weq a b));
axiom ax-rep (ph: wff y z):
<< A. y E. x A. z (ph -> z = x) ->
E. x A. z (z e. x <-> E. y (y e. a /\ ph)) >>
(wi (wal y (wex x (wal z (wi ph (weq z x)))))
(wex x (wal z (wb (wel z x) (wex y (wa (wel y a) ph))))));
axiom ax-pow: << E. x A. y (A. z (z e. y -> z e. a) -> y e. x) >>
(wex x (wal y (wi (wal z (wi (wel z y) (wel z a))) (wel y x))));
axiom ax-un: << E. x A. y (E. z (y e. z /\ z e. a) -> y e. x) >>
(wex x (wal y (wi (wex z (wa (wel y z) (wel z a))) (wel y x))));
axiom ax-reg:
<< E. x x e. a -> E. x (x e. a /\ A. y (y e. x -> ~ y e. a)) >>
(wi (wex x (wel x a))
(wex x (wa (wel x z) (wal y (wi (wel y x) (wn (wel y a)))))));
axiom ax-inf:
<< E. x (a e. x /\ A. y (y e. x -> E. z (y e. z /\ z e. x))) >>
(wex x (wa (wel a x) (wal y (wi (wel y x)
(wex z (wa (wel y z) (wel z x)))))));
axiom ax-ac:
<< E. x A. y (y e. a -> E. z z e. y ->
E! z (z e. y /\ E. w (w e. x /\ y e. w /\ z e. w))) >>
(wex x (wal y (wi (wel y a) (wi (wex z (wel z y))
(weu z (wa (wel z y) (wex w
(wa (wa (wel w x) (wel y w)) (wel z w)))))))));
}
nonempty sort class;
var A B: class*;
term cab (x: set) (ph: wff x): class;
term welc (a: set) (A: class): wff;
notation cab (x: set) (ph: wff x) := << { x | ph } >>;
{
local infix welc: e. 50;
axiom ax-8b: << a = b -> a e. A -> b e. A >>
(wi (weq a b) (wi (welc a A) (welc b A)));
axiom ax-clab: << x e. {x | ph} <-> ph >>
(wb (welc x (cab x ph)) ph);
def wceq (A B: class): wff :=
<< A. x (x e. A <-> x e. B) >>
(wal x (welc x A) (welc x B)) {
infix wceq: = 50;
theorem df-ceq: << A = B <-> A. x (x e. A <-> x e. B) >>
(wb (wceq A B) (wal x (welc x A) (welc x B)));
}
def cv (a: set): class := << {x | wel x a} >>
(cab x (wel x a)) {
coercion cv: set -> class;
theorem df-cv: << a e. b <-> wel a b >>
(wb (welc a (cv b)) (wel a b));
}
}
def wcel (A B: class): wff :=
<< E. x (x = A /\ welc x B) >>
(wex x (wceq (cv x) A) (welc x B)) {
infix wcel: e. 50;
theorem df-cel: << A e. B <-> E. x (x = A /\ welc x B) >>
(wb (wcel A B) (wex x (wceq (cv x) A) (welc x B)));
}