ABSTRACT

Every Well-formed formula of Lower Predicate Calculus-1 is a truth-function of quantified schemata; i.e. it has the form of a Well-formed formula of Propositional Calculus, with quantified schemata taking the place of propositional variables. Hence since every Well-formed formula of Propositional Calculus can be reduced to CNF, so can every Well-formed formula of Lower Predicate Calculus-1, 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 Well-formed formula of Lower Predicate Calculus-1 can be reduced to the required standard form.