- Constructing Boolean algebra using type theory

Here we look at constructing logic using type theory. Now, mostly all branches of mathematics involve two kinds of entities: objects and propositions about those objects. This very much corresponds to basic composition of programming languages - objects and their APIs.

Type with no object - cannot ever create an object of this type. This makes it possible to define absurd functions, which map `⟂`

to anything, as given nothing, one can create anything, or assuming any `False`

statement can serve as a proof for anything, which is absurd.

Absurd can imply anything, be it true or not. Thus, any statement can be proven using absurdity.

However, it is, we argue, impossible to create an object of absurd type (as `⟂`

has no constructor) and hence these functions make no sense in the “real world”, as in they can never be invoked. This is called the “absurd pattern”.

Set with only one object: `True`

.

We also have a more standard representation of boolean objects, Bool.

`NOT`

We use the fact that a negation of a proposition `P`

(to exist and hence be true) implies `¬ P`

has to be false, `⟂`

.

`∧`

or the logical `AND`

The logic `AND`

and `OR`

are pretty straightforward for both representations:

`OR`

These higher-order operations are built by composing the lower ones in various ways:

Implication, or `if P then Q`

, is derived from the well-known construction

\[ a ⟹ b = ¬ a ∨ b \]

Notice how the two implementations are different: `⟹`

is constructive, whereas `impl`

is computatational.

`XOR`

The absurd pattern for proving `Whatever`

, we discussed above:

A proposition `P`

can always be true `⊤`

if `¬ P`

is always false `⟂`

. If one were to assume a contradictory proposition `P`

, one could prove anything as a contradiction makes `P`

absurd. This is called as “ex falso quodlibet” or “from falsity, whatever you like”. We can `⟂-elim`

it in such a way to prove this:

```
contradiction : ∀ {p w} {P : Set p} {Whatever : Set w}
→ P
→ ¬ P
→ Whatever
contradiction p (¬p) = ⟂-elim (¬p p)
```

Consider two propositions, `A`

and `B`

. Now if `A → B`

is true, then `¬ A → ¬ B`

will be true. In other words, if a statement `A`

always implies another `B`

, then `B`

not being true would imply `A`

not being true. This is called a contraposition and is proven in the following manner:

```
contrapos : ∀ {a b} {A : Set a}{B : Set b}
→ (A → B)
→ ¬ B → ¬ A
contrapos f ¬b a = contradiction (f a) ¬b
```

We can obviously go ahead now and implement the `if-then-else`

semantic:

```
if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true then x else y = x
if false then x else y = y
```

Note again that since this is a computational semantic, we provide implementation for only the concrete type `Bool`

.

Existential Quantification, or better known as “there exists” or `∃`

, essential indicates if a proposition can exist:

This is a dependent type, which creates propositions from a proposition family `P`

: