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)));
}
I'm experimenting with a new language, Metamath Zero, an amalgamation of Metamath, Ghilbert and Lean syntax. The goal is to balance human readability and ease of writing a verifier, while also making some attempts to patch the bugs in metamath soundness (not that it's wrong, but there is a lot of soundness justification currently happening outside the metamath verifier kernel). Without giving too much explanation of what the syntax means (it's all fictional syntax at the moment, there is no parser yet), I would like to use some of you as guinea pigs for the "readability" aspect. How obvious is it what things mean? I will put some more explanatory comments at the end.nonempty sort wff;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