Proof theory


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:


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.



Link to graph
Log In
Improvements of the human condition