===== 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. [[http://en.wikipedia.org/wiki/Cut-elimination_theorem|Cut-elimination_theorem]].

=== Reference ===
Wikipedia: 
[[http://en.wikipedia.org/wiki/Proof_theory|Proof theory]],
[[http://en.wikipedia.org/wiki/Sequent_calculus|Sequent_calculus]],
[[http://en.wikipedia.org/wiki/Linear_logic|Linear logic]],
[[http://en.wikipedia.org/wiki/Cut-elimination_theorem|Cut-elimination_theorem]]

==== Parents ====
=== Related ===
[[Logic]]