# Introduction to Logic (with Lean)

(under construction ... feel free to get in touch if that interests you)

This introduction to logic starts out as a running commentary to the [Lean Intro to Logic](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/), an online game one can start playing without much background in programming, math or logic.

The first aim of these notes is to get you started on the game.

But, more importantly, the Lean-Intro-to-Logic game is based on a long history of deep and far reaching concepts in philosophy, logic, mathematics and computer science. As we go along, I want to highlight these ideas and encourage the reader to take the Lean Intro to Logic as a spring board into one of the most beautiful areas of philosophy and science.

In footnotes I add references that can be ignored at first but will be of interest later.

Under [Propositional Intutionistic Logic](https://hackmd.io/@alexhkurz/rkgaquGrR), I link the full formal summary of what we are going to learn in terms of rules of logical reasoning. Study the rules and speculate what they might mean in terms of programming.

## Introduction

The fundamental idea is [^bhk]

[^bhk]: If you want to read ahead check out [Brouwer–Heyting–Kolmogorov interpretation](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation) and [Curry-Howard Correpondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence).

$$
\text{propositions are types,}
$$

$$
\text{proofs are programs.}
$$

Lean is a programming language in which programs are proofs and proofs are programs.

The notation

$$
a:A
$$

can be read in three ways:

- $a$ is data of type $A$;[^declarations]
- $a$ is a proof of the proposition $A$;
- $a$ is an element of the set $A$ (as in $a\in A$).

[^declarations]: If $a$ is a variable this is known as variable declaration in programming languages. For example, $a:\mathbb Z$ in Lean and $a\in \mathbb Z$ in math correspond to`int a;` in C, C++, Java, C#.

In the following we will work through the Lean Intro to Logic building up a logical language for propositions $A$ and a programming language for programs $a$.

## The logic of "and"

We start with a simple language where the only programs we can write are lists:

- If $a$ is data of type $A$ and $b$ is data of type $B$ then the list $\langle a,b\rangle$ is data of type $A\wedge B$.

(Read $A\wedge B$ as "A and B".)

- If $c:A\wedge B$ is a list, then we can decompose the list $c$ into its components with $c.\text{left}$ (which is of type $A$) and $c.\text{right}$ (which is of type $B$). [^equations]

[^equations]: If you wonder whether this means that $c=\langle c.\text{left}, c.\text{right}\rangle$ and $\langle a,b\rangle.\text{left}=a$ and $\langle a,b\rangle.\text{right}=b$ then the answer is yes.

Ok, now you are ready to plunge in and take your first lesson in programming in Lean.

### The $\wedge$ Tutorial

Work through the [$\wedge$ Tutorial](https://hackmd.io/@alexhkurz/SJJGQQpmR) in Lean.

My recommendation is to read the rest of the section only after you worked through the $\wedge$ Tutorial.

In the following you will meet some advanced concepts such mathematical proofs, natural deduction, introduction and elimination rules and the distinction between meta and object language.

### Outlook and Explanations

Mathematically, the $\wedge$ Tutorial can be summarized by the following two rules of logic.

#### $\wedge$-introduction

$$
\frac{A\quad\quad B}{A\wedge B}
$$

#### $\wedge$-elimination

$$
\frac{A\wedge B}{A}
\quad\quad\quad\quad
\frac{A\wedge B}{B}
$$

**Explanation:**

- $\wedge$-introduction says "if $A$ and $B$ then $A\wedge B$". Or, if you have a proof of $A$ and a proof $B$ then you also have a proof of $A\wedge B$.
- Left $\wedge$-elimination says that "if $A\wedge B$ then $A$" and right $\wedge$-elimination says "if $A\wedge B$ then $B$". Or, if you have a proof of $A\wedge B$ then you also have a proof of $A$ (resp $B$).
- Together these rules just say that "$A$ and $B$" is the same as $A\wedge B$.
- We have logic here at two levels. At the meta-level we use "and" and natural language. At the object-level we use $\wedge$ and the formal language of mathematical logic.
- The distinction between meta-level and object-level is familiar from programming. The object-level language is the programming language (Python, Java, Lean, etc) and the meta-level language is the language in which programmers and users talk about programs.

#### A Proof in Natural Deduction

The two rules above are part of a mathematical proof system called [Natural Deduction](https://en.wikipedia.org/wiki/Natural_deduction). In natural deduction [Level 8 of the $\wedge$ Tutorial](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/AndIntro/level/8)


could be written as follows.

Assuming

$$
((P ∧ S) ∧ A) ∧ (¬I ∧ ((C ∧ ¬O) ∧ ¬U)),
$$

we need to prove

$$
A\wedge (C\wedge(P\wedge S)).
$$

Using the rules of $\wedge$-introduction and of $\wedge$-elimination we can do this as follows.

> (1) $((P ∧ S) ∧ A) ∧ (¬I ∧ ((C ∧ ¬O) ∧ ¬U))$
> (2) $(P ∧ S) ∧ A$
> (3) $P ∧ S$
> (4) $A$
> (5) $(¬I ∧ ((C ∧ ¬O) ∧ ¬U))$
> (6) $(C ∧ ¬O) ∧ ¬U$
> (7) $C ∧ ¬O$
> (8) $C$
> (9) $C\wedge(P\wedge S)$
> (10) $A\wedge (C\wedge(P\wedge S))$

In mathematics, in a proof, each line must be justified.

I go through the proof above line by line, writing out the justification. (Take a mental note of how each line is justified so that you can do this in the future yourself.)

> (1) is an assumption.
> (2) by left $\wedge$-elimination applied to (1).
> (3) by left $\wedge$-elimination applied to (2).
> (4) by right $\wedge$-elimination applied to (2).
> (5) by right $\wedge$-elimination applied to (1).
> (6) by right $\wedge$-elimination applied to (5).
> (7) by left $\wedge$-elimination applied to (6).
> (8) by left $\wedge$-elimination applied to (7).
> (9) by $\wedge$-introduction applied to (8) and (3).
> (10) by $\wedge$-introduction applied to (4) and (9).

**Discussion:** Sometimes a Lean proof can be easier, sometimes a math proof. Which one do you like better?

### Trees

An important idea is that we can form lists of lists. This is also called nested lists. And nested lists are trees.

$A\wedge B\wedge C$ is an abbreviation for $A\wedge (B\wedge C)$.[^abbrev]

We can depict this as

  ∧
 / \
A   ∧
   / \
  B   C

**Exercise:** First add all missing parentheses to $(A\wedge B \wedge C) \wedge D\wedge E$ and then write the expression in tree notation.

[^abbrev]: It is also common to say that $A\wedge B\wedge C$ abbreviates $(A\wedge B)\wedge C$, but Lean decided to have $\wedge$ "associative on the right".

## The logic of "if-then"

With only lists $\langle a,b\rangle$ available, we seem to be far away from a complete programming language. All we can do with the language from the previous section is to assemble and take apart lists (or trees).

At the end of this section you will have learned the basics of a complete programming language known as lambda-calculus or $\lambda$-calculus. So buckle in and get ready for a ride.

The fundamental idea is that to prove an implication "if A then B", in symbols

$$
A\to B,
$$

is equally to program a function

$$
\lambda a \mapsto b
$$

that takes inputs of type $A$ to outputs of type $B$.

There is more to explain here, but I think it is best you give the tutorial a try.

### The $\to$ Tutorial

Work through the [$\to$ Tutorial](https://hackmd.io/@alexhkurz/Hy7Q021EA) in Lean.

My recommendation is to read the rest of the section only after you worked through the $\wedge$ Tutorial.

### ... tbc ...