Transformation of formulas (Calculation of predicates) . In “propositional normal forms” the equivalence relation establishes, for each formula, an equivalence class. Within each of these classes, there is a set of members (formulas) that have a particular structure that makes them the object of special interest. These are the normal ways. Obviously, if the relation “logical equivalence” is also present in the Calculation of predicates , it is logical to expect that some kind of “Normal form” exists between the formulas of the calculation of predicates.
Summary
[ hide ]
- 1 Standard form attached
- 2 Skölem shape
- 3 sets of clauses
- 4 External links
- 5 Bibliography
Pre-attached normal form
A formula of the predicate calculus, is said to be in normal prenexada if of the form: Q (x1) Q (x2) … Q (x) M . ), while M is a formula without quantifiers and in conjunctive normal form, M is said to be the matrix of the$ or “Where each Q (xi) is a quantifier ( formula .
The following are examples of pre-attached normal forms:
- a) Ɐ (x) ∃ (y) [(¬P (x, y) v R (x)) ʌ (P (y, x) v¬R (y))]
- b) Ɐ (x) ∃ (y) [P (x, y) ʌ (¬P (y, x) v R (y))]
- c) Ɐ (x) ∃ (y) [P (y, x) v ¬R (y)]
- d) Ɐ (x) ∃ (y) P (y, x)
- e) P (a, b) ʌ (¬P (b, a) v R (b))
However, the formulas presented below are not in the normal pre-attached form:
- a) Ɐ (x) [∃ (y) (¬P (x, y) v R (x)) ʌ ¬R (x)]b) Ɐ (x) ∃ (y) [(¬P (x, y ) ʌ R (x)) v ¬R (x)]
In case a), the existential quantifier (∃ (y)) does not affect the whole conjunctive normal form or seen otherwise, a quantifier is present in the matrix.
In case b), the quantifiers are well positioned, but the matrix is not in conjunctive normal form.
Although evidently not every formula of the calculation of predicates is a pre-attached normal form, it is possible to find for each one, another formula that is logically equivalent and is in pre-attached normal form.
The way to achieve this is through the equivalence laws studied following the logical order that appears below:
- Delete all conditionals (→) and biconditional (⇔). For this the laws are applied as many times as necessary:
A → B ⇔ ¬A v B
A ↔ B ⇔ A → B ʌ B → A
- Remove the negations (¬) towards the interior of the matrix, until they affect only atoms. This is done by relying on D` Morgan’s laws, generalized D` Morgan’s laws, and the law of double negation:
¬ (A ʌ B) ⇔ ¬A v¬B
¬ (A v B) ⇔ ¬A ʌ ¬B ¬Ɐ (x) A (x) ⇔ ∃ (x) ¬A (x)
Ɐ (x) ¬A ( x) ⇔ ¬∃ (x) A (x) ¬¬A ⇔ A
- Remove the quantizers (Ɐ, ∃) on the left, increasing their range until each affects the entire matrix.
The laws that make this objective possible are:
Ɐ (x) A (x) v B ⇔ Ɐ (x) [A (x) v B]
∃ (x) A (x) v B ⇔ ∃ (x) [A (x) v B]
Ɐ (x) A (x) ʌ B ⇔ Ɐ (x) [A (x) ʌ B]
∃ (x) A (x) ʌ B ⇔ ∃ (x) [A (x) ʌ B]
Ɐ (x) A (x) ʌ Ɐ (x) B (x) ⇔ Ɐ (x) [A (x) ʌ B (x)]
∃ (x) A (x) v∃ (x) B (x) ⇔ ∃ (x) [A (x) v B (x)]
Ɐ (x) A (x) ⇔ Ɐ (y) A (y)
∃ (x) A (x) ⇔ ∃ (y) A (y)
- Transform the matrix into a conjunctive normal form. Because at this stage, negations only affect literals in the matrix and there are no conditionals or biconditional ones, all that is necessary to obtain a conjunctive normal form is to apply the distributive laws conveniently:
A ʌ (B v C) ⇔ (A ʌ B) v (A ʌ C) A v (B ʌ C) ⇔ (A v B) ʌ (A v C)
The following example illustrates how to transform a predicate calculus formula into an equivalent pre-attached normal form:
Let be the formula: Ɐ (x) Ɐ (y) [S (x, y) ↔ Ɐ (z) [P (z, x) → P (z, y)]]
Firstly, the double implication is eliminated, leaving:
Ɐ (x) Ɐ (y) [(S (x, y) → Ɐ (z) [P (z, x) → P (z, y)]) ʌ (Ɐ (z) [P (z, x) → P (z, y)] → S (x, y))]
Then the implications are removed, resulting in:
Ɐ (x) Ɐ (y) [(¬S (x, y) v Ɐ (z) [¬P (z, x) v P (z, y)]) ʌ (¬Ɐ (z) [¬P ( z, x) v P (z, y)] v S (x, y))]
The next step is to remove the deniers towards the interior of the matrix, looking for them to affect only atoms, in this case you simply have a denier that does not affect an atom (¬Ɐ (z) […), by applying the law of D ‘Morgan ( Augustus De Morgan ) generalized you get:
Ɐ (x) Ɐ (y) [(¬S (x, y) v Ɐ (z) [¬P (z, x) v P (z, y)]) ʌ (∃ (z) ¬ [¬P ( z, x) v P (z, y)] v S (x, y))]
As can be seen, even the denier does not directly affect an atom , which makes it necessary to apply D ‘Morgan’s law to obtain:
Ɐ (x) Ɐ (y) [(¬S (x, y) v Ɐ (z) [¬P (z, x) v P (z, y)]) ʌ (∃ (z) [P (z, x) ʌ ¬P (z, y)] v S (x, y))]
Once all the deniers affect only atoms, it is necessary to remove the quantifiers to the left, in this case firstly the existential quantifier (it can be any), being in a first step:
Ɐ (x) Ɐ (y) [(¬S (x, y) v Ɐ (z) [¬P (z, x) v P (z, y)]) ʌ ∃ (z) ([P (z, x) ʌ ¬P (z, y)] v S (x, y))]
A second step is necessary to continue increasing the scope of the quantizer, as a result of this we obtain:
Ɐ (x) Ɐ (y) ∃ (z) [(¬S (x, y) v Ɐ (z) [¬P (z, x) v P (z, y)]) ʌ ([P (z, x) ʌ ¬P (z, y)] v S (x, y))]
There is still a quantizer left in the array, the first step to removing it outside results in:
Ɐ (x) Ɐ (y) ∃ (z) [Ɐ (z) (¬S (x, y) v [¬P (z, x) v P (z, y)]) ʌ ([P (z, x) ʌ ¬P (z, y)] v S (x, y))]
Before taking the next step to extract the quantizer from the matrix, we must solve the problem that occurs when free z occurs in:
[P (z, x) ʌ ¬P (z, y)] v S (x, y)
One way to solve it is substituting z in Ɐ (z) (¬S (x, …) for another variable not used in the formula, in this case v:
Ɐ (x) Ɐ (y) ∃ (z) [Ɐ (v) (¬S (x, y) v [¬P (v, x) v P (v, y)]) ʌ ([P (z, x) ʌ ¬P (z, y)] v S (x, y))]
Now it is possible to finish extracting the quantizer from the matrix:
Ɐ (x) Ɐ (y) ∃ (z) Ɐ (v) [(¬S (x, y) v [¬P (v, x) v P (v, y)]) ʌ ([P (z, x) ʌ ¬P (z, y)] v S (x, y))]
To finally obtain the pre-attached normal form, you just have to transform the matrix into a conjunctive normal form, which is achieved by means of the distributive law:
Ɐ (x) Ɐ (y) ∃ (z) Ɐ (v) [(¬S (x, y) v ¬P (v, x) v P (v, y)) ʌ (P (z, x) v S (x, y)) ʌ (¬P (z, y) v S (x, y))]
Skölem shape
The Skölem form, is a pre-attached normal form, where existential quantifiers do not appear, any formula can be transformed into a Skölem form based on the following principles:
- If in an formula, an existential quantifier is not preceded by any universal quantifier, as in ∃ (x) A (x), it expresses the existence of an element of the universe that makes the bounded formula true by replacing the variable ( x). In other words ∃ (x) A (x) ⇔ A (a), where a is the aforementioned element. From the above it follows that any existential quantifier not preceded by any universal quantifier can be eliminated if the dimensioning variable is replaced by a constant symbol that does not occur in the formula.
- If in an formula, an existential quantifieris preceded by universal quantifiers, as in Ɐ (x) Ɐ (y) ∃ (z) A (x, y, z), it expresses the existence of an element of the universe that makes true the bounded formula when substituting the variable (z). But this element is determined by x and y, that is, for each pair x and y that the element is taken it can be different. This dependency can be expressed as a functionthat takes ax and y as arguments. So:
Ɐ (x) Ɐ (y) ∃ (z) A (x, y, z) ⇔ Ɐ (x) Ɐ (y) A (x, y, f (x, y))
From the above it follows that every quantifier Existential preceded by universal quantifiers can be removed if the dimensioning variable is replaced by a function symbol that does not occur in the formula and that receives as arguments, all the variables delimited by the universal quantifiers that precede it.
The following example illustrates how to transform a formula of predicate calculus into an equivalent Skölem form:
Let the formula ∃ (x) Ɐ (y) ∃ (z) Ɐ (u) ∃ (v) [(¬S (x, y) v¬P (v, z)) ʌ (P (z, u) v S (z, y)) ʌ (¬P (u, x) v S (x, y))]
Since it can be seen that the formula is already in pre-attached normal form, then we proceed directly to eliminate the existential quantifiers (∃ (x) ∃ (z) se (v)). The first of these is not preceded by any universal quantifier, therefore when eliminating it, the variable (x) is replaced by a constant symbol that does not occur in formula (a), leaving:
Ɐ (y) ∃ (z) Ɐ (u) ∃ (v) [(¬S (a, y) v¬P (v, z)) ʌ (P (z, u) v S (z, y)) ʌ (¬P (u, a) v S (a, y))]
The next existential quantifier (∃ (z)), is preceded by Ɐ (y), which causes that when eliminating it, the variable (z) is replaced by a function symbol that does not occur in the formula and take as argument a, in this case f (y):
Ɐ (y) Ɐ (u) ∃ (v) [(¬S (a, y) v¬P (v, f (y))) ʌ (P (f (y), u) v S (f (y ), y)) ʌ (¬P (u, a) v S (a, y))]
Only one existential quantifier (∃ (v)) remains, which is preceded by Ɐ (y) and Ɐ (u), therefore when eliminating it, the variable (u) must be replaced by a function symbol that does not occur in the formula and take the variables y and y as arguments, in this case g (y, u), obtaining the Skölem form:
Ɐ (y) Ɐ (u) [(¬S (a, y) v¬P (g (y, u), f (y))) ʌ (P (f (y), u) v S (f ( y), y)) ʌ (¬P (u, a) v S (a, y))]
Clause sets
A clause is nothing more than a disjunction of literals. Thus, a set of clauses will be a set of literal disjunctions.
The transformation of a Skölem form into a set of clauses is therefore a fairly direct and simple procedure. First, all universal quantifiers are removed, this is perfectly possible since all variables are universally quantified, their omission does not create ambiguity.
Then each of the disjunctions is taken (the formula is in fnc) as a clause and the conjunctions are omitted. The example above:
Ɐ (y) Ɐ (u) [(¬S (a, y) v ¬P (g (y, u), f (y))) ʌ (P (f (y), u) v S (f ( y), y)) ʌ (¬P (u, a) v S (a, y))]
It would give rise to the following set of clauses:
¬S (a, y) v ¬P (g (y, u), f (y)),
P (f (y), u) v S (f (y), y),
¬P (u, a ) v S (a, y)}
