In 1.6 we introduced the principle of substitution of equivalents, according to which if we replace in a sentence an expression with a logically equivalent expression, there will be no change in the truth value of the sentence. In propositional logic, we used this principle in the natural deduction (1.8) and in the logical transformations (1.9). We also used it in the proof procedure of predicate logic (3.5). For example, in the latter the expression “¬∀” may always be replaced by “∃¬” because any formula of the type “¬∀…” is logically equivalent to “∃¬…”. We will proceed with the use of the principle and will obtain within the predicate logic a procedure analogous to the logical transformations in propositional logic.
Some of the equivalence schemes we will use have been introduced in 3.5:
| The relationship between the quantifiers: | ∀xα ⇔ ¬∃х¬α |
| ∃хα ⇔ ¬∀х¬α | |
| ¬∀хα ⇔ ∃х¬α | |
| ¬∃хα ⇔ ∀х¬α |
| The distribution of the universal quantifier over conjunctions and of the existential quantifier over disjunctions: : |
∃х(α ∨ β)
⇔ ∃хα ∨ ∃хβ |
|
∀х(α ∧ β)
⇔ ∀хα ∧ ∀хβ |
The first of the last two schemes allows us, if the scope of an existential quantifier is a disjunction, to distribute the quantifier over the disjuncts, and vice versa – if before each disjunct there is an existential quantifier with the same variable, to bring the quantifier before the disjunction. According to the last scheme, the same applies to universal quantifier and conjunction. The disjunctions and conjunctions in question can have more than two members.
A further group of equivalence schemes that we will use are called rules of passage.
If p is an arbitrary statement (say “Socrates is mortal”) and F an arbitrary (simple or compound) predicate, there is the following logical equivalence:
| ∃x(Fх ∧ p) ⇔ ∃xFх ∧ p |
It matters that p is a statement. As such it contains no free occurrences of “x”. Therefore, the quantifier in “∃x(Fх ∧ p)” is irrelevant to p and its scope can “pass” through p without a change in the meaning of the whole sentence. For example, if p is “Socrates is mortal” and F is “…is a cat”, the statement “There is something that satisfies the condition that it is a cat and that Socrates is mortal” (“∃x(Fx ∧ p)”) will be true if and only if there exists a cat and Socrates is mortal, i.e. if and only if the sentence “There are cats and Socrates is mortal” (“∃xFх ∧ p”) is true. Thе scheme will also be valid if p is not a statement but an open sentence, as long as there are no free occurrences of “x” in it. Then the quantifier will again be irrelevant to p and its scope can be moved through p without changing the meaning of the whole sentence. For example, the following equivalence scheme is also valid:
| ∃x(Fх ∧ Gy) ⇔ ∃xFх ∧ Gy |
To say that there is something that satisfies the condition that it is a cat (F) and that y is a human (G) is the same as saying that there are cats and (irrelevantly) that y is a person.
So, the following general equivalence scheme is logically valid:
| (1) |
∃x[α(х) ∧ β]
⇔ ∃xα(х) ∧ β |
| where “x” is not free in β |
α(x) is an expression in which there may be free “x” and β is an expression in which there may or may not be free variables but there is no free “x”. Of course, in place of “x” can be any other variable.
In support of the above informal argument, we will prove by our proof procedure that the two expressions in (1) are indeed logically equivalent.
We first prove that from “∃x[α(x) ∧ β]” logically follows “∃xα(x) ∧ β”:
| 1. ∃x[α(х) ∧ β] / ∃xα(х) ∧ β |
| 2. ¬[∃xα(х) ∧ β] assumption |
| 3. ¬∃xα(х) ∨ ¬β 2, De M |
| 4. ∀x¬α(х) ∨ ¬β 3, RbQ |
| 5. α(a) ∧ β 1, EI (a is an arbitrary new constant)1 |
| 6. α(a) 5, S |
| 7. β 5, S |
| 8. ∀x¬α(х) 4, 7, DS |
| 9. ¬α(a) 8, UI – contradicts 6 |
| 10. ∃xα(х) ∧ β 2–9, reductio ad absurdum |
A proof that “∃xα(x) ∧ β” entails “∃x[α(x) ∧ β]”:
| 1. ∃xα(х) ∧ β / ∃x[α(х) ∧ β] |
| 2. ¬∃x[α(х) ∧ β] assumption |
| 3. ∀x¬[α(х) ∧ β] 2, RbQ |
| 4. ∃xα(х) 1, S |
| 5. α(a) 4, EI (a is an arbitrary new constant) |
| 6. ¬[α(a) ∧ β] 3, UI2 |
| 7. β 1, S |
| 8. α(a) ∧ β 5, 7, Conj – contradicts 6 |
| 9. ∃x[α(х) ∧ β] 2–8, reductio ad absurdum |
Let us see why (1) may not be valid if β contains a free occurrence of “x”. Let α(x) be “Fx” and β be “Gx”, and interpret “F” as “…is round” and “G” as “…is square”. Then the sentence “∃x(Fx ∧ Gx)” becomes false – it states that something is both round and square. On the other hand, “∃xFx ∧ Gx” corresponds to the open sentence “Something is round, and x is square”. It becomes true if “x” takes a square thing as value. The two formulas are not logically equivalent, as if they were, it would not be possible for one to be true and the other false.
We continue with the rules of passage. The following equivalence scheme is also logically valid:
| (2) |
∃x[α(х) ∨ β]
⇔ ∃xα(х) ∨ β |
| where “x” is not free in β |
The proof is like that of (1).
The order of the conjuncts in (1) and disjuncts in (2) is obviously irrelevant – “∃x[β ∧ α(x)]” ⇔ “β ∧ ∃xα(x)” and “∃x[β ∨ α(x)]” ⇔ “β ∨ ∃xα(x)” are also logically valid equivalence schemes when there is no free “x” in β.
(1) and (2) allow us to move the scope of the existential quantifier through one of the members of a conjunction or a disjunction when the quantifier variable is not free in it. The same is true for the universal quantifier because the following two equivalence schemes are also logically valid:
| (3) |
∀x[α(х) ∧ β]
⇔ ∀xα(х) ∧ β |
| where “x” is not free in β |
| (4) |
∀x[α(х) ∨ β]
⇔ ∀xα(х) ∨ β |
| where “x” is not free in β |
(3) can be derived from (2) by the following sequence of logical equivalences:
| ∀x[α(х) ∧ β] |
| ¬∃x¬[α(х) ∧ β] RbQ |
| ¬∃x[¬α(х) ∨ ¬β] De M |
| ¬(∃x¬α(х) ∨ ¬β) by (2) (there is no free “x” in ¬β) |
| ¬∃x¬α(х) ∧ ¬¬β De M |
| ∀xα(х) ∧ β RbQ and DN |
In turn, (4) can be derived from (1) by the following sequence of equivalences:
| ∀x[α(х) ∨ β] |
| ¬∃x¬[α(х) ∨ β] RbQ |
| ¬∃x[¬α(х) ∧ ¬β] De M |
| ¬(∃x¬α(х) ∧ ¬β) by (1) (there is no free “x” in ¬β) |
| ¬∃x¬α(х) ∨ ¬¬β De M |
| ∀xα(х) ∨ β RbQ and DN |
Equivalence schemes (3) and (4) allow us to move the scope of the universal quantifier through one of the members of a conjunction or disjunction when they lack free occurrences of the quantifier variable. Here, as in the analogous rules for the existential quantifier, the order of the disjuncts or conjuncts is irrelevant – it does not matter whether β is in the first or in the second place. Not so, however, with the rules of passage through the antecedent or the consequent of a conditional, which we will consider now.
Below are the rules of passage through the antecedent of a conditional – one for the existential, the other for the universal quantifier:
| (5) |
∃x[β → α(х)]
⇔ β → ∃xα(х) |
| where “x” is not free in β |
| (6) |
∀x[β → α(х)]
⇔ β → ∀xα(х) |
| where “x” is not free in β |
(5) is derived from (2) by the following series of equivalences:
| ∃x[β → α(х)] | |
| ∃x[¬β ∨ α(х)] | Imp |
| ¬β ∨ ∃xα(х) | by (2) |
| β → ∃xα(х) | Imp |
(6) is derived from (4) by the following series of equivalences:
| ∀x[β → α(х)] | |
| ∀x[¬β ∨ α(х)] | Imp |
| ¬β ∨ ∀xα(х) | by (4) |
| β → ∀xα(х) | Imp |
By the equivalence schemes (5) and (6), the scope of the existential or universal quantifier can pass through the antecedent of a conditional when it lacks free occurrences of the quantifier variable. They are analogous to the rules of passage for conjunction and disjunction. The rules of passage through the consequent of a conditional are different as the quantifier changes – if it is existential, after the passage it becomes universal, and vice versa. I.e. we have the following two equivalence schemes:
| (7) |
∃x[α(х) → β]
⇔ ∀xα(х) → β |
| where “x” is not free in β |
| (8) |
∀x[α(х) → β]
⇔ ∃xα(х) → β |
| where “x” is not free in β |
(7) is derived from (2) by the following series of equivalences:
| ∃x[α(х) → β] | |
| ∃x[¬α(х) ∨ β] | Imp |
| ∃x¬α(х) ∨ β | by (2) |
| ¬∀xα(х) ∨ β | RbQ |
| ∀xα(х) → β | Imp |
(8) is derived from (4) by the following series of equivalences:
| ∀x[α(х) → β] | |
| ∀x[¬α(х) ∨ β] | Imp |
| ∀x¬α(х) ∨ β | by (4) |
| ¬∃xα(х) ∨ β | RbQ |
| ∃xα(х) → β | Imp |
The following table summarizes the rules of passage:
| “x” is not free in β | |
|
passage through conjunction
(the quantifier remains the same) |
∃x[α(х) ∧ β] ⇔ ∃xα(х) ∧ β |
|
∀x[α(х) ∧ β] ⇔ ∀xα(х) ∧ β |
|
|
passage through disjunction
(the quantifier remains the same) |
∃x[α(х) ∨ β] ⇔ ∃xα(х) ∨ β |
|
∀x[α(х) ∨ β] ⇔ ∀xα(х) ∨ β |
|
|
passage through the antecedent of a conditional
(the quantifier remains the same) |
∃x[β → α(х)] ⇔ β → ∃xα(х) |
|
∀x[β → α(х)] ⇔ β → ∀xα(х) |
|
|
passage through the consequent of a conditional
(the quantifier changes) |
∃x[α(х) → β] ⇔ ∀xα(х) → β |
|
∀x[α(х) → β] ⇔ ∃xα(х) → β |
|
Using the rules of passage, we can transform formulas of predicate logic into very different formulas, which express the same. As an example, we will show that the formulas “∀y¬Fy → (¬∃xGаx ∨ ¬∀yHаy)” and “∀х∃y[Fy ∨ (Gax → ¬Hay)]” are logically equivalent by transforming the former into the latter:
| ∀y¬Fy → (¬∃xGаx ∨ ¬∀yHаy) |
| ¬∀y¬Fy ∨ ¬∃xGаx ∨ ¬∀yHаy Imp |
| ¬∀y¬Fy ∨ (∃xGаx → ¬∀yHаy) Imp |
| ∃yFy ∨ (∃xGаx → ∃y¬Hаy) RbQ, two times |
| ∃yFy ∨ ∀х(Gаx → ∃y¬Hаy) The scope of “∃x” passes through the consequent “∃y¬Hay”, in which there is no free “x”. |
| ∀х[∃yFy ∨ (Gаx → ∃y¬Hаy)] The scope of “∀x” passes through the disjunct “∃yFy”, in which there is no free “x”. |
| ∀х[∃yFy ∨ ∃y(Gаx → ¬Hаy)] The scope of the second “∃y” passes through the antecedent “Gax”, in which there is no free “y”. |
| ∀х∃y[Fy ∨ (Gаx → ¬Hаy)] distribution of the existential quantifier over disjunction |
The rules of passage allow any formula of predicate logic to be transformed into a logically equivalent formula in which all quantifiers are at the beginning. This is done through a series of equivalent transformations, through which the quantifiers gradually move forward until they are all at the beginning. We will say of such a formula (in which all quantifiers are in front) that it is in prenex form. Here is an example:
| ∀xFx → ∃y[Gya ∨ ∀z(Fyz ∧ Gzy)] initial formula |
| ∃x{Fx → ∃y[Gya ∨ ∀z(Fyz ∧ Gzy)]} „∀х“ passes through the consequent |
| ∃x∃y{Fx → [Gya ∨ ∀z(Fyz ∧ Gzy)]} „∃y“ passes through the antecedent |
| ∃x∃y{Fx → ∀z[Gya ∨ (Fyz ∧ Gzy)]} „∀z“ passes through the disjunct |
| ∃x∃y∀z{Fx → [Gya ∨ (Fyz ∧ Gzy)]} „∀z“ passes through the antecedent |
The last formula is in prenex form.
Depending on the order in which the quantifiers are moved forward, a formula can be converted to different prenex forms. In the above example, we could first move forward “∃y” and “∀z” and then “∃x”, as a result of which we would get the different but logically equivalent formula in prenex form “∃y∀z∃x{Fx → [Gya ∨ (Fyz ∧ Gzy)]}”.
The subformula after the quantifiers in a formula in prenex form is called matrix. For example, the matrix of “∃x∃y∀z{Fx → [Gya ∨ (Fyz ∧ Gzy)]}” is “Fx → [Gya ∨ (Fyz ∧ Gzy)]”.
Each formula can be converted to prenex form. Sometimes, however, it is necessary to make some preparations. They are of two types. The first is necessary when a biconditional occurs in the formula and in at least one of the subformulas it connects there is a quantifier. Then, since we do not have a rule of passage for the biconditional, the quantifiers will be “locked” on one side of the biconditional and will not be able to move forward. The solution is to replace the biconditional with a conjunction of two conditionals according to the scheme “α↔β” ⇔ “(α→β) ∧ (β→α)”. Then the rules of passage become applicable.
The second kind of preparation is required in cases when the formula has two (or more) quantifiers with the same variable or when a quantifier has the same variable as a variable that is free in the formula. Then we must replace some quantifiers’ variables with new variables until these two things cease to be a fact. Such replacements do not change the meaning of the initial formula. For example, there will be no change in the meaning of a formula if we replace in it “∃xFx” with “∃yFy” – both formulas state that there is something that is F. When replacing a quantifier’s variable with a new one, we must of course also replace all the occurrences of the variable bound by the quantifier. For example, if we want to change the variable of the existential quantifier in “∃x(Fx ∨ ¬Gx) ∧ ∀xHx” to “y”, except replacing “∃x” with “∃y”, we must also replace the occurrences of “x” within the parentheses; the result we will be “∃y(Fy ∨ ¬Gy) ∧ ∀xHx”.
Let us consider the case in which a quantifier has the same variable as a variable free in the formula. Such is the case with the formula “Fx → ∀xGx”. The first occurrence of “x” is free in it, while the variable of the universal quantifier is also “x”. This prevents the formula from being converted to prenex form because the quantifier cannot move forward due to the free occurrence of “x” in “Fx”. If we change the quantifier’s variable with a new one, say with “y”, there will no longer be a problem – “∀y” in “Fx → ∀уGу” can move forward as in “Fx” there is no free “y”.
This is what we should do when there are quantifiers with the same variable in a formula. Consider, for example, the formula “∀x(Fx → ∃xGxa)”. It has a universal and existential quantifier with the same variable. As a result, “∃x” cannot move forward because “Fx” has a free “x”. However, if we change the variable of one of the quantifiers (say the second one) with “y”, there will be no problem. The quantifier “∃у” in “∀х(Fx → ∃уGуa”) can move forward now because there is no free “y” in the antecedent of the conditional. The result is the prenex form “∀х∃у(Fx → Gуa)”.
Finally, let us convert to prenex form a formula in which both things are present – a biconditional and quantifiers with the same variable:
| ∀y(Fa ↔ ∃xGxy) initial formula |
| ∀y[(Fa → ∃xGxy) ∧ (∃xGxy → Fa)] Equiv |
| ∀y[(Fa → ∃xGxy) ∧ (∃zGzy → Fa)] The variable of the second “∃x” is changed to „z“. |
| ∀y[∃x(Fa → Gxy) ∧ (∃zGzy → Fa)] “∃х” passes through the antecedent |
| ∀y∃x[(Fa → Gxy) ∧ (∃zGzy → Fa)] “∃х” passes through the conjunct |
| ∀y∃x[(Fa → Gxy) ∧ ∀z(Gzy → Fa)] “∃z” passes through the consequent |
| ∀y∃x∀z[(Fa → Gxy) ∧ (Gzy → Fa)] “∀z” passes through the conjunct |
| (1) Prove by transformations that the following pairs of formulas are logically equivalent. |
| 1) |
∀x(¬Fx ∧ Gbx)
¬∃xFx ∧ ∀xGbx |
| 2) |
∀x[∃yFyx → ∃zGzx]
∀x∀y∃z(Fyx → Gzx) |
| 3) |
¬∀z(Hz ∧ ∃xFxz) → ∀yGy
∀y[(∀zHz ∧ ∀z∃xFxz) ∨ Gy] |
| 4) |
∃y(Fy → ∀xGxy)
¬∀yFy ∨ ∃y∀xGxy |
| 5) |
∃z¬(Hzz ∧ Gza)
¬∀zHzz ∨ ∃z¬Gza |
| 6) |
∀y[¬Fay ∧ ∀zGyz] ∨ ∃zHz
∀z¬Hz → [¬∃yFay ∧ ∀y∀zGyz] |
| 7) |
∀xFxy ↔ ¬∃zGz
∃x(Fxy → ∀z¬Gz) ∧ ∀x∃z(¬Gz → Fxy) |
| 8) |
∀y[Fy → Hay] → ∃zHza
∃z∃y[(Fy ∧ ¬Hay) ∨ Hza] |
| 9) |
∃y[∃x(Hy ∨ ¬Gxy) → ¬∃zFz]
∀z[∀y∃x(Gxy → Hy) → ¬Fz] |
| 10) |
∀yFy → {[∃xHxх ∨ ∃xGx] → ∃zHzz}
∃z∃y{Fy → ∀x[(Hxх ∨ Gx) → Hzz]} |
| 11) |
∀y[∀xFx → (∃zGzy ∧ Hy)]
∃x[Fx → ∀y∃z(Gzy ∧ Hy)] |
| 12) |
∀x(Hx ∧ Fxy) → ∃z(Gх ∧ Hz)
∃z[¬∀xHx ∨ ¬∀xFxy ∨ (Gx ∧ Hz)] |
| (2) Convert each of the following formulas to prenex form. |
| 1) | ∀х∃уGxy → [∃y∀zGyz → ∀x∀zFxz] |
| 2) | ∃x∀yFxy → [∀y∃xGyx ∧ ¬∀x∃zHxz] |
| 3) | [∀xFx ↔ ∀xGx] → ∀xHx |
| 4) | ∃xFx → [∃xGx ↔ ∃xHx] |