# Tag Info

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

Concerning your actual proof attempt: Here is the completed proof: ...
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 ...
• 8,825
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&...
• 1,589
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 ...

### 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 ...
• 121
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 ...
Accepted

### Metamath - simple equation solution / proof

Here is a proof for the first direction: A = 2 -> ( A + 2 ) = 4 ...
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 ...
• 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 ...
• 119

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