Definition
Derivation (Propositional Hilbert Calculus)
A derivation from a theory
in the Hilbert calculus is a finite sequence of formulas, , where each is either:
- an instance of
; - a premise
; or - obtained by modus ponens from earlier entries:
Its conclusion is
. For , it is an assumption-free proof.