\begin{definition}[Definition:Gentzen Proof System/Instance 1]
This instance of a Gentzen proof system is used in:
* {{BookReference|Mathematical Logic for Computer Science|2012|M. Ben-Ari|ed=3rd|edpage=Third Edition}}
Let $\LL$ be the language of propositional logic.
The Gentzen system applies to sets of propositional formulae.
The intuition behind the system is that a set $U$ represents its disjunction.
$\mathscr G$ has the following axioms and rules of inference:
\end{definition}