Section 1 : Logic

By “logic” here we mean the study of propositions. A proposition is a true/false statement. For example 2+2=4, 2+2=5, and the statement of the Riemann Hypothesis are all propositions.

Basic mathematics with propositions involves learning about how functions like →, ¬, ∧, ↔ and ∨ interact with propositions like true and false.

In Lean we can prove mathematical theorems using tactics such as intro and apply. The purpose of this section is to teach you ten or so basic tactics which can be used to solve logic problems.

Fire up a Lean session, open up the formalising-mathematics-2022 Lean repository, find section01 within the src directory of the repository, and try doing the problem sheets! If you need help getting started, you can read the below, or you can watch the video TODO make a video and link to it here.

Lean’s notation for logic.

In Lean, P : Prop means “P is a proposition”, and P → Q is the proposition that “P implies Q”. Note that Lean uses a single arrow → rather than the double arrow ⇒.

The notation h : P means any of the following equivalent things:

  • h is a proof of P;

  • h is the assumption that P is true;

  • P is true, and this fact is called h.

Here h is just a variable name. We will often call proofs of P things like hP but you can call them pretty much anything.

WARNING: do not confuse P : Prop with hP : P. The former means that P is a true-false statement; the latter means that it is a true statement (and hP is its proof).

Lean’s tactic state.

Lean’s “tactic state”, or “local context”, is what you see on the right hand side of the screen when you have Lean up and running. In the middle of a proof it might look something like this:

P Q : Prop
hP : P
hPQ : P → Q
⊢ Q

The proposition after the “sideways T” at the bottom (it’s called a “turnstile” apparently) is the thing you are supposed to be proving – this is the goal of the level of the game. The stuff above the turnstile is the stuff you are assuming. In the example above, P and Q are propositions, and we are assuming that P is true and that P implies Q, and we are supposed to be proving that Q is true. If you succeed in proving the goal, Lean will display a “goals accomplished 🎉” message and, assuming you didn’t use sorry at any point (which is cheating), you’ve solved the level.

How then do we manipulate the tactic state? We do this using tactics, which you type in on the left hand side of the screen, between a begin and an end. Take a look at some of the tactic documentation in Part C of this book to learn more about tactics. If you’re just getting started, then try reading about intro, apply and exact. Those are the tactics you’ll need to solve the levels in the first problem sheet of the course, logic sheet 1 in section 1.