 Powerful, incisive and revolutionary though Gentzen’s approach has since proved to be, it was, in its turn, curiously limited. It was restricted to just the universally acknowledged logical operators of first-order logic: ¬, ∧, ∨, →, ∃ and ∀. 