The intuitive connections between some and every noted earlier are reflected in the fact that the following equivalences are valid: (∃x)ϕx ≡ ∼(∀x)∼ϕx
(∀x)ϕx ≡ ∼(∃ x)∼ϕx These equivalences remain valid when ϕx is replaced by any wff, however complex; i.e., for any wff α whatsoever, (∃x)α ≡ ∼(∀x)∼α and (∀x)α ≡ ∼(∃ x)∼α are valid. Because the rule of substitution of equivalents can be shown to hold in LPC, it follows that (∃x) may be replaced anywhere in a wff by ∼(∀x)∼, or (∀x) by ∼(∃x)∼, and the resulting wff will be equivalent to the original. Similarly, because the law of double negation permits the deletion of a pair of consecutive negation signs, ∼(∃x) may be replaced by (∀x)∼, and ∼(∀x) by (∃x)∼.

These principles are easily extended to more complex cases. To say that there is a pair of objects satisfying a certain condition is equivalent to denying that every pair of objects fails to satisfy that condition, and to say that every pair of objects satisfies a certain condition is equivalent to denying that there is any pair of objects that fails to satisfy that condition. These equivalences are expressed formally by the validity, again for any wff α, of (∃x)(∃y)α ≡ ∼(∀x)(∀y)∼α and (∀x)(∀y)α ≡ ∼(∃x)(∃y)∼α and by the resulting replaceability anywhere in a wff of (∃x)(∃y) by ∼(∀x)(∀y)∼, or of (∀x)(∀y) by ∼(∃x)(∃y)∼.

Analogously, (∃x)(∀y) can be replaced by ∼(∀x)(∃y)∼ [e.g., (∃x)(∀y)(x loves y)—“There is someone who loves everyone”—is equivalent to ∼(∀x)(∃y)∼(x loves y)—“It is not true of everyone that there is someone whom he does not love”]; (∀x)(∃y) can be replaced by ∼(∃x)(∀y)∼; and in general the following rule, covering sequences of quantifiers of any length, holds:

1. If a wff contains an unbroken sequence of quantifiers, then the wff that results from replacing ∀ by ∃ and vice versa throughout that sequence and inserting or deleting ∼ at each end of it is equivalent to the original wff.

This may be called the rule of quantifier transformation. It reflects, in a generalized form, the intuitive connections between some and every that were noted above.

The following are also valid, again where α is any wff: (∀x)(∀y)α ≡ (∀y)(∀x)α
(∃x)(∃y)α ≡ (∃y)(∃x)α

The extensions of these lead to the following rule:

• 2. If a wff contains an unbroken sequence either of universal or of existential quantifiers, these quantifiers may be rearranged in any order and the resulting wff will be equivalent to the original wff.

This may be called the rule of quantifier rearrangement.

Two other important rules concern implications, not equivalences:

• 3. If a wff β begins with an unbroken sequence of quantifiers, and β′ is obtained from β by replacing ∀ by ∃ at one or more places in the sequence, then β is stronger than β′—in the sense that (β ⊃ β′) is valid but (β′ ⊃ β) is in general not valid.

• 4. If a wff β begins with an unbroken sequence of quantifiers in which some existential quantifier Q₁ precedes some universal quantifier Q₂, and if β′ is obtained from β by moving Q₁ to the right of Q₂, then β is stronger than β′.

As illustrations of these rules, the following are valid for any wff α:

In each case, the converses are not valid (though they may be valid in particular cases in which α is of some special form).

Some of the uses of the above rules can be illustrated by considering a wff α that contains precisely two free individual variables. By prefixing to α two appropriate quantifiers and possibly one or more negation signs, it is possible to form a closed wff (called a closure of α) that will express a determinate proposition when a meaning is assigned to the predicate variables. The above rules can be used to list exhaustively the nonequivalent closures of α and the implication relations between them. The simplest example is ϕxy, which for illustrative purposes can be taken to mean “x loves y.” Application of rules 1 and 2 will show that every closure of ϕxy is equivalent to one or another of the following 12 wffs (none of which is in fact equivalent to any of the others):

• (a) (∀x)(∀y)ϕxy (“Everybody loves everybody”);
• (b) (∃x)(∀y)ϕxy (“Somebody loves everybody”);
• (c) (∃y)(∀x)ϕxy (“There is someone whom everyone loves”);
• (d) (∀y)(∃x)ϕxy (“Each person is loved by at least one person”);
• (e) (∀x)(∃y)ϕxy (“Each person loves at least one person”);
• (f) (∃x)(∃y)ϕxy (“Somebody loves somebody”); and
• (g)–(l) the respective negations of each of the above.

Rules 3 and 4 show that the following implications among formulas (a)–(f) are valid:

The implications holding among the negations of (a)–(f) follow from these by the law of transposition; e.g., since (a) ⊃ (b) is valid, so is ∼(b) ⊃ ∼(a). The quantification of wffs containing three, four, etc., variables can be dealt with by the same rules.

