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.

Filter by
Sorted by
Tagged with
2 votes
2 answers
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 ...
Hamster's user avatar
  • 21
2 votes
1 answer
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 ( ...
Jorge Agra's user avatar
3 votes
1 answer
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-...
Jorge Agra's user avatar
0 votes
1 answer
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 ...
Corbin's user avatar
  • 119
10 votes
1 answer
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 ...
Max New's user avatar
  • 304
8 votes
1 answer
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 ...
Ember Edison's user avatar
7 votes
0 answers
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 ...
Guy Coder's user avatar
  • 2,836
8 votes
2 answers
180 views

What is the closest you can get to introducing and discharging hypotheses in metamath?

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 ...
Greg Nisbet's user avatar
  • 2,711