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.
