LPC1: Decision Procedure II- Justification
Every wff of LPC1 is a truth-function of quantified schemata; i.e. it has the form of a wff of PC, with quantified schemata taking the place of propositional variables. Hence since every wff of PC can be reduced to CNF (see Appendix 1), so can every wff of LPC1, the quantified schemata within it remaining unchanged in the process. The rules for the transformation of quantifiers always enable us to remove a negation sign in front of a quantifier; and LED can be applied to any disjunction of unnegated existentially quantified schemata. Therefore every wff of LPC1 can be reduced to the required standard form.