Intuitionistic logic

According to Wikipedia:

In type theory, a system has inductive types if it has facilities for creating a new type along with constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

Let’s look at how Coq defines False/True and false/true (as per Mike Nahas’ tutorial) in terms of inductive types:

Inductive False : Prop := .

Inductive True : Prop :=
  | I : True.

Inductive bool : Set :=
  | true : bool
  | false : bool.

False/True are Prop(s), where False has no constructors (i.e. it is the bottom type for which no proof exists), and True has one constructor.
false/true are bool(s), where both of them are a constructor for bool.

Coq also has definitions for both Prop and bool, e.g. for comparison we use eq and eqb respectively.
The definitions of them are:

eq  : ?A -> ?A -> Prop where ?A : [ |- Type]
eqb : bool -> bool -> bool

But there are some fancy lemmas for converting some of them, e.g. one example is:

Nat.eqb_eq : forall n m : nat, (eqb n m) = true <-> (eq n m)

If we now take a look at the modus ponens theorem:
Theorem modus_ponens : (forall A B : Prop, A -> (A -> B) -> B).
We can clearly see that A and B are Prop(s), and not bool(s).

So even though there is some similarity between bool and Prop, they are fundamentally different. bool can be looked as either being true or false (and can also be computed a value for), and Prop as either provable or not (no computation). The logical system that depends on Prop at the fundamental level is called Intuitionistic logic, and the distinction from classical logic can be noticed easily.

This logic closely mirrors the notion of constructive proof, where for a proof we need to provide the actual object that satisfies it. As a result, the law of excluded middle (P or not P) is not defined in Intuitionistic logic. As we said, Prop cannot be true or false (i.e. doesn’t represent truth), rather True or False (i.e. represents the fact that we have a direct proof or not).

For a propostion x : Prop, a valid proof would be proof_x : x, that is an object of type x. To demonstrate what I mean by this, let’s see how a proof in Coq looks:

Inductive x : Prop.
Variable proof_x : x.

Theorem a_random_proof_exists : exists a, a.
Proof.
  exists x.
  exact proof_x.
Qed.

Inhabitants of Prop (e.g. x) are types whose inhabitants are proofs of logical statements (e.g. proof_x). Note that (a : b : c) means exactly the same as (a : b) and (b : c), that is a has a type of b, and b has a type of c. (proof_x : x : Prop) means that x is a logical proposition and proof_x is its proof. This is very close to BHK interpretation, where:

• A proof of P ∧ Q is a pair <a, b> where a is a proof of P and b is a proof of Q.
• A proof of P ∨ Q is a pair <a, b> where a is 0 and b is a proof of P, or a is 1 and b is a proof of Q.
• A proof of P → Q is a function f that converts a proof of P to a proof of Q.
• A proof of ∃x ∈ S : φ(x) is a pair <a, b> where a is an element of S, and b is a proof of φ(a).
• A proof of ∀x ∈ S : φ(x) is a function f that converts an element a of S into a proof of φ(a).
• The formula ¬P is defined as P → ⊥, so a proof of it is a function f that converts a proof of P into a proof of ⊥.
• There is no proof of ⊥.

If we try to print the definitions of “and” and “or” in Coq, here’s what we get:

Print and. (* Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B *)
Print or.  (* Inductive or (A B : Prop) : Prop :=  or_introl : A -> A \/ B | or_intror : B -> A \/ B *)

It’s the famous product and sum types, which line up well with the BHK interpretation above. But what about ->? Whoops, it’s just a notation:

Locate "->". (* Notation "A -> B" := forall _ : A, B : type_scope *)

This is a notation for non-dependent product, contrast to the case of (forall x : A, B) where x is a sub-term of B.

So all of this is fancy, we have types that can extend types. However, one might ask, why construct such a logical system?

Given this system, we know that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object (relation to Curry–Howard correspondence between proofs and algorithms). One reason that this particular aspect of intuitionistic logic is so valuable is that it enables the usage of proof assistants, i.e. Coq.

So, have fun and make sure your types match! 🙂