$\newcommand{\sem}[1]{[\![#1]\!]}$

# Completeness of Propositional Logic

(under construction)

(part of my course Programming Languages)

In a previous lecture, we studied a language of arithmetic expressions, gave it an operational and denotational semantics and proved that the operational and denotational semantics agree.

This can be taken as an instance of the more general idea that one should prove that the implementation[^opsem] satisfies the specification[^densem].

[^opsem]: We can think of the operational semantics of a programming language as its implementation via an interpreter.

[^densem]: We can think of the denotational semantics of a programming lnaguage as its specification. (But note that terms like "implementation" and "specification" change their meaning depending on the context.)

In this lecture, we replace arithmetic expressions by Boolean expressions.

Moreover, we use the opportunity to present the material not from the point of programming languages but from the point of logic. The fact that everything we do in this lecture can be expressed both in terms of logic and interms of programming languages is interesting in its own right and one of the points we want to make.

## Venn Diagrams

We all know [Venn Diagrams](https://en.wikipedia.org/wiki/Venn_diagram#Overview).

Venn Diagrams can be used not only for illustrating logical relationships but also to justify reasoning. For example, we can prove

$$(A\cup B)^c = A^c\cap B^c$$

by looking at [this diagram](https://en.wikipedia.org/wiki/Venn_diagram#/media/File:Venn0111.svg).

While Venn diagrams are good for explaining basic logical relationships, they are not the best tool for reasoning. And certainly not suitable for implementing reasoning on a computer.

For this purpose, George Boole invented what is known today as Boolean rings or Boolean algebra.

Two big ideas of Boole were to extend algebra to a language underpinning all of science and to create a version of calculus in which the truth values $0,1$ play a role similar to the real numbers in Newton's calculus.

## A Programming Language for Boolean Expressions

In programming languages, we are familiar with the datatype of Booleans. In analogy with the previous lecture, we define define the language

$$\mathcal L$$

via the context-free grammar (in BNF)

$$ e ::= \bot\mid\top\mid e\vee e \mid e\wedge e \mid \neg e \mid p$$

We read
- $\bot$ as bottom or false
- $\top$ as top or true
- $\vee$ as or
- $\wedge$ as and
- $\neg$ as not

$p$ is a letter ranging over a fixed set $P$ of 'atomic propositions'. In programming language terms, what is called an atomic propositions in logic would comprise expressions such as `x==2` or `x<y` etc.

Atomic propositions are considered to vary over truth values and are often called propositional variables.

In logic, expressions in this language are called *formulas* of propositional logic. One often uses the Greek letter $\phi$ to denote formulas.

## Denotational Semantics of Boolean Expressions

Let $\phi$ be Boolean formula with atomic propositions in $P=\{p,q,r\}$.

We could try to give a semantics of formulas directly in terms of Venn diagrams. Instead we will go back to truthtables.

**Activity:** Write down an example of a formula $\phi$ and translate it into a truth table.

**Activity:** Write down the type of truthtables in Haskell.

**Activity:** Write down the type of t has a type in Haskell.

In the following, I write

$$\sf TT$$

for the type of truth tables.

## An Axiomatization of Boolean Algebra

Again following the previous lecture on arithmetic, we are going to relate syntax and semantics via functions

$$\sem{-}:\mathcal L\to \sf TT$$

and

$${\sf nf}: \sf TT \to \mathcal L$$

We defined the normal form of a truth table via its [disjunctive normal form](https://en.wikipedia.org/wiki/Disjunctive_normal_form).

This definition is made in a way that the following is true:

**Proposition:** For every truth table $t\in\sf TT$, we have $\sem{{\sf nf}(t)} = t$.

What about the other direction, ${\sf nf}(\sem{e})$ for expressions $e\in\mathcal L$?

**Activity:** Compute the disjunctive normal form of the truth-table of the implication $p\to q$.

As this example shows (taking $\neg p\vee q$ for $e$), **we do not** have

$${\sf nf}(\sem{e}) = e.$$

On the other hand, if we throw in some equations, which we will write using $\equiv$, we can have

$${\sf nf}(\sem{e}) \equiv e.$$

Moreover, if we set out to prove ${\sf nf}(\sem{e}) \equiv e$ for all expressions $e$, we will find the needed equations on the way.

In class, we didnt finish a formal proof, but we indicated the process that would lead us to the well-known [axioms of Boolean algebra](https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Definition) (we would write $\equiv$ where Wikipedia has $=$).

**Recommended Homework:** For each [axiom of Boolean algebra](https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Definition) find a Boolean expressions $e$ such that the proof of

$${\sf nf}(\sem{e}) \equiv e$$

requires this equation.

**Ambitious Homework:** Prove by induction over the grammar $e ::= \bot\mid\top\mid e\vee e \mid e\wedge e \mid \neg e \mid p$ that ${\sf nf}(\sem{e}) \equiv e$ holds for all Boolean expressions $e$.