\begin{definition}[Definition:Gentzen Proof System]
'''Gentzen proof systems''' are a class of proof systems for propositional and predicate logic.
Their characteristics include:
* The presence of few axioms and many rules of inference.
* Use of formal, sequent-like notation involving the turnstile $\vdash$.
* Proofs whose structure can be viewed as rooted trees.
Specific instances may deviate from this general scheme at some points.
{{transclude:Definition:Gentzen Proof System/Instance 1
  |section = tc
  |header = 3
  |title = Instance 1
  |increase = 1
  |link = true
}}
{{NamedforDef|Gerhard Karl Erich Gentzen|cat = Gentzen}}
\end{definition}