Did you try going through
http://us.metamath.org/mpeuni/mmset.html#traditional and
http://us.metamath.org/mpeuni/mmset.html#distinct ? I suspect that might
be closer to what you are looking for than those papers.
As for the MM1 video, I totally agree. Although I've learned to do
things in mmj2 and am OK with living with its quirks, when I saw the MM1
video my reaction was some version of "oh yeah, that's what all this
stuff should be".
On 3/24/22 17:38, Andrew Lubrino wrote:
Hello there friends.
I emailed this group some months ago about learning discrete math
using Metamath. That thread persuaded me to double down on studying
with Lean. I made some progress with Lean, but it is monolithic and I
have too many gaps in my understanding to continue making progress there.
I approached Metamath again and found that the tooling was really bad.
Then I watched Mario's MM0 and MM1 video. The MM1 proof assistant is
awesome. All the simplicity of Metamath with a modern interface. Wow.
So I started using the MM1 proof assistant (along with Mario's
set.mm0). I've managed to prove many useful theorems in propositional
logic, but I'm having trouble understanding the non-traditional form
of predicate logic that comes with set.mm.
Are there any resources to help beginners learn the "finitely
axiomatized" predicate calculus? I tried to read Norm's paper on the
subject, but it is incomprehensible to me. I also tried to read
Tarski's paper, but it is behind a paywall. Is there any simple
mapping of Norm's system to the natural deduction version of predicate
logic I already know?
Thanks for the help!
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/dd154ec9-243a-46f8-a30d-9766fce108fan%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/dd154ec9-243a-46f8-a30d-9766fce108fan%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/94691495-f33a-71ec-999a-d716769385f8%40panix.com.
