ABSTRACT
The formulae in the system LPC1 contain predicate variables, operators and quantifiers, but no individual-variables. Every well-formed formula (wffs) of LPC1 consists either of a quantified schema, or of a truth-function of one or more quantified schemata. Predicate-expressions on their own are not to count as formulae, either well-formed or ill-formed, of LPC1. The reason is as follows. Just as Propositional Calculus (PC) is a calculus which displays the relations between propositions regardless of their internal structure, so LPC1 is to be a calculus which displays relations between certain limited types of propositions, viz. those with a certain kind of internal structure. The wffs of LPC1 can be divided into those which are valid, those which are contingent, and those which are inconsistent. The Decision Problem for LPC1 is exactly analogous to that for Propositional Calculus.