Intuitively, (∀x)ϕx and (∀y)ϕy both “say the same thing”—namely, that everything is ϕ—and (∃x)ϕx and (∃y)ϕy both mean simply that something is ϕ. Clearly, so long as the same variable occurs both in the quantifier and as the argument of ϕ, it does not matter what letter is chosen for this purpose. The procedure of replacing some variable in a quantifier, together with every occurrence of that variable in its scope, by some other variable that does not occur elsewhere in its scope is known as relettering a bound variable. If β is the result of relettering a bound variable in a wff α, then α and β are said to be bound alphabetical variants of each other, and bound alphabetical variants are always equivalent. The reason for restricting the replacement variable to one not occurring elsewhere in the scope of the quantifier can be seen from an example: If ϕxy is taken as before to mean “x loves y,” the wff (∀x)ϕxy expresses the proposition form “Everyone loves y,” in which the identity of y is left unspecified, and so does its bound alphabetical variant (∀z)ϕzy. If x were replaced by y, however, the closed wff (∀y)ϕyy would be obtained, which expresses the proposition that everyone loves himself and is clearly not equivalent to the original.

A wff in which all the quantifiers occur in an unbroken sequence at the beginning, with the scope of each extending to the end of the wff, is said to be in prenex normal form (PNF). Wffs that are in PNF are often more convenient to work with than those that are not. For every wff of LPC, however, there is an equivalent wff in PNF (often simply called its PNF). One effective method for finding the PNF of any given wff is the following:

1. Reletter bound variables as far as is necessary to ensure (a) that each quantifier contains a distinct variable and (b) that no variable in the wff occurs both bound and free.
2. Use definitions or PC equivalences to eliminate all operators except ∼, ·, and ∨.
3. Use the De Morgan laws and the rule of quantifier transformation to eliminate all occurrences of ∼ immediately before parentheses or quantifiers.
4. Gather all of the quantifiers into a sequence at the beginning in the order in which they appear in the wff and take the whole of what remains as their scope. Example:

   (∀x){[ϕx · (∃y)ψxy] ⊃ (∃y)χxy} ⊃ (∃z)(ϕz ⊃ ψzx).

Step 1 can be achieved by relettering the third and fourth occurrences of y and every occurrence of x except the last (which is free); thus (∀w){[ϕw · (∃y)ψwy] ⊃ (∃u)χwu} ⊃ (∃z)(ϕz ⊃ ψzx). Step 2 now yields ∼(∀w){∼[ϕw · (∃y)ψwy] ∨ (∃u)χwu} ∨ (∃z)(∼ϕz ∨ ψzx). By step 3 this becomes (∃w){[ϕw · (∃y)ψwy] · (∀u)∼χwu} ∨ (∃z)(∼ϕz ∨ ψzx). Finally, step 4 yields (∃w)(∃y)(∀u)(∃z){[(ϕw · ψwy) · ∼χwu] ∨ (∼ϕz ∨ ψzx)}, which is in PNF.

Classification of dyadic relations

Consider the closed wff (∀x)(∀y)(ϕxy ⊃ ϕyx), which means that, whenever the relation ϕ holds between one object and a second, it also holds between that second object and the first. This expression is not valid, since it is true for some relations but false for others. A relation for which it is true is called a symmetrical relation (example: “is parallel to”). If the relation ϕ is such that, whenever it holds between one object and a second, it fails to hold between the second and the first—i.e., if ϕ is such that (∀x)(∀y)(ϕxy ⊃ ∼ϕyx) —then ϕ is said to be asymmetrical (example: “is greater than”). A relation that is neither symmetrical nor asymmetrical is said to be nonsymmetrical. Thus, ϕ is nonsymmetrical if (∃x)(∃y)(ϕxy · ϕyx) · (∃x)(∃y)(ϕxy · ∼ϕyx) (example: “loves”).

Dyadic relations can also be characterized in terms of another threefold division: A relation ϕ is said to be transitive if, whenever it holds between one object and a second and also between that second object and a third, it holds between the first and the third—i.e., if (∀x)(∀y)(∀z)[(ϕxy · ϕyz) ⊃ ϕxz] (example: “is greater than”). An intransitive relation is one that, whenever it holds between one object and a second and also between that second and a third, fails to hold between the first and the third; i.e., ϕ is intransitive if (∀x)(∀y)(∀z)[(ϕxy · ϕyz) ⊃ ∼ϕxz] (example: “is father of”). A relation that is neither transitive nor intransitive is said to be nontransitive. Thus, ϕ is nontransitive if (∃x)(∃y)(∃z)(ϕxy · ϕyz · ϕxz) · (∃x)(∃y)(∃z)(ϕxy · ϕyz · ∼ϕxz) (example: “is a first cousin of”).

