The Curry-Howard Correspondence 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 $\varphi$ for each premise $\varphi$, and vice versa. Essentially,

where a statement like ${\alpha }_1:{\varphi }_1$ says that ${\alpha }_1$ has type ${\varphi }_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 …

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.¹ 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 . 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 …

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:¹

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

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

System $B$:

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

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

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 …