  So the idea underlying Gentzen’s programme is that we have “definitions” in the form of introduction rules and some sort of semantic reasoning which, by using “certain requirements”, validate the elimination rules.