  For the justification of the laws for the logical constants ∧, ∨, ∃ and ⊥, Lorenzen uses an inversion principle (a term he coined). In a very simplified form, without taking variables in rules into account, the inversion principle says that everything that can be obtained from every defining condition of A can be obtained from A itself. For example, in the case of disjunction, let A and B each be a defining condition of A∨B as expressed by the primitive rules A → A∨B and B → A∨B. Then the inversion principle says that A∨B →C is admissible assuming A →C and B →C, which justifies the elimination rule for disjunction. The remaining connectives are dealt with in a similar way. In the case of ⊥, the absurdity rule ⊥→ A is obtained from the fact that there is no defining condition for ⊥.