Skip to main content
8 votes

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

Concerning your actual proof attempt: Here is the completed proof: ...
Thierry Arnoux's user avatar
7 votes
Accepted

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

I rewrote my answer, but still I don't really know Metamath per se. I'm just going off of your logic. If you tell me I'm completely misunderstanding, I'll delete my answer. So far it looks like you ...
Jason Rute's user avatar
  • 8,825
7 votes
Accepted

Kunen's inconsistency axiom-free proof on Metamath

The answer to this question is a tentative "yes", but it depends on how you interpret the resulting statement. From my understanding, there isn't anything about "elementary embedding&...
Mario Carneiro's user avatar
6 votes
Accepted

How "generic" are "generic proof assistants"?

Isabelle/Sequents contains a formalisation of intuitionistic linear logic, so conceivably you have a chance of implementing your logic in Isabelle, following the techniques used there. Whether what ...
Lawrence Paulson's user avatar
2 votes

metamath meta variables

I'm not an expert in any of Metamath, Isabelle (Isabelle/ZFC or otherwise) or Mizar, but I did some research on this topic when Hamster asked me essentially the same question a couple of days ago. So ...
Theo H's user avatar
  • 121
2 votes
Accepted

Metamath unification example

I'm assuming you want to achieve this in the set.mm database for set theory with classical logic. In that case, everything is a set (or a class), and therefore we have to look for sets which can ...
Thierry Arnoux's user avatar
2 votes
Accepted

Metamath - simple equation solution / proof

Here is a proof for the first direction: A = 2 -> ( A + 2 ) = 4 ...
Thierry Arnoux's user avatar
1 vote

metamath meta variables

I can make a few comments about Mizar's axiomatic set theory compared to ZFC, and give pointers to the code where it is stated. The ZF Axioms in Mizar are contained in ...
Alex Nelson's user avatar
  • 1,564
1 vote
Accepted

Can context-free languages be automatically formalized with Metamath?

Yes, there are no apparent obstacles. The two nuances are typecodes and ambiguous constructions, as detailed in the second link in the question. That said, it probably isn't a good idea to directly ...
Corbin's user avatar
  • 119

Only top scored, non community-wiki answers of a minimum length are eligible