On March 25, 2022 1:19:08 PM PDT, Andrew Lubrino <[email protected]>
wrote:
>Yeah, maybe I'm being too hard on mmj2. Certainly don't mean to offend the
>creators / maintainers, but it is old.
Old and.... well I don't want to offend anyone either (partly because mmj2 is
pretty useful) but I don't think hoping/dreaming for better tools is against
The Metamath Way or anything.
>Usually, predicates are represented with something like P(x). But here, it
>doesn't list the variable that the formula includes.
It is backwards from what you are expecting. In metamath you list the variables
that it *does not* contain. See http://us.metamath.org/mpeuni/df-sb.html for
more on the P(x) notation and how it is problematic.
You can also look at the "allowed substitution hints", described at
http://us.metamath.org/mpeuni/mmset.html#allowedsubst which shows something a
bit closer to what you are thinking of.
>Sorry for all the basic questions and thanks for the help!
That's what this list is for. We've documented most of this stuff in various
ways, but it can sometimes take a bit of help to find the relevant information
and understand what you are reading.
>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/83F034D8-E0DB-42F0-84DC-D051EBE909CA%40panix.com.
