## Propositions in Lean

The engine that makes Lean interactive theorem verifier and prover is the idea that every piece of data has a type. This include mathematical data. So the natural numbers have (are) a type `Nat`

as are the real numbers. Individual natural numbers are called *terms* of type `Nat`

. To express this relationship, we write `5: Nat`

. If you know a little set theory, it will be harmless to imagine replacing the semi-colon with an element symbol $\in$.

Lean has type for propositions called `Prop`

. We can think of this as the whole universe of possible propositions. A term of `Prop`

is a individual proposition.

Suppose I have propositional variables $A,B,C$ in my logic. How do I tell Lean about them? We declare them as variables.

A useful tool built into the system is the ability to check what Lean believes an expression means.

The window pane on the right hand side of the editor reports `D: Prop`

which Lean reporting back that indeed it thinks `D`

is a proposition.

Next we can combine propositional variables into formulas.

## Connectives

Let’s see how each of our connectives, $\neg, \to, \lor, \land,$ and $\leftrightarrow$ are encoded in Lean.

Here is negation

Lean tells that indeed `¬ A : Prop`

. Note that ¬ is a Unicode symbol (like emoji). In general, we do not have those on our keyboard but the editor nows how to fill it in if we type `\neg`

and hit the spacebar.

Unicode is pretty but we can also use standard (ASCII) characters to access negation.

will also report `¬ A : Prop`

.

We mentioned that everything in Lean has a type. What about Not? Checking it returns `Not : Prop → Prop`

. If we interpret this (Unicode) arrow as an assignment, this makes sense. Given a formula `X`

, `¬ X`

is another one.

Next, we turn to implication, $\to$. It has the same Unicode arrow ( typeset as `\to`

)

gives that `A → B : Prop`

.

For conjunction, $\land$, we have (at least) three notations that all work:

Here `∧`

is typed using `\and`

.

Next we have disjunction.

Note the text between `/- -/`

. This tells Lean that to ignore the what is written. They are only comments and not commands.

Finally, bi-implication.

Aside from negation, all of the other connectives take in two formulas and yield a single one. So if you `#check Iff`

you will get `Iff : Prop → Prop → Prop`

. What happens if you `#check ↔`

?