\begin{definition}[Definition:Hilbert Proof System]
'''Hilbert proof systems''' are a class of proof systems for propositional and predicate logic.
Their characteristics include:
* The presence of many axioms;
* Typically only Modus Ponendo Ponens as a rule of inference.
Specific instances may deviate from this general scheme at some points.
{{improve|Transclusion is going to be unfeasible in this detail. But how to change it?}}
{{transclude:Definition:Hilbert Proof System/Instance 1
  | section = tc
  | header = 3
  | title = Instance 1
  | increase = 1
  | link = true
}}
{{transclude:Definition:Hilbert Proof System/Instance 2
  | section = tc
  | header = 3
  | title = Instance 2
  | increase = 1
  | link = true
}}
{{NamedforDef|David Hilbert|cat = Hilbert}}
Category:Definitions/Mathematical Logic
Category:Definitions/Propositional Logic
\end{definition}