Zulip Chat Archive

Stream: new members

Topic: tutorials 0019/20

Sara Fish (Jul 10 2020 at 00:39):

In the text right between 0019 and 0020 in this tutorial (https://github.com/leanprover-community/tutorials), they write

Similarly, given a proof h of P ↔ Q, one can get a proof of P → Q using h.mp
and a proof of Q → P using h.mpr

What do mp and mpr stand for?

Yakov Pechersky (Jul 10 2020 at 00:44):

modus ponens and modus ponens, reversed

Sara Fish (Jul 10 2020 at 00:46):

Ah, of course! Thanks.

Heather Macbeth (Jul 10 2020 at 01:12):

That's funny, I always thought mp was a mnemonic for "implies" :)

Johan Commelin (Jul 10 2020 at 02:44):

It's true that I don't think I've ever had this terminology used in any of the courses I took...

Kevin Buzzard (Jul 10 2020 at 14:08):

But you took very few if any logic courses, right?

Last updated: Dec 20 2023 at 11:08 UTC