Pure mathematics is all about proofs, so we have to learn how to do proofs.
Let’s start with a super-abstract proof. Let’s just take three random mathematical true/false propositions , and , and let’s say that we know that implies , and that implies . Can we deduce that implies in Lean? Let’s take a look at this. Oh — to get the cute little arrow try writing “\to ” and to get the cool and sign try “\and “.
-- anything after two minus signs like this is a comment. variables P Q R : Prop -- P, Q, R are now true/false statements. -- Reminder : ∧ means "and". theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) := begin admit end
Here “admit” means “I haven’t done that proof yet”. Sort-of like admitting defeat.
If you click here you’ll open a version of Lean running in your browser, with the above code pasted in.
OK so here is the strategy for proving this. First of all, we establish that
P → Q and that
Q → R. We want to prove that
P → R, so we assume
P, we deduce
P → Q and then we deduce
Q → R
In Lean, it looks like this.
-- anything after two minus signs like this is a comment. variables P Q R : Prop -- P, Q, R are now true/false statements. -- Reminder : ∧ means "and". theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) := begin intro H, -- H is "P implies Q and Q implies R" have HPQ : P → Q, exact H.left, have HQR : Q → R, exact H.right, clear H, -- we don't need it any more -- We now have hypothesis HPQ, which is P -> Q -- and hypothesis HQR, which is Q -> R. -- We want to prove P -> R so let's assume P -- and deduce R. intro HP, have HQ : Q, exact HPQ HP, -- apply P->Q to P to get Q. -- now we can get the goal exact HQR HQ end
This is hard to understand if you do not have the code running in a Lean session, so try it out, or, even better, get Lean running on a computer near you and cut and paste it in (who knows if this will work).
We can skip steps. Here are some shorter versions.
variables P Q R : Prop theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) := begin intro H, -- H is "P implies Q and Q implies R" intro HP, -- we want P -> R so let's assume P. have HQ : Q, exact H.left HP, -- apply P->Q to P to get Q. -- now we can get the goal exact H.right HQ end
variables P Q R : Prop theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) := begin intros H HP, exact H.right (H.left HP) end
Try and figure out how this works. “Intros” is just introducing more than one thing at once. The thing in the brackets in the last but one line evaluates to a proof that
Q is true.
Here’s another example. We need to talk about “not”. The idea is that
not P is supposed to be the opposite of
P — i.e. if
P is true then
not P is false, and if
P is false then
not P is true. There’s a really cute way to do this in logic — we can define
not P to be
P → false. This works because (true implies false) is false, and (false implies false) is true.
In VS Code or Lean online, you can write
\not instead of not, and it will give you some weird symbol, which is the notation used by some computer scientists and logicians.
The contrapositive of the statement
P → Q is
not Q → not P. The contrapositive of a statement should follow from the statement itself, so we should be able to prove this:
variables P Q : Prop example : (P → Q) → (¬ Q → ¬ P) := begin admit end
Try firing this up, and use the intro (or intros) commands to see how many hypotheses you can introduce. If you keep using “intro” to introduce as many hypotheses as you can all at once, then a funny thing happens!
variables P Q : Prop example : (P → Q) → (¬ Q → ¬ P) := begin intro HPQ, -- HPQ is P implies Q intro HnQ, -- HnQ is "not Q" -- our goal is now "not P", i.e. "P implies false". intro HP, -- this is hypothesis P. admit end
Run this in Lean, click on “admit” and see what happens.
Rather weirdly, our goal (the thing we’re supposed to be proving) is now the word “false”, which apparently means that our job is to prove something which isn’t true. This sounds tricky, until you realise that we are allowed to assume a bunch of hypotheses which actually can’t all be true, so this is really just what a mathematician would call a proof by contradiction.
Our hypotheses include both P and “P implies Q”, so we can deduce Q from these. Another hypothesis is “Q implies false”, so if we put it all together we can indeed prove “false”! Try it yourself, or see this in action here.
For an even cooler finish, we can use “contradiction”, which proves anything you like from two contradictory assmptions. Here is the proof using the contradiction tactic.
I need to say one more important thing. Clearly every proposition is either true or false, so in other words we should be able to prove this:
variable P : Prop example : P ∨ ¬ P := begin admit end
How do we do this? Well, we can’t 😀 Computer scientists have a name for this basic fact — it’s apparently called “the law of the excluded middle”. Amazingly, this basic fact is not built into Lean by default, as apparently some computer scientists try and do mathematics without assuming it. We are mathematicians, so we will assume it. We can (and definitely should!) add it in as an axiom in fact.
axiom em (X : Prop) : X ∨ ¬ X -- no proof required, it's an axiom. variable P : Prop example : P ∨ ¬ P := begin exact em P end
Without assuming this as an axiom, “P or not P” is actually an unprovable statement for a general proposition P, in Lean. This just reflects the fact that Lean is designed for computer scientists as well as mathematicians. In fact more generally there is a “maths library” for Lean, called mathlib, which is not loaded into Lean by default, but which we as mathematicians will definitely need. I do not know how to load this library into the online version of Lean but I do know how to install it on a computer.
Questions 2 to 4 on M1F example sheet 1 might need to assume the law of the excluded middle. In fact, worrying about whether something assumes the Law of the Excluded Middle or not is not really a question for mathematicians, we just assume it.