- Constructing Boolean algebra using type theory

Here we look at constructing logic using type theory.

```
module Logic.logicBasics where
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
```

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.

`data ⟂ : Set where`

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`

.

```
data ⊤ : Set where
: ⊤ singleton
```

We also have another representation of boolean objects, Bool.

`open import Lang.dataStructures using (Bool; true; false)`

`NOT`

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

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

has to be false, `⟂`

.

```
: ∀ {a} → Set a → Set a
¬ = P → ⟂ ¬ P
```

for our other representation:

```
: Bool → Bool
not = false
not true = true not false
```

`∧`

or the logical `AND`

The logic `AND`

and `OR`

are pretty straightforward for both representations:

```
data _∧_ (A B : Set) : Set where
: A → B → A ∧ B
AND
infixr 4 _∧_
```

similarly:

```
_&&_ : Bool → Bool → Bool
= x
true && x = false
false && x
infixr 4 _&&_
```

`OR`

```
data _∨_ (A B : Set) : Set where
: A → A ∨ B
inj1 : B → A ∨ B
inj2
infixr 4 _∨_
```

```
_||_ : Bool → Bool → Bool
= true
true || x = false
false || x
infixr 4 _||_
```

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 \]

```
data _⟹_ (A B : Set) : Set where
: (¬ A) ∨ B → A ⟹ B it⟹
```

```
: Bool → Bool → Bool
impl = (not x) || y impl x y
```

Notice how the two implementations are different: `⟹`

is constructive, whereas `impl`

is computatational.

`XOR`

```
data _⨁_ (A B : Set) : Set where
: A → B → (A ∨ B) ∧ (¬ (A ∧ B)) → A ⨁ B ⨁₁
```

```
: Bool → Bool → Bool
xor = (x || y) && (not (x && y)) xor x y
```

The absurd pattern for proving `Whatever`

, we discussed above:

```
: ∀ {w} {Whatever : Set w}
⟂-elim → ⟂ → Whatever
() ⟂-elim
```

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:

```
: ∀ {p w} {P : Set p} {Whatever : Set w}
contradiction → P
→ ¬ P
→ Whatever
(¬p) = ⟂-elim (¬p p) contradiction 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:

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

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

semantic:

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

```
data ∃ {A : Set} (P : A → Set) : Set where
: {x : A}
exists → P x
→ ∃ P
```

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

:

```
: {A : Set}(P : A -> Set) -> Set
∏ {A} P = (x : A) → P x ∏
```