# Questions tagged [metamath]

For questions specific to the proof assistant Metamath. Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.

8 questions
Filter by
Sorted by
Tagged with
83 views

### metamath meta variables

I'm reading https://us.metamath.org/mpeuni/mmzfcnd.html and it says Each "axiom" in Metamath's version of ZFC set theory is not an actual axiom in the language of first-order logic but is a ...
• 21
86 views

### Metamath unification example

Basic question Suppose we define a point and some related stuff: x , y are reals Point ( x , y ) Abscissa ( Point ( x , y ) ) = x Ordinate ( Point ( x , y ) ) = y And we want to have/prove: Point ( ...
118 views

### Metamath - simple equation solution / proof

Sorry if an improper question, looking into metamath and metamath-lamp and though it should be trivial to prove A = 2 -> ( A + 2 ) = 4, or the inverse. But cant seem to get it right in metamath-...
72 views

### Can context-free languages be automatically formalized with Metamath?

In this introduction to Metamath, the author suggests that the $c and$v statements can be viewed as encoding the terminals and ...
• 119
222 views

### How "generic" are "generic proof assistants"?

I've read that Isabelle and Metamath (and maybe Andromeda) are "generic" proof assistants in some sense that allows them to be used to implement different theories such as HOL, ZF and ...
• 304
347 views

### Kunen's inconsistency axiom-free proof on Metamath

Kunen's inconsistency theorem is an important theorem in set theory on upper bounds for large cardinals. It has long been thought to be able to be encoded on ZFC, but the full implementation has never ...
• 231
145 views

### Could the Incredible Proof Machine work automatically with Metamath if rules of Metamath can be automatically translated into IPM custom logic blocks?

The Incredible Proof Machine (pdf) is a visual means of doing proofs. The Incredible Proof Machine can also be extended to do custom logics (Section 2.7 Custom logics). Metamath has thousands of ...
• 2,836
How close can you get to introducing and discharging hypotheses in metamath? I'm trying to define a symbol formal system for the $\land$-only fragment of classical propositional logic. It has the ...