Yeah, maybe I'm being too hard on mmj2. Certainly don't mean to offend the creators / maintainers, but it is old.
Those links helped a lot, but I think I'm still confused about notation maybe. Let's say we have the following formula: (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) Usually, predicates are represented with something like P(x). But here, it doesn't list the variable that the formula includes. In this system, is it possible that there are only two predicates: '=' and 'is a member of' and that every statement is just some combination of those two? In the above formula, are there different names for letters next to quantifiers and Greek letters that represent sentences with true or false values? Sorry for all the basic questions and thanks for the help! On Fri, Mar 25, 2022 at 2:44 AM Jim Kingdon <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/94691495-f33a-71ec-999a-d716769385f8%40panix.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/CAOcJWNE8GksdXNLpGxNeEuD0k6_7BRa7PeUT7vCMLfD%3DDPTaVw%40mail.gmail.com.
