5. From Nil to Nat: Logic

5.1. Propositions as types

We have seen that one can use inductive types to build a respectable model of the natural numbers. The next goal is to to see whether inductive types can likewise provide a computational model of logic.

Recall what we had to say before about the basic idea:

The first step is to associate with every mathematical proposition a type: The type of its proofs. In fact, Lean does not distinguish between a proposition and the type of its proofs. So 1+0=1 and 1+1=1 are types (remember that a proposition doesn't have to be true, just well-formed). Call a type inhabited if one can construct objects of that type, and empty else. Thus, in type-theory jargon, we don't say that "1+0=1 is provable", we say that "the type 1+0=1 is inhabited", and a proof would be a computation that produces an object of that type.

5.1.1. True and False

To warm up, let's construct a type that's inhabited by construction:

inductive mTrue : Prop where
 | intro : mTrue

mTrue : Prop#check mTrue -- `Type`
mTrue.intro : mTrue#check mTrue.intro -- `mTrue`

-- Lean's standard version
-- (For our implementation, use "m" prefix -- think "my")
True.intro : True#check True.intro

The type mTrue is inhabited because it has a constructor mTrue.intro that takes no arguments. We'll use mTrue as our model of an unconditionally true proposition.

Note the "Prop" in the definition of the inductive type, in the place where we wrote "Type" before. Types that represent propositions behave slightly different from types that represent other mathematical objects: We'll comment on the distinction later.

Conversely, this type is manifestly empty, i.e. unprovable, simply because it has no constructor

inductive mFalse : Prop

mFalse : Prop#check mFalse -- `Type`

We'll use mFalse to model an unconditionally false proposition.

5.1.2. Next steps

To do anything useful, we now have to (a) construct types that represent interesting propositions about the natural number, and (b) work out how to combine propositions using the standard connectives of mathematical logic. It turns out that (a) is more challenging -- in particular defining the concept of "equality" will require a surprising amount of thought! For this reason, we'll focus on (b) first.

5.2. Logical connectives

Assume we have convinced ourselves (via proofs, or axiomatically) that a collection p, q, r, ... of propositions is true. We can use the logical connectives ∧, ∨, →, ¬ of propositional logic, and later also the quantifiers ∃, ∀ of predicate logic to form new propositions. A deductive system is a collection of rules for forming new propositions out of existing ones. The most important property of a deductive system is soundness, which means that it "preserves truth" in the sense that if the initial propositions are all true, then the same holds for those derived by the deductive system. A sound rule would e.g. be "if p and q are true, you may deduce p ∧ q".

Remarks:

It's very boring. Boring is what you want in a deductive system!
Logicians use the turnstile symbol "⊢" to indicate that a collection of premises entails a conclusion, like so: "p, q ⊢ p ∧ q".

There's various ways of formalizing the deduction rules of classical logic -- but given that you made it to this point in your education, it seems fair to assume that you have a pretty good feeling for the intended meaning of the standard logical connectives, so we won't lay out a formal theory here.

In the remainder of this section, we will implement data types that provide a computational model of a sound deductive system. For example, given two propositions p, q, we will define a datatype And p q so that elements of that type can be constructed only if both p and q are proven. You should verify to your own satisfaction that all our constructions are sound.

The implementation will be guided by the BHK interpretation, previously outlined here.

We accept the possibility that our system will be conservative, i.e. that there are propositions provable in classical logic that we won't be able to prove.

Interestingly, the properties of the resulting logic have been studied abstractly before the computational point of view was developed. It is called intuitionist logic, and it is indeed a slightly weaker than classical logic. (That's the reason the BHK approach is called an interpretation -- it provided one for the previously known rules of intuitionist logic).

5.2.1. Conjunctions

A datatype that represents proofs of the conjunction p ∧ q of two propositions must be such that constructing an element of the type is possible only if there exists an element of type p and an element of type q. The following definition achieves this goal:

inductive mAnd (p q : Prop) : Prop
 | intro (hp : p) (hq : q) : mAnd p q

mAnd (p q : Prop) : Prop#check mAnd -- mAnd (p q : Prop) : Prop

The type mAnd takes parameters p and q, which are required to be of type Prop. That is to say, we have declared a type mAnd p q for every pair p, q of propositions. There is only one constructor, intro, and thus only one way to instantiate an object of type mAnd p q. The constructor takes two arguments: hp which is an object of type p and hq, an object of type q.

Based on what we know at this point, the only provable proposition we know is mTrue. Here's our first Lean-proven theorem: a proof of True ∧ True:

theorem true_and_true : mAnd mTrue mTrue :=
  mAnd.intro mTrue.intro mTrue.intro

Meta-theoretically, we can see that mAnd mTrue mFalse has no proof (because it would require an object hq of type mFalse, which doesn't exist). Below, we'll see how to positively express that a proposition is false within the system.

Exercise

Now we know a second true proposition! Use it to prove (True ∧ True) ∧ True

5.2.2. Implications

For two propositions p, q, we model the proposition that says that p implies q as the type of functions p → q, i.e. functions that turn proofs of p into proofs of q. Nowhere else is the computational mindset so obvious: A theorem is an algorithm for computing the conclusion from the premises. It is also plausible (and indeed true) that requiring a concrete algorithm means that fewer theorems are provable than in a system where all we require to conclude p → q is that q is true whenever p is.

Let's prove the implication p ∧ q → p. To this end, we'll have to write a function that takes an argument of type mAnd p q and returns an element of type p. Because mAnd is just an inductive type, we can define functions from it using pattern matching on its constructor intro. The same way we computed the predecessor of a natural number that was constructed using nat.succ k -- namely by returning its argument k -- we now take the first parameter (a proof of p) off of intro:

open mAnd

theorem p_of_p_and_q (p q : Prop) : (mAnd p q) → p :=
  fun hpq ↦
    match hpq with
    | intro hp hq => hp

Remarks:

We have followed Lean's convention of using "h" as in "hypothesis" as the first letter for the name of variables holding proofs of assumptions.
The function p_of_p_and_q actually takes three arguments: The proposition p, the proposition q, and the hypothesis hpq. Note that the type mAnd p q of the third argument depends on the values p, q of the first two arguments. Such dependent types, absent from more standard programming languages, are used extensively in Lean. There are various equivalent ways of declaring the function type:

theorem p_of_p_and_q' (p q : Prop) (hpq : mAnd p q) : p :=
  match hpq with | intro hp hq => hp

-- Only anonymous parameters
theorem p_of_p_and_q'' :
  (p : Prop) → (q : Prop) → (mAnd p q) → p :=
  fun p q hpq ↦ match hpq with | intro hp hq => hp

The first two parameters are strictly speaking redundant. Since every term in Lean is explicitly typed, Lean can infer p and q when it sees an argument hpq of type mAnd p q. Arguments listed before the colon in curly braces are implicit: Lean will attempt to infer them from the context:

theorem p_of_p_and_q''' {p q : Prop} : (mAnd p q) → p :=
  fun hpq ↦ match hpq with | intro hp hq => hp

def TrueAndTrue := mAnd.intro mTrue.intro mTrue.intro

TrueAndTrue : mAnd mTrue mTrue#check TrueAndTrue
p_of_p_and_q''' TrueAndTrue : mTrue#check p_of_p_and_q''' TrueAndTrue
-- Use `@` to supply implicit parameters explicitly
p_of_p_and_q''' TrueAndTrue : mTrue#check @p_of_p_and_q''' mTrue mTrue TrueAndTrue

Exercise

Prove p → p ∧ p.
Prove p → (q → (p ∧ q)). Hint: Curry.

5.2.3. Disjunctions

We take the datatype that represents proofs of the disjunction p ∨ q of two propositions to be such that constructing an element of the type is possible only if one supplies an element of type p or an element of type q. We'll model this using two constructors, one for each case:

inductive mOr (p q : Prop) : Prop
 | inl (hp : p) : mOr p q -- "intro left"
 | inr (hq : q) : mOr p q -- "intro right"

open mOr

theorem true_or_false : mOr mTrue mFalse :=
  inl mTrue.intro

theorem and_of_or (p q : Prop) : (mAnd p q) → mOr p q :=
  fun hand ↦ match hand with
    | intro hp hq => mOr.inl hp

5.3. Negations

There are propositions, like true ∧ false, for which we can see from the outside that it won't be possible to construct a proof. We'd like to prove within the system that they are false.

To this end, we need to associate with every proposition p a datatype ¬p so that constructing an object of type ¬p is possible only if p is wrong.

It might not be obvious how to achieve this. If you scour through classical logic texts, you'll find that negations can be reduced to implications via the tautology ¬p ↔ (p → false). With this in mind, let's define ¬p to be the type of functions that turn proofs of p into proofs of false:

def mNeg (p : Prop) : Prop := p → mFalse

If you already believe (which you should at this point!) that the computational interpretation of implication is sound, then mNeg will obviously be sound, too. That is, it will be possible to write a function of type p → mFalse only if p actually is false. On the other hand, one might suspect that this model of negation is quite conservative: How should one write a function that constructs a proof of a syntactically unprovable statement?? Short answer: It's possible surprisingly often, see below. Longer answer: It often is quite difficult! Proving ¬(1=0) will be among the more challenging problems we'll face. And yes, the construction is conservative relative to classical logic, as we'll see next.

The construction in action:

theorem neg_true_and_false :
    mNeg (mAnd mTrue mFalse) := fun h =>
  match h with
  | intro ht hf => hf

In words: The type of the theorem is mNeg (mAnd mTrue mFalse), which δ-reduces to (mAnd mTrue mFalse) → mFalse: We have stated our intention of defining a function from proofs of mAnd mTrue mFalse to proofs of mFalse. This is done via the well-trodden path of pattern matching (exactly replicating the proof of (p ∧ q) → q from the Exercises): Should our function ever be called, then someone must have built its argument h, which is of type mAnd mTrue mFalse. But objects of this type can only be created using intro ht hf, where in particular, hf is an object of type mFalse. So we might just grab hf and return it.

Confused? Here's a soothing smiley to calm you down: 😌. (Or two: 😌 😌).

Exercise

(Very cute) Prove the no contradiction principle: ¬(p ∧ ¬p).
Prove (¬p ∨ ¬q) → ¬(p ∧ q), one of the implications of de Morgan's laws. (Hint: The theorem will be function-valued).
(This will be important in the next section). Prove double negation introduction p → ¬¬p ("assuming p, it is contradictory to assume ¬p").

5.3.1. Law of the excluded middle

Recall our discussion of the law of the excluded middle (LEM), a tautology of classical logic, which says that for every proposition p, the disjunction p ∨ ¬p is true. In our model, the only way to prove a disjunction is to call the inl or the inr constructor of mOr. For this, we'd have to know whether p or ¬p is true. But in general, there's no computational way to decide this, This follows from these three facts: (1) (Arithmetization) For every Turing machine M, there exists a formula p in the first-order logic of the natural numbers, such that p is true if and only if M halts. Hence, deciding arithmetic truths is at least as difficult as deciding the halting problem. (2) No TM can solve the halting problem. (3) (Church-Turing Hypothesis) Any process that can be reasonably described as a "computation" can be emulated by a TM. and thus ∀ p, p ∨ ¬p is not constructively provable.

...that's actually big news! The LEM is not exactly an obscure move in mathematical reasoning. It turns out that the situation can be understood better by thinking about double negations.

5.3.2. Double negation elimination

In the exercises above, we've showed that whenever we can prove a proposition p, we can also prove ¬¬p. Hence the double negation cannot be a stronger claim than p, but might potentially be weaker! And in fact, while the LEM does not hold constructively, the double negation ∀ p, ¬¬(p ∨ ¬p) is provable. We can draw two conclusions from this:

The LEM "almost holds" constructively, in the sense that it is contradictory to assume it is false.
Double negation elimination, i.e. the deduction rule ¬¬p → p, is also not valid constructively (for if we had DNE, we could prove the LEM from its double negation).

Exercise. Prove ¬¬(p ∨ ¬p). This is a bit harder than our previous results. For this reason, we'll use the built-in Lean logical functions, which use standard mathematical notation and are thus easier to read (but we won't use any library results, so you can also implement the same argument for our mNeg and mOr data types).

Replace the sorry block by proofs of the two lemmas orImplLeft and orImplRight sketched below. They say, respectively, that if (p ∨ q) implies r, then p implies r and q implies r.

theorem declaration uses 'sorry'orImpLeft {p q r : Prop} : ((p ∨ q) → r) → (p → r) := sorry

theorem declaration uses 'sorry'orImpRight {p q r : Prop} : ((p ∨ q) → r) → (q → r) := sorry

Note the curly braces around the named parameters p q r, which tell the Lean elaborator to try to auto-fill these parameters when the theorem is invoked.

Note that ¬(p ∨ ¬p) means (p ∨ ¬p) → ⊥ (⊥ is logician-speak for false). Thus, from h : ¬(p ∨ ¬p), by orImpLeft, we have p → ⊥, or ¬p; and by orImpRight, we have ¬p → ⊥. Combine those to prove

theorem declaration uses 'sorry'neg_neg_lem (p : Prop) : ¬¬(p ∨ ¬p) := sorry

5.3.3. Axioms

The fact that ∀ p, ¬¬(p ∨ ¬p) is provable points to a pragmatic solution for handling the lack of the LEM in constructivist logic: Just postulate it! Pretending that there is a proof of p ∨ ¬p won't lead to an outright contraction, because, if the system was consistent before, the negation of our axiom isn't provable.

Lean's facility for adding axioms is the axiom keyword

axiom lem {p : Prop} : p ∨ ¬ p

The object lem has a type, but no term associated with it (because, of course, there does not exist a term of that type!). Internally, it has the same effect as using sorry as the definition, but the keyword axiom tells the linter that, yes, we do mean it, and there's no need to bother us with warnings.

Axioms are invoked as if they were proof terms:

theorem false_or_neg_false : False ∨ ¬False := lem

Of course, there's no computational content to back up lem. Using #reduce just reproduces the name of the axiom

lem#reduce(proofs:=true) false_or_neg_false
-- lem

Conceptually, what has just happened? The original intuitionists set out to purge non-constructible objects from mathematics. BKH found a computational model that could implement this program. However, in the framework of the Curry-Howard correspondence, we won't actually run the algorithms that represent proofs -- we just use the fact that they exist to conclude that the corresponding type is populated. And if we won't run the programs anyways, it becomes possible again to add axioms, a list of statements which the type checker is told to accept even without a program backing them. Why bother then? My feeling (as a newcomer to the field) is that the answer is "Why not?". There might no longer be a fundamental reason for using type theory as the foundation for formalizing mathematics. The fights of the early 20th century have died down -- non-constructive arguments might sometimes feel a bit unsatisfactory, but few would claim today that they are unsound. But still, experience over the past decades seems to have shown that type theory is well-suited as a framework for formal mathematics. (And who knows? Maybe it's a fashion and the pendulum will swing back at some point.)

Remark:

You can use #print axioms to get a list of axioms that were used in the definition of a term

#print axioms false_or_neg_false
-- depends on axioms: [lem]

5.3.4. The principle of explosion

Above, we have shown that DNE implies the LEM. The converse is also true, the two principles are thus equivalent. A proof in Lean requires another reasoning principle: The principle of explosion, or ex falso quodlibet.

To explain what this is about, recall that a proof of an implication p → q is a function turning proofs of p to proofs of q. How shall we handle the edge case where p is the unprovable definition false? Since there are no elements of type false, the domain of such a function would be empty.

In the usual set-theoretic model of functions, one associates with any set S the empty function. It has domain ∅ (the empty set), codomain S, and graph ∅.

So it would match mathematical precedence if we agreed that for every p, the empty function is a legitimate element of the type false → p. This would make the implication false → p true under our interpretation of propositions as types. Of course, "precedence" is not a decisive argument: We have to convince ourselves that this convention is logically sound. But... it is. Since there is no argument of type false, there's no way to invoke the empty function, and thus no wrong statement can be constructed this way.

The deduction of an arbitrary proposition from a contradiction is called the Principle of explosion in logic.

The remaining question is how to syntactically define an empty function. Recall that the recursor of a type takes one parameter of every constructor, and returns a function defined on the type. For types with no constructors, the recursor takes no arguments, and implements the empty function:

theorem exfalso {p : Prop} : False → p := False.rec

We can now derive ¬¬p → p using the axiom lem and the theorem exfalso:

theorem dne (p : Prop) : ¬¬p → p := fun h_neg_neg_p =>
  match @lem p with
    | Or.inl hp => hp
    | Or.inr h_neg_p => exfalso (h_neg_neg_p h_neg_p)

Remark: Note the @ in front of lem? We have declared the argument p : Prop for lem as implicit, by putting it in curly braces. In most cases, Lean is able to guess p correctly from context -- but here it isn't, and we have to supply it manually. The @ turns off implicit parameters.

5.3.5. Proofs by contradiction

TBD, but here's a good read.