This is an old revision of the document!
Proof theory
Meta
We can use logic to reason about logical derivations. The object language contains formulae $foo$, $bar$, etc. and we use
$foo\vdash bar$,
which one might reads as
“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. The rules are all pretty intuitive, here the simplest ones:
| ${\large\frac{}{\phi\vdash\phi}}(identity)$ |
|---|
| ${\large\frac{\Gamma,\Psi\vdash\vartheta}{\Gamma,\alpha,\Psi\vdash\vartheta}}(weaken)$ |
The second two are also easy to interpret, but it's worth pointing out that they give $\Gamma$ the property of a set over a list:
| ${\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)$ |
From a computational point of view, the cut rule has a little more going on:
| ${\large\frac{\Gamma\vdash\alpha\hspace{.5cm}\alpha,\Psi\vdash\vartheta}{\Gamma,\Psi\vdash\vartheta}}(cut)$ |
|---|
Reference
Wikipedia: Proof theory, Sequent_calculus, Cut-elimination_theorem
Parents
Related
