Metamath Zero

[Mario Carneiro]

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 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)));

  }

* The "sort" keyword declares a new typecode.

* "var" is like "$f".

* "bound" is another kind of variable, that can appear in binders. (Each mm0 sort is represented by two mm sorts, one for bound variables and one for terms. Only bound variables can participate in DV conditions.)

* "term" declares a new axiomatic term constructor.

* DV conditions are implicitly declared by saying what a variable depends on. The global wff variables are declared with type " wff* " meaning that they are open terms, they are not disjoint from anything. The global set variables a,b are declared as "set" meaning that they are disjoint from all bound variables in theorems containing these variables. Bound variables are always disjoint from each other.

* "def" declares a definition. Different from both Ghilbert and Metamath, definitions here are "limited lifetime unfolded". Each def has a block after it containing one or more theorems about the definition. These theorems are proven where the definition is replaced by the definiendum, and once the block is closed these theorems are the only access to the definition. (This enables some information privacy if desired.) See wb for example, which uses characterizing theorems instead of an iff.

* The notation system turned out a bit more complicated than I'd hoped. Each "math expression" is stated twice, once in chevrons and once in s-expression notation. The intent is that the system actually uses the s-expressions to represent the axioms (so there is no parse tree funny business), and because they form part of the trust base they are displayed to the user. The notation in the chevrons is checked only in the reverse direction - the s-expression is printed and compared to the given string. (In an IDE there would be a mode where you only type the notation and the computer generates the s-expression.) There is still a danger of ambiguous parsing, but at least you can see the parse directly in the case of a mismatch, and the worst effect of a bad parse is that the theorem being proven is not what the user thought - the ambiguity can't be further exploited in the proof.

You might wonder where the proofs are. They go in a separate file, not human readable. The idea is that this file contains all the information that is necessary to appraise the content and correctness of a theorem, and the proof file is just directions to the verifier to produce a proof of the claimed theorems. In particular, if this "specification file" is inspected and correct, then there is no possible input for the proof file that makes the verifier falsely accept a bad theorem. (So no adding axioms, although new definitions are okay.)

I'm curious to hear what you all think of a project such as this. I'm especially interested in ways to simplify the grammar if we can retain readability.

Mario Carneiro