Constructive Logic | Hype For Types

Proofs That Carry Evidence

Consider the claim:

There exist irrational numbers $a$ and $b$ such that $a^b$ is rational.

A familiar classical proof considers $x=(\sqrt2)^{\sqrt2}$. If $x$ is rational, choose $a=b=\sqrt2$. If $x$ is irrational, choose $a=x$ and $b=\sqrt2$; then

$$a^b=\left((\sqrt2)^{\sqrt2}\right)^{\sqrt2}=2.$$

This is a valid classical proof, but it does not tell us which pair to use unless we can decide whether $x$ is rational. The proof relies on the law of excluded middle, $P\vee\neg P$, where $P$ means “$x$ is rational.”

In constructive logic, a proof that something exists should provide an example. Here is one:

$$a=\sqrt2,\qquad b=\log_2 9,\qquad a^b=3.$$

Checking that $\sqrt2$ and $\log_2 9$ are irrational is left as an exercise. Their power is easy to calculate:

$$\begin{aligned} (\sqrt2)^{\log_2 9} &=(2^{1/2})^{\log_2 9}\\ &=2^{(\log_2 9)/2}\\ &=\sqrt{2^{\log_2 9}}\\ &=\sqrt9=3. \end{aligned}$$

Unlike the classical argument, this proof gives us one specific pair of witnesses.

Constructive does not mean “without cases.” We may eliminate a proof of $P\vee Q$ by considering both cases. What constructive logic does not provide automatically is a proof of $P\vee\neg P$ for every proposition $P$.

This view of proofs is useful because constructive proofs behave like algorithms. A proof of an existential returns a witness, a proof of a conjunction returns a pair, and a proof of an implication transforms one piece of evidence into another.

Judgments and Natural Deduction

The judgment $\Gamma\vdash A$ means that $A$ follows from the assumptions listed in $\Gamma$. Natural deduction gives each logical connective two kinds of rules. Introduction rules explain how to prove a statement that uses the connective. Elimination rules explain how to use such a proof.

Conjunction

$$\frac{\Gamma\vdash A\qquad\Gamma\vdash B}{\Gamma\vdash A\wedge B}\;\wedge I \qquad \frac{\Gamma\vdash A\wedge B}{\Gamma\vdash A}\;\wedge E_1 \qquad \frac{\Gamma\vdash A\wedge B}{\Gamma\vdash B}\;\wedge E_2$$

To prove a conjunction, provide both parts. To use it, project either part.

Implication

$$\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}\;\to I \qquad \frac{\Gamma\vdash A\to B\qquad\Gamma\vdash A}{\Gamma\vdash B}\;\to E$$

To prove $A\to B$, temporarily assume $A$ and use that assumption to prove $B$. The assumption is then discharged. To use a proof of $A\to B$, supply a proof of $A$; this is modus ponens.

Disjunction

$$\frac{\Gamma\vdash A}{\Gamma\vdash A\vee B}\;\vee I_1 \qquad \frac{\Gamma\vdash B}{\Gamma\vdash A\vee B}\;\vee I_2$$ $$\frac{\Gamma\vdash A\vee B\qquad\Gamma,A\vdash C\qquad\Gamma,B\vdash C}{\Gamma\vdash C}\;\vee E$$

A proof of $A\vee B$ records which side is true and includes evidence for that side. To use it, consider both possibilities and show that each leads to the same conclusion $C$.

Truth and falsehood

$$\frac{}{\Gamma\vdash\top}\;\top I \qquad \frac{\Gamma\vdash\bot}{\Gamma\vdash A}\;\bot E$$

Truth has a trivial proof. Falsehood has no introduction rule because there is no way to construct a proof of it. If inconsistent assumptions nevertheless let us derive falsehood, $\bot E$ allows us to conclude anything. This is the principle of explosion.

Negation

$$\neg A\;\overset{\mathrm{def}}{=}\;A\to\bot.$$

A proof of $\neg A$ is therefore a procedure that turns any proposed proof of $A$ into a contradiction.

What Constructive Logic Withholds

Intuitionistic logic does not accept either of the following schemas without further evidence:

$$A\vee\neg A\qquad\text{and}\qquad\neg\neg A\to A.$$

Double-negation elimination shows why. Expanding the definition gives

$$\neg\neg A=(A\to\bot)\to\bot.$$

This says that assuming $\neg A$ leads to a contradiction. It still does not give us a proof of $A$. We can, however, prove the other direction: $A\to\neg\neg A$.

Show a proof of $A\to\neg\neg A$

Assume $A$. Our goal is $\neg\neg A$. By the definition of negation, this goal expands to

$$\neg\neg A\equiv\neg A\to\bot\equiv(A\to\bot)\to\bot.$$

