Hierarchy of logical systems

This post is a generalization to one of my previous posts, Abstractions with Set Theory.

At its core, mathematical logic deals with mathematical concepts expressed using formal logical systems.

These systems, though they differ in many details, share the common property of considering only expressions in a fixed formal language.

Here’s the hierarchy of these logical systems:

Propositional logic
This branch of logic is concerned with the study of propositions (whether they are True or False) that are formed by other propositions with the use of logical connectives.

The most basic logical connectives are AND $\land$ , OR $\lor$ , and NOT $\lnot$ .

The connectives are commutative. Here are their values (T stands for True, F for false):
$T \land T = T$ , everything else is F.
$F \lor F = F$ , everything else is T.
$\lnot F = T$ , $\lnot T = F$ .

We can also use variables to represent statements.

For example, we can say “a = Salad is organic”, and thus a is a True statement.
Another example is “a = Rock is organic”, and thus a is a False statement.
“a = Hi there!” is neither a True nor a False statement.

Propositional logic defines an argument to be a list of propositions. For example, given the two propositions $A \lor B, \lnot B$ we can conclude A.

An argument is valid iff for every row where the propositions are True, the conclusion is also True.

An easy way to check the validity of this argument is to use the definitions above and draw a table with all possible values of A and B.
```
A	B	A OR B	NOT B
F	F	F		T
F	T	T		F
T	F	T		T
T	T	T		F
```
In this case, the row where all of the propositions are true is 3. We see that the conclusion A is also True, so the argument is valid and will hold for any value we put in place of A or B.

Besides using tables to check for values, we can also construct proofs given a natural deduction system.

We can use the system’s rules to either prove or disprove a statement.
First-order logic
This logical system extends propositional logic by additionally covering predicates and quantifiers.

A predicate P(x) takes as an input x, and produces either True or False. For example, having “P(x) = x is a organic”, then P(Salad) is True, but P(Rock) is False.

Note that in set theory, P would be a subset of a relation, i.e. $P \subseteq A \times \{ True, False \}$ . When working with other systems we need to be careful, as this is not the case with FOL. In the case of FOL, we have P(Salad) = True, P(Rock) = False, etc as atomic statements (i.e. they cannot be broken down into smaller statements).

There are two quantifiers introduced: forall (universal quantifier) $\forall$ and exists (existential quantifier) $\exists$ .

In the following example the universal quantifier says that the predicate will hold for all possible choices of x: $\forall x P(x)$
In the following example the existential quantifier says that the predicate will hold for at least one choice of x: $\exists x P(x)$
Second-order logic, …, Higher-order (nth-order) logic
First-order logic quantifies only variables that range over individuals; second-order logic, in addition, also quantifies over sets; third-order logic also quantifies over sets of sets, and so on.

For example, Peano’s axioms (the system that defines natural numbers) are a mathematical concept expressed using a combination of first-order and second-order logic.

This concept consists of a set of axioms for the natural numbers, and all of them (except the ninth, induction axiom) are statements in first-order logic.

The base axioms can be augmented with arithmetical operations of addition, multiplication and the order relation, which can also be defined using first-order axioms.

The axiom of induction is in second-order, since it quantifies over predicates.

In my next post we’ll have a look at intuitionistic logic, a special logical system based on type theory.

Curry–Howard correspondence

For most of my schooling (basic school, high school), I’ve had a private math teacher thanks to my parents. I believe this has shaped my career path for the better.

I’ve always wanted to be a programmer, and I used to be interested in nothing else. Now I am lucky for the past years to be doing exactly what I’ve always wanted, and that is programming.

Back in basic school, I remember one thing that one of my math teachers kept reminding me: “Study math, it is very closely related to programming”. Now I think I really understand what that statement means.

In any case, I’ve recently started digging into Lean Theorem Prover by Microsoft Research. Having some Haskell experience, and experience with mathematical proofs, the tutorial is mostly easy to follow.

I don’t have much experience with type theory, but I do know some stuff about types from playing with Haskell. I’ve heard about the Curry-Howard correspondence a bunch of times, and it kind of made sense, but I haven’t really understood it in depth. So, by following the Lean tutorial, I got to get introduced to it.

