Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
proof_theory [2014/03/28 00:19] nikolaj |
proof_theory [2014/03/28 10:43] nikolaj |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| 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. | 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: | + | 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{}{\phi\vdash\phi}}(identity)$ ^ | ||
| ^ ${\large\frac{\Gamma,\Psi\vdash\vartheta}{\Gamma,\alpha,\Psi\vdash\vartheta}}(weaken)$ ^ | ^ ${\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,\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,\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)$ ^ | ||
| - | From a computational point of view, the cut rule has a little more going on: | + | 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]]. |
| - | + | ||
| - | ^ ${\large\frac{\Gamma\vdash\alpha\hspace{.5cm}\alpha,\Psi\vdash\vartheta}{\Gamma,\Psi\vdash\vartheta}}(cut)$ ^ | + | |
| === Reference === | === Reference === | ||
| Line 29: | Line 25: | ||
| [[http://en.wikipedia.org/wiki/Proof_theory|Proof theory]], | [[http://en.wikipedia.org/wiki/Proof_theory|Proof theory]], | ||
| [[http://en.wikipedia.org/wiki/Sequent_calculus|Sequent_calculus]], | [[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]] | [[http://en.wikipedia.org/wiki/Cut-elimination_theorem|Cut-elimination_theorem]] | ||
