A proof theory involves the following concepts:
- An axiom system, consisting of:
- a set of formulas, called axioms,
- a set of relations between formulas, called inference rules.
If $R$ is an inference rule and if $\langle X_1,\ldots,X_n,Y\rangle\in R$, the $Y$ is a direct consequence of $X_1,\ldots,X_n$ under $R$.
- A proof is a finite sequence $A_1\ldots A_n$ of formulas s.t. for each $A_i$ $(1\leq i\leq n)$:
- $A_i$ is an axiom, or
- $A_i$ is a direct consequence of earlier elements in the sequence under some inference rule.
- A formula $A$ is provable, symbolically $\vdash A$, iff there is a proof $A_1\ldots A_n$ s.t. $A_n=A$ holds.
- A derivation from a theory $T$ is a finite sequence $A_1,\ldots,A_n$ of formulas s.t. for each $A_i$ $(1\leq i\leq n)$:
- $A_i\in T$ or
- $A_i$ is an axiom, or
- $A_i$ is a direct consequence of earlier elements in the sequence under some inference rule.
- A (closed) formula $A$ is derivable from a theory $T$, symbolically $T\vdash A$, iff there is a derivation $A_1\ldots A_n$ of $T$ s.t. $A_n=A$ holds.
Recall that a theory $T$ is:
- a set of formulas, in case of propositional logic, and
- a set of closed formulas, in case of first-order logic.
- The deductive closure of a theory $T$ is given by:
- $Th(T)=\{A|T\vdash A\}$, in case of propositional logic, and
- $Th(T)=\{A|T\vdash A$ and $A$ is closed$\}$, in case of first-order logic.
- Properties:
- Inflationaryness: $T\subseteq Th(T)$
- Idempotency: $Th(T)=Th(Th(T))$
- Monotony: $T\subseteq T'$ implies $Th(T)\subseteq Th(T')$
Acknoledgement: the entry was inspired by the course Non-monotonic Reasoning given by Prof. Hans Tompits