Proof theory
Framework
We can use logic to reason about logical derivations. The object language contains formulae foo, bar, etc. and we use
foo⊢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 Γ. Moreover, we then must deal with several notion of “and”: We possibly have a notion of conjunction in the object language (generally written ∧), 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:
| ϕ⊢ϕ(identity) |
|---|
| Γ,Ψ⊢ϑΓ,α,Ψ⊢ϑ(weaken) |
| Γ,α,α,Ψ⊢ϑΓ,α,Ψ⊢ϑ(contract) |
| Γ,α,β,Ψ⊢ϑΓ,β,α,Ψ⊢ϑ(exchange) |
| Γ⊢αα,Ψ⊢ϑΓ,Ψ⊢ϑ(cut) |
It's worth pointing out that contract and exchange last two rules give Γ 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