An excerpt from Wikipedia:

In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.

In simpler words, a proof is a program, and the formula it proves is the type for the program.

Now as an example, consider your neat function of swapping 2 values of a product type:

swap :: (a, b) -> (b, a)
swap (a, b) = (b, a)

What the Curry-Howard correspondence says is that this has an equivalent form of a mathematical proof.

Although it may not be immediately obvious, think about the following proof:
Given P and Q, prove that Q and P.
What you do next is use and-introduction and and-elimination to prove this.

How does this proof relate to the swap code above? To answer that, we can now consider these theorems within Lean:

variables p q : Prop
theorem and_comm : p ∧ q → q ∧ p := fun hpq, and.intro (and.elim_right hpq) (and.elim_left hpq)

variables a b : Type
theorem swap (hab : prod a b) : (prod b a) := prod.mk hab.2 hab.1

Lean is so awesome it has this #check command that can tell us the complete types:

#check and_comm -- and_comm : ∀ (p q : Prop), p ∧ q → q ∧ p
#check swap     -- swap     : Π (a b : Type), a × b → b × a

Now the shapes are apparent.

We now see the following:

and.intro is equivalent to prod.mk (making a product)
and.elim_left is equivalent to the first element of the product type
and.elim_right is equivalent to the second element of the product type
forall is equivalent to the dependent type pi-type
A dependent type is a type whose definition depends on parameters. For example, consider the polymorphic type List a. This type depends on the value of a. So List Int is a well defined type, or List Bool is another example.

More formally, if we’re given A : Type and B : A -> Type, then B is a set of types over A.
That is, B contains all types B a for each a : A.
We denote it as Pi a : A, B a.

As a conclusion, it’s interesting how logical AND being commutative is isomorphic to a product type swap function, right? 🙂

Code checklist

Here is a checklist of some of the most important stuff (in my opinion) that should be ran through any code change, regardless of a programming language:

Does what it’s supposed to do
- Process it mentally (proof of correctness)
- Automated tests
- Manual tests
Can’t be further broken into smaller pieces
Is written in a generalized way (re-usage)
Has no repeating parts
My future-self and coworkers can understand it
- Is documented
- Is readable
Conforms to (any) coding standards for consistency
Separation of concerns

With experience, one doesn’t need to think about these, since they occur naturally.

There might be a couple of more that I missed, but these should be a good base.

Induction with Coq

To get ourselves introduced to the induction tactic, we’ll start by showing that 0 is a right identity for the naturals under addition, i.e. $\forall n \in \mathbb{N}, n + 0 = n$ .

The definition of addition is: $n = 0 + n, S(m) + n = S(m + n)$ .

Mathematically, we start with induction on n.

We have $0 + 0 = 0$ for the base case, which is true (based on definition of add).
For the inductive step, we assume that $n + 0 = n$ , and try to prove that $S n + 0 = S n$ .
We can rewrite our goal by using the definition of add, where we have $S n + 0 = S (n + 0)$ .
Now using the hypothesis we have $S (n + 0) = S n$ , which is what we needed to show.

Programmatically, we have:

