- Constructing Boolean algebra using type theory

Here we look at constructing logic using type theory.

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. Looking at it from a different angle, 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 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.

Set with only one object: `True`

.

We also have another representation of boolean objects, Bool.

`NOT`

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

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

has to be false, `⟂`

.

for our other representation:

`∧`

or the logical `AND`

The logic `AND`

and `OR`

are pretty straightforward for both representations:

similarly:

`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
-- a more pythonic style `P ? if_true : if_false` (with universe polymorphism)
_then_else_ : ∀ {a} {A : Set a} -> Bool -> A -> A -> A
true then x else y = x
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`

: