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$,
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:
| ${\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.
Reference
Wikipedia: Proof theory, Sequent_calculus, Linear logic, Cut-elimination_theorem
Parents
Related