Compute 2+3. (* Test to see what's 2 plus 3 *)

Theorem zero_identity_on_addition : (forall n:nat, n + 0 = n).
Proof.
  intros n.
  induction n.     (* Use induction on n *)
  (* Base case *)
    simpl.         (* Simplify 0 + 0 = 0 to 0 = 0 *)
    exact eq_refl. (* Which is exactly reflexivity *)
  (* Inductive step *)
  simpl.           (* At this point we have S n + 0 = S n, in other words n + 1 + 0 = n + 1 *)
                   (* Simplify to get (n + 0) + 1 = n + 1 *)
  rewrite IHn.     (* Use the hypothesis to rewrite (n + 0) to n *)
  exact eq_refl.   (* n + 1 = n + 1 is proven by reflexivity *)
Qed.

Neat, right?

Our second example is more complex. We will:
1. Define a recursive function, fact.
2. Prove that $fact(3) = 6$ .
3. Introduce and prove a lemma to be used for our proof.
4. Prove that $fact(n) > 0$ .

Mathematically:

$fact(n) = \left\{ \begin{array}{ll} 1 & \mbox{if } n = 0 \\ n * fact(n - 1) & \mbox otherwise \end{array} \right.$
To show what fact(3) is, we go by definitions: $3 * fact(2) = 3 * 2 * fact(1) = 3 * 2 * 1 * fact(0) = 6$ .
To prove $x > 0 \implies x + y > 0$ , which is the lemma we’ll use in our Coq proof, note we have as givens $x > 0, y \ge 0$ (since $y \in \mathbb{N}$ ).

From here, we have two cases:
$\begin{cases} y = 0: x + y = x + 0 = x > 0 \\ y > 0: x + y > 0 + x = x > 0 \end{cases}$

By transitivity on $(>, \mathbb{N})$ for the second case, combined with the first case, we can conclude that $x + y > 0$ .
To prove that $fact(n) > 0$ for $n \ge 0$ , we use induction on n.

Base case: $n = 0: fact(0) = 1 > 0$ , which is true.
Inductive step: Assume $fact(k) > 0$ for some $n = k$ . Note that $n \ge 0 \implies k + 1 > 0$ , so we’re good to multiply with a positive number.

Multiply both sides by k + 1 to get $(k + 1) * fact(k) = fact(k + 1) > 0$ , which is what we needed to show.

Thus $fact(n) > 0$ in general.

Now for the programming part.

The recursive definition:

(* If we try to use Definition, we get fact is not defined *)
(* Coq provides a special syntax Fixpoint for recursion *)
Fixpoint fact (n:nat) : nat :=
  match n with
    | S n => S n * fact n
    | 0 => 1
end.

Evaluate and prove $fact(3) = 6$

Compute (fact 3).
 
Theorem fact_3_eq_6 : (fact 3 = 6).
Proof.
  simpl.           (* Evaluate fact 3 = 6 *)
  exact eq_refl.   (* 6 = 6 is exactly reflexivity *)
Qed.

We start our lemma as follows:

Require Import Coq.Arith.Plus.

Lemma x_plus_y_gt_0 : (forall x y : nat, x > 0 -> x + y > 0).
Proof.
  intros x y.
  intros x_gt_0.
  unfold gt.           (* Convert x + y > 0 to 0 < x + y *) 
  unfold gt in x_gt_0. (* Convert x_gt_0 : x > 0 to x_gt_0 : 0 < x *)
  (* We have that Theorem lt_plus_trans n m p : n < m -> n < m + p *)
  (* So we feed 0, x, y to match the arguments, and additionally pass x_gt_0 to match the n < m part *)
  exact (lt_plus_trans 0 x y x_gt_0).
Qed.

Nothing new going on here. But, we can try to be smart, and try to rewrite the lemma as:

Require Import Omega.

Lemma x_plus_y_gt_0 : (forall x y : nat, x > 0 -> x + y > 0).
Proof.
  intros x y.
  omega.
Qed.

The new thing we can notice here is the usage of the omega tactic.

This tactic is an automatic decision procedure for Presburger arithmetic, i.e. it will solve any arithmetic-based proof goal that it understands (and that is true). But note e.g. that it doesn’t understand multiplication.

The actual proof

Theorem fact_gt_0 : (forall n : nat, fact n > 0).
Proof.
  intros n.
  induction n.
  (* Base case *)
    simpl.          (* At this point we have fact 0 > 0, simplify to get 1 > 0 *)
    exact (le_n 1). (* This is exactly 1 > 0 *)
  (* Inductive step *)
    simpl.          (* Simplify to convert fact(n + 1) > 0 to fact n + n * fact n > 0 *)
                    (* Which is exactly our lemma defined above *)
                    (* We also have IHn : fact n > 0 *)
    (* Feed (fact n), (n * fact n) into x_plus_y_gt_0, and IHn as well for the x > 0 part *)
    exact (x_plus_y_gt_0 (fact n) (n * fact n) IHn).
Qed.

Thus, the complete program:

Require Import Omega.

(* If we try to use Definition, we get fact is not defined *)
(* Coq provides a special syntax Fixpoint for recursion *)
Fixpoint fact (n:nat) : nat :=
  match n with
    | S n => S n * fact n
    | 0 => 1
end.

Compute (fact 3).

Theorem fact_3_eq_6 : (fact 3 = 6).
Proof.
  simpl.           (* Evaluate fact 3 = 6 *)
  exact eq_refl.   (* 6 = 6 is exactly reflexivity *)
Qed.

Lemma x_plus_y_gt_0 : (forall x y : nat, x > 0 -> x + y > 0).
Proof.
  intros x y.
  omega.
Qed.

Theorem fact_gt_0 : (forall n : nat, fact n > 0).
Proof.
  intros n.
  induction n.
  (* Base case *)
    simpl.          (* At this point we have fact 0 > 0, simplify to get 1 > 0 *)
    exact (le_n 1). (* This is exactly 1 > 0 *)
  (* Inductive step *)
    simpl.          (* Simplify to convert fact(n + 1) > 0 to fact n + n * fact n > 0 *)
                    (* Which is exactly our lemma defined above *)
                    (* We also have IHn : fact n > 0 *)
    (* Feed (fact n), (n * fact n) into x_plus_y_gt_0, and IHn as well for the x > 0 part *)
    exact (x_plus_y_gt_0 (fact n) (n * fact n) IHn).
Qed.

As a conclusion from the examples above, we can say that Coq with its type mechanism provides a neat way for us to reason about properties of our programs.

More proofs and tactics with Coq

If you look at the Tactics index, you will find many useful tactics to use in attempt to prove what you’re trying to prove.

One interesting example I’ve found is the auto tactic.

This tactic implements a Prolog-like resolution procedure to solve the current goal. So let’s try it and see how we can use it:

Goal (5 > 4).
  auto.       (* This magical command tries to prove stuff automatically *)
  Show Proof. (* And show us how it did it *)
Qed.

It’s proven 5 > 4 very easily, and with Show Proof we can additionally see how it did that. We see it used le_n 5, so now we can rewrite our proof:

Goal (5 > 4).
  exact (le_n 5).
Qed.

We could also dig into le_n to see what it actually does.

In our next example we’ll have a look at the case tactic (we’ve already used destruct before):

Require Import Bool.

Notation "x && y" := (andb x y).

Theorem x_and_true : (forall x : bool, x && true = x).
Proof.
  intros x.
  case x. (* Case analysis on x *)
  (* Handle the case where x is true *)
    simpl.       (* Simplify true && true *)
    reflexivity. (* true = true is proven by reflexivity *)
  (* Handle the case where x is false *)
    simpl.       (* Simplify false && true *)
    reflexivity. (* false = false is proven by reflexivity *)
Qed.

As you can see we’re relying on the Bool package and its function andb, but for simplicity we wrote an alias for it (&&) to use as infix operator.

We can check how Bool is defined, and if we do that we’ll see it has 2 options (true, false) and we’re ready to use case.

When we say case on something of type bool, it will go through the cases in order, so it starts with true, and once we prove that case it will proceed with false.

Our last (and most complex) example is where we introduce ourselves to the unfold tactic, and also rely on external proofs:

Require Import PeanoNat.

Theorem x_gte_5_x_gt_4 : (forall x : nat, x = 5 \/ x > 5 -> x > 4).
Proof.
  intros x.
  intros x_gte_5.
  case x_gte_5.
  (* Handle case x = 5 *)
    intros x_eq_5.  (* At this point we have x = 5 and x > 4 *)
    rewrite x_eq_5. (* Rewrite x > 4 with x = 5 to get 5 > 4 *)
    exact (le_n 5). (* Check le_n in Coq library, 5 > 4 is exactly that *)
  (* Handle case x > 5 *)
    (* Coq's ">" (gt) is defined in terms of "<" (lt), so we unfold to convert *)
    unfold gt.      (* At this point we have 5 < x -> 4 < x *)
    (* Check lt_succ_l in Coq library, 5 < m -> 4 < m is exactly that (which is why we used unfold) *)
    exact (Nat.lt_succ_l 4 x).
Qed.

In our next post we’ll be looking at the induction tactic, as well as some examples for it.