Visualizing Curry-Howard Correspondence

A tutorial on finding programs of proofs.

The Curry-Howard Correspondence external link says that types of terms (programs) corresponds to theorems of some logic, and the programs corresponds to the proofs of the theorems. So when a proposition $\psi$ can be proven from a set of premises, then there is derivation of some term with type $\psi$ from a typing context, where the typing context contains a term of type $\phi$ for each premise $\phi$, and vice versa. Essentially,

\[ \begin{gather*} \phi_1, \phi_2, \dots, \phi_n \tf \psi\\ \text{ iff }\\ \alpha_1 : \phi_1, \alpha_2 : \phi_2, \dots, \alpha_n : \phi_n \tf \beta : \psi \end{gather*} \]

where a statement like $\alpha_1 : \phi_1$ says that $\alpha_1$ has type $\phi_1$.

Here, we will concern ourselves with intuitionist (propositional) logic and an equivalent type system, namely a type system with function types, product types, and sum types. Then, we will show some proofs to see, in …

...

Callcc and Classical Logic

I couldn’t find a simple written explanation of callcc, its type, and the connection to classical logic, so I thought I’d write one here.1 I won’t assume that you are familiar with the syntax of Scheme (because I’m not), so I will be using a made up language. I hope the first part of this post will be self-contained, so that you don’t have to understand any particular langauge to understand callcc. The second part concerns how the type of callcc relates to classical logic under Curry-Howard Correspondence external link . I will assume some familiarity and comfort with the concept and type theory notations.

Prelude: Syntax

The syntax we use here is close to functional programming languages like ML.

  • Everything is an expression, so has a value.
  • Function definition: A function that takes input x and return z is written as (fn x => z). All functions take only one argument. Besides …
...

Deductions in Hilbert Systems

Hilbert systems are systems of deduction based on a large set of axioms and a minimal set of inference rules. Since deductions in Hilbert systems can be very hard to come up with, I will discuss some tips and tricks that I learned when I tried to solve this problem in Troelstra’s Basic Proof Theory:1

Prove that the following two sets of axioms are equivalent.2
System $A$:

  1. $P \to (Q \to P)$
  2. $(P \to Q \to R) \to (P \to Q) \to (P \to R)$

System $B$:

  1. $A \to (B \to A)$ (identical to 1)
  2. $(A \to A \to B) \to (A \to B)$ (Contraction)
  3. $(A \to B) \to (C \to A) \to (C \to B)$ (Pseudo-Transitivity)3
  4. $(A \to B \to C) \to (B \to A \to C)$ (Permutation)

The only inference rules available are Modus Ponens external link (MP; also called $\to$-Elimination).4

Note that here, we use the convention that $\to$ is right associative, meaning

$A \to B \to C \equiv (A \to (B \to C))$.

We may drop or add parenthesis so long …

...