A relation ϕ that always holds between any object and itself is said to be reflexive; i.e., ϕ is reflexive if (∀x)ϕxx (example: “is identical with”). If ϕ never holds between any object and itself—i.e., if ∼(∃x)ϕxx —then ϕ is said to be irreflexive (example: “is greater than”). If ϕ is neither reflexive nor irreflexive—i.e., if (∃x)ϕxx · (∃x)∼ϕxx —then ϕ is said to be nonreflexive (example: “admires”).

A relation such as “is of the same length as” is not strictly reflexive, as some objects do not have a length at all and thus are not of the same length as anything, even themselves. But this relation is reflexive in the weaker sense that, whenever an object is of the same length as anything, it is of the same length as itself. Such a relation is said to be quasi-reflexive. Thus, ϕ is quasi-reflexive if (∀x)[(∃y)ϕxy ⊃ ϕxx]. A reflexive relation is of course also quasi-reflexive.

For the most part, these three classifications are independent of each other; thus a symmetrical relation may be transitive (like “is equal to”) or intransitive (like “is perpendicular to”) or nontransitive (like “is one mile distant from”). There are, however, certain limiting principles, of which the most important are:

1. Every relation that is symmetrical and transitive is at least quasi-reflexive.
2. Every asymmetrical relation is irreflexive.
3. Every relation that is transitive and irreflexive is asymmetrical.

A relation that is reflexive, symmetrical, and transitive is called an equivalence relation.

Axiomatization of LPC

Rules of uniform substitution for predicate calculi, though formulable, are mostly very complicated, and, to avoid the necessity for these rules, axioms for these systems are therefore usually given by axiom schemata in the sense explained earlier (see above Axiomatization of PC). Given the formation rules and definitions stated in the introductory paragraph of the earlier section on the lower predicate calculus (see above The lower predicate calculus), the following is presented as one standard axiomatic basis for LPC:

Axiom schemata:

1. Any LPC substitution-instance of any valid wff of PC is an axiom.
2. Any wff of the form (∀a)α ⊃ β is an axiom if β is either identical with α or differs from it only in that, wherever α has a free occurrence of a, β has a free occurrence of some other individual variable b.
3. Any wff of the form (∀a)(α ⊃ β) ⊃ [α ⊃ (∀a)β] is an axiom, provided that α contains no free occurrence of a.

Transformation rules:

1. Modus ponens.
2. If α is a theorem, so is (∀a)α, where a is any individual variable (rule of universal generalization).

The axiom schemata call for some explanation and comment. By an LPC substitution-instance of a wff of PC is meant any result of uniformly replacing every propositional variable in that wff by a wff of LPC. Thus, one LPC substitution-instance of (p ⊃ ∼q) ⊃ (q ⊃ ∼p) is [ϕxy ⊃ ∼(∀x)ψx] ⊃ [(∀x)ψx ⊃ ∼ϕxy]. Axiom schema 1 makes available in LPC all manipulations such as commutation, transposition, and distribution, which depend only on PC principles. Examples of wffs that are axioms by axiom schema 2 are (∀x)ϕx ⊃ ϕx, (∀x)ϕx ⊃ ϕy, and (∀x)(∃y)ϕxy ⊃ (∃y)ϕzy. To see why it is necessary for the variable that replaces a to be free in β, consider the last example: Here a is x, α is (∃y)ϕxy, in which x is free, and β is (∃y)ϕzy, in which z is free and replaces x. But had y, which would become bound by the quantifier (∃y), been chosen as a replacement instead of z, the result would have been (∀x)(∃y)ϕxy ⊃ (∃y)ϕyy, the invalidity of which can be seen intuitively by taking ϕxy to mean “x is a child of y,” for then (∀x)(∃y)ϕxy will mean that everyone is a child of someone, which is true, but (∃y)ϕyy will mean that someone is a child of himself, which is false. The need for the proviso in axiom schema 3 can also be seen from an example. Defiance of the proviso would give as an axiom (∀x)(ϕx ⊃ ψx) ⊃ [ϕx ⊃ (∀x)ψx]; if ϕx were taken to mean “x is a Spaniard,” ψx to mean “x is a European,” and the free occurrence of x (the first occurrence in the consequent) to stand for Francisco Franco, then the antecedent would mean that every Spaniard is a European, but the consequent would mean that, if Francisco Franco is a Spaniard, then everyone is a European.

It can be proved—though the proof is not an elementary one—that the theorems derivable from the above basis are precisely the wffs of LPC that are valid by the definition of validity given in the earlier section on validity in LPC (see above Validity in LPC). Several other bases for LPC are known that also have this property. The axiom schemata and transformation rules here given are such that any purported proof of a theorem can be effectively checked to determine whether it really is a proof or not; nevertheless, theoremhood in LPC, like validity in LPC, is not effectively decidable, in that there is no effective method of telling with regard to any arbitrary wff whether it is a theorem or not. In this respect, axiomatic bases for LPC contrast with those for PC.