We therefore assume $A\to\bot$.:

$$\frac{ \overline{A,A\to\bot\vdash A\to\bot}^{\mathrm{assumption}} \qquad \overline{A,A\to\bot\vdash A}^{\mathrm{assumption}} }{ A,A\to\bot\vdash\bot }\;\to E$$

Next, discharge the assumption $A\to\bot$. Implication introduction gives $(A\to\bot)\to\bot$, which is the definition of $\neg\neg A$:

$$\frac{ A,A\to\bot\vdash\bot }{ A\vdash(A\to\bot)\to\bot }\;\to I$$ $$A\vdash(A\to\bot)\to\bot\equiv A\vdash\neg\neg A.$$

Finally, discharge the original assumption $A$:

$$\frac{ A\vdash\neg\neg A }{ \vdash A\to\neg\neg A }\;\to I$$

Every implication used by $\to E$ now appears explicitly as a premise.

We can recover classical logic by adding a principle such as excluded middle or double-negation elimination. Constructive logic simply does not include either principle by default.

Curry–Howard: Propositions as Types

The Curry–Howard correspondence connects logic with programming. Propositions correspond to types, and proofs correspond to programs of those types. The judgment $\Gamma\vdash p:A$ can therefore be read in two ways: “$p$ is a proof of $A$” or “program $p$ has type $A$.”

Logic	Type theory	Evidence
$A\wedge B$	$A\times B$	a pair $(a,b)$
$A\vee B$	$A+B$	`Left a` or `Right b`
$A\to B$	$A\to B$	a function mapping proofs of $A$ to proofs of $B$
$\top$	`unit`	the sole value $\langle\rangle$
$\bot$	`void`	no canonical value

For example, implication introduction is exactly function abstraction:

$$\frac{\Gamma,x:A\vdash e:B}{\Gamma\vdash(\lambda x:A.e):A\to B}.$$

Implication elimination is application. Conjunction introduction builds a pair, conjunction elimination projects from it, and disjunction elimination is case analysis.

Harmony. Introduction rules tell us what evidence for a connective looks like. Elimination rules let us use exactly that evidence. Beta-reduction simplifies a proof that introduces a connective and immediately eliminates it. Eta-expansion says that we can take a proof apart using its elimination rules and rebuild it using its introduction rules.

Proofs as Programs

We can prove each proposition below by writing a program with the corresponding type. Expand a solution to see the program and the idea behind it.

$A\to A$

Show solution

fn a : A => a

The identity function transforms any proof of $A$ into the same proof of $A$.

$(A\wedge B)\to A$

Show solution

fn (a, b) : A * B => a

A proof of a conjunction is a pair; return its first component.

$((A\wedge B)\to C)\to(A\to(B\to C))$

Show solution

fn f : (A * B) -> C =>
  fn a : A =>
    fn b : B =>
      f (a, b)

The input function expects a pair. Our new function accepts the two parts one at a time, puts them into a pair, and passes that pair to the original function. This transformation is called currying.

$\bot\vee\top$

Show solution

Right <>

The unit value $\langle\rangle$ proves $\top$, so the right injection proves the disjunction.

$A\wedge(B\vee C)\leftrightarrow(A\wedge B)\vee(A\wedge C)$

Show both directions

Read $P\leftrightarrow Q$ as the pair $(P\to Q)\wedge(Q\to P)$.

fn (a, choice) =>
  case choice of
      Left b  => Left (a, b)
    | Right c => Right (a, c)

fn choice =>
  case choice of
      Left (a, b)  => (a, Left b)
    | Right (a, c) => (a, Right c)

In each direction, case analysis preserves the tag that identifies which disjunct was proved.

$(A\wedge\neg A)\to B$

Show solution

fn (a, notA) =>
  absurd (notA a)

Applying notA : A -> void to a : A produces falsehood. The eliminator absurd : void -> B then yields $B$.

$(A\to B)\to(\neg B\to\neg A)$

Show solution

fn f : A -> B =>
  fn notB : B -> void =>
    fn a : A =>
      notB (f a)

This is constructive contraposition. Notice that the converse, $(\neg B\to\neg A)\to(A\to B)$, is not generally constructively valid.

Dependent Evidence: Even Squares

Constructive proofs become even more expressive when types can mention values. We will see this more in depth later, but to get a taste of it, define

$$\operatorname{Even}(n)\;=\;\sum_{k:\mathbb N}(n=2k).$$

A proof of $\operatorname{Even}(n)$ is a pair $(k,p)$. The number $k$ is the witness, and $p$ proves that $n=2k$. We will use the following facts about equality and multiplication:

$$\begin{aligned} \operatorname{sym}&:(x=y)\to(y=x),\\ \operatorname{cong}&:(f:X\to Y)\to(x=y)\to(f(x)=f(y)),\\ \operatorname{trans}&:(x=y)\to(y=z)\to(x=z),\\ \operatorname{assoc}(a,b,c)&:(ab)c=a(bc),\\ \operatorname{comm}(a,b)&:ab=ba. \end{aligned}$$

The theorem “if $n$ is even, then $n^2$ is even” becomes the function type

$$\operatorname{Even}(n)\to\operatorname{Even}(n^2).$$

Show the complete constructive proof

Assume $(k,p):\operatorname{Even}(n)$, so $p:n=2k$. Choose $m=2(k k)$ as the witness for the evenness of $n^2$. Congruence first gives

$$p_1=\operatorname{cong}(\lambda x.x x,p):n n=(2k)(2k).$$

The remaining arithmetic equality is:

$$\begin{aligned} (2k)(2k) &=((2k)2)k &&\text{associativity}\\ &=(2(k2))k &&\text{associativity}\\ &=(2(2k))k &&\text{commutativity of }k2\\ &=2((2k)k) &&\text{associativity}\\ &=2(2(kk)) &&\text{associativity.} \end{aligned}$$

Call this chain of equalities $p_2:(2k)(2k)=2(2(kk))$. Combining $p_1$ and $p_2$ gives a proof that $n n=2m$. This is exactly what we need to show that $n^2$ is even.

We can now write every arithmetic step as an equality proof. The comment beside each line gives its type:

fn (k, p) : Even(n) =>
  let
    m = 2 * (k * k)

    p1 =
      cong (fn x => x * x) p
      -- p1 : n*n = (2*k)*(2*k)

    q1 =
      sym (assoc (2*k) 2 k)
      -- q1 : (2*k)*(2*k) = ((2*k)*2)*k

    q2 =
      cong (fn x => x*k) (assoc 2 k 2)
      -- q2 : ((2*k)*2)*k = (2*(k*2))*k

    q3 =
      cong (fn x => (2*x)*k) (comm k 2)
      -- q3 : (2*(k*2))*k = (2*(2*k))*k

    q4 =
      assoc 2 (2*k) k
      -- q4 : (2*(2*k))*k = 2*((2*k)*k)

    q5 =
      cong (fn x => 2*x) (assoc 2 k k)
      -- q5 : 2*((2*k)*k) = 2*(2*(k*k))

    p2 =
      trans q1 (trans q2 (trans q3 (trans q4 q5)))
      -- p2 : (2*k)*(2*k) = 2*(2*(k*k))

    result =
      trans p1 p2
      -- result : n*n = 2*m
  in
    (m, result)

The returned pair has type $\operatorname{Even}(n^2)$. Its first component is the witness $m=2k^2$, and its second component proves $n^2=2m$. The code is intentionally a little dense: it gives a preview of how one function can both compute a new witness and construct a proof that the witness is correct.

Don't worry about it if the above is confusing, we will return to these ideas in later notes.

This proof gives us more than a yes-or-no answer. Given a witness $k$ for the evenness of $n$, it computes the new witness $2k^2$ for the evenness of $n^2$ and produces a proof that the witness is correct.

Why Constructivity Matters

In constructive logic, the form of a statement tells us what evidence for it must contain:

A proof of $A\wedge B$ contains both components.
A proof of $A\vee B$ records a choice and the evidence supporting it.
A proof of $A\to B$ is a transformation from evidence for $A$ to evidence for $B$.
A proof of $\exists x.\,P(x)$ contains a witness $x$ together with a proof of $P(x)$.
A proof of $\forall x.\,P(x)$ is a procedure producing evidence for every input $x$.

This is why type checking can also serve as proof checking. If a trusted type checker confirms that a program has a proposition as its type, that program is a mechanically checkable proof.

Functions are proofs (and values)

This does not mean that every program is automatically an interesting proof. The type must accurately express the theorem we intend to prove, and the type theory itself must be consistent. Once those pieces are in place, programming and proving become two ways to view the same construction.

References

Pfenning, Frank. 2017. “Overview.” 15-317 Constructive Logic, Carnegie Mellon University. Lecture 1 notes (PDF).
Pfenning, Frank. 2017. “Natural Deduction.” 15-317 Constructive Logic, Carnegie Mellon University. Lecture 2 notes (PDF).
Pfenning, Frank. 2017. “Harmony.” 15-317 Constructive Logic, Carnegie Mellon University. Lecture 4 notes (PDF).
Howard, William A. 1980. “The Formulae-as-Types Notion of Construction.” In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 479–490.
Martin-Löf, Per. 1984. Intuitionistic Type Theory. Bibliopolis.