Mapping Metamath predicate logic to traditional predicate logic

[Andrew Lubrino]

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!

[Jim Kingdon]

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".

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/dd154ec9-243a-46f8-a30d-9766fce108fan%40googlegroups.com.

[Andrew Lubrino]

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! 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/94691495-f33a-71ec-999a-d716769385f8%40panix.com.

[Jim Kingdon]

On March 25, 2022 1:19:08 PM PDT, Andrew Lubrino <andrew...@gmail.com> 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.

>> <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 metamath+u...@googlegroups.com.
>> 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>
>> .
>>
>

[Thierry Arnoux]

Hi Andrew,

I don't think hoping/dreaming for better tools is against The Metamath Way or anything.

Completely agree!

Following a discussion in this group a while ago, I've started to work on a VS Code extension for Metamath, you can find it here: https://github.com/tirix/metamath-vspa. It currently provides features such as syntax highlighting, "go to definition", "search references", "show proof", etc. Glauco has been helping with testing.

I would like to add other functionalities so that it can match the Eclipse plugin I've been using to do formalization, hopefully also including some proof assistant functionality. I also think one could build it up to a Metamath proof assistant using tactics, but that's a longer term goal.

BR,
_
Thierry