## Negation

Let’s see how Lean understands negation.

The command `#reduce`

tells Lean to try to peel away notation and write things in a more basic form. So Lean-speak for not of a formula are functions that take proofs of `A`

to proofs of `False`

. With this in mind, $\neg$-elimination is another instance of function application.

If `¬ A`

means `A → False`

, then negation introduction looks very similar to implication introduction.

**Example**. Let’s prove the formula `(A → B) → (¬ B → ¬ A)`

.

Tilting our heads to the side, we can read this as constructing a function which inputs

- A function
`f`

taking proofs of`A`

to proofs of`B`

- A function
`h`

taking proofs of`B`

to proofs of`False`

- A proof
`a`

of`A`

From `f a`

we get a proof of `B`

. Applying `h`

gives us a proof of `False`

. Thus, our output is a proof of `False`

. Since Lean views `¬ A`

as `A → False`

, it accepts this construction.

Repeatedly writing the `fun =>`

is a little tedious. Thankfully, Lean accepts notation more closely adhering to our sense of multivariate functions.

Recall that we can prove anything from `False`

. In Lean, this is

Appending `@`

forces Lean to make explicit some arguments it usually infers from the context. (And makes nicer messages to copy.)

## Proof by contradiction

Recall that proof by contradiction (or reducito ad absurdum) allows us to conclude $A$ from $\neg A \vdash \bot$. In Lean this is called `Classical.byContradiction`

.

We can eliminate double negation using this in Lean.

Note that `fun (n : ¬ A) => h n`

is function that takes proofs of `¬ A`

to proofs of `False`

. Applying `byContradiction`

to this yields a proof of `A`

as we want.

We also have access to the law of the excluded middle built in.

**Example**. Let’s prove the converse of the previous example `(¬ B → ¬ A) → (A → B)`

.

Notice how Lean just “figured out” that we wanted to eliminate `False`

into `B`

.