Proof theory

Framework

We can use logic to reason about logical derivations. The object language contains formulae $foo$, $bar$, etc. and we use

$foo\vdash bar$,

“if $foo$ is provable, then $bar$ also provable.”

In the proof theoretic logic, we use a variable which represents a collection of object language formulae, called context, and generally denoted $\Gamma$. Moreover, we then must deal with several notion of “and”: We possibly have a notion of conjunction in the object language (generally written $\land$), but we also need two conjunctions in the meta language: A gap in the top line denotes a conjunction of premises as introduces in Logic, and a comma between formulae denotes a conjunction which arises from such a gap in a rule of the object language.

There are dozens of proof theories, but in the following we present some rules of a traditional one:

${\large\frac{}{\phi\vdash\phi}}(identity)$
${\large\frac{\Gamma,\Psi\vdash\vartheta}{\Gamma,\alpha,\Psi\vdash\vartheta}}(weaken)$
${\large\frac{\Gamma,\alpha,\alpha,\Psi\vdash\vartheta}{\Gamma,\alpha,\Psi\vdash\vartheta}}(contract)$
${\large\frac{\Gamma,\alpha,\beta,\Psi\vdash\vartheta}{\Gamma,\beta,\alpha,\Psi\vdash\vartheta}}(exchange)$
${\large\frac{\Gamma\vdash\alpha\hspace{.5cm}\alpha,\Psi\vdash\vartheta}{\Gamma,\Psi\vdash\vartheta}}(cut)$

It's worth pointing out that $contract$ and $exchange$ last two rules give $\Gamma$ the property of a set over a list. The rules $contract$ and $weaken$ are modified in Linear logic, which, roughly speaking, considers arguments to be a bounded resource. It has applications in programming. From a computational point of view, the $cut$ rule has a little more going on and is focal point of interesting theorems about proof theory, see e.g. Cut-elimination_theorem.