Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
proof_theory [2014/03/28 10:42] nikolaj |
proof_theory [2014/11/11 11:13] nikolaj |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Proof theory ===== | ===== Proof theory ===== | ||
| - | ==== Meta ==== | + | ==== Framework ==== |
| We can use logic to reason about logical derivations. The object language contains formulae $foo$, $bar$, etc. and we use | We can use logic to reason about logical derivations. The object language contains formulae $foo$, $bar$, etc. and we use | ||
| 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 simple to interpret, proof theoretically | + | 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)$ ^ | ||
