  Lorenzen, in his Introduction to Operative Logics and Mathematics (1955) starts with logic-free (atomic) calculi, which correspond to production systems or grammars. He calls a rule admissible in such a system if it can be added to it without enlarging the set of its derivable atoms. The implication arrow → is interpreted as expressing admissibility. An implication A → B is considered to be valid, if, when read as a rule, it is admissible (with respect to the underlying calculus). For iterated implications (= rules) Lorenzen develops a theory of admissibility statements of higher levels. Certain statements such as A →A or ((A →B), (B →C)) → (A →C) hold independently of the underlying calculus. They are called universally admissible [“allgemeinzulässig”]), and constitute a system of positive implicational logic. In a related way, laws for universal quantification ∀ are justified using admissibility statements for rules with schematic variables.