Predicate calculus and computing
Predicate calculus also uses many of the rules that propositional calculus uses. One of the most noticeable are the De Morgan’s laws. The main laws involve the negation of a conjunction and the negation of a disjunction. They are as follows: [4]
¬ ( F ∨ G )
is equivalent to
¬ F ∧ ¬ G
If we replace F and G , which are currently propositions, with predicates, De Morgan’s law still applies. The same operation is true with the quantifiers ∃ and ∀ . This is shown below:
¬( ∀ α ( P ( α )))
is equivalent to
∃ α (¬( P ( α )))
These rules of negation also work in reverse. For example, ∧ would become ∨ and ∃ would become ∀ . When working with formulas, it is important to know the difference between a free variable and a bound variable. [5] For example, in the formula ∀ μ P ( ν , μ ), the variable ν is free, whereas the variable μ is bound. From this example, it is easy to see that a free variable is a variable that is not quantified. This is important because it is a simple way of checking whether a formula is true or not. If a formula contains a free variable, it is impossible to check whether it is true or not, because the free variable may, or may not exist. In the formula above, we cannot tell whether it is true. However, if we added a quantifier to the ν variable, we are able to state that the formula is satisfiable . For example, ∀ μ ∃ ν P ( ν , μ ) contains no free variables and so it is satisfiable. It is also important to note the difference between satisfiable and valid . [1] A formula is satisfiable if it has at least one interpretation that will render the formula true, whereas a formula is valid if it is true under all possible interpretations. It is also possible to derive formulas (hereafter called a theorem) from other formulas (hereafter called axioms) using the resolution method. To begin the resolution method, one must start with the first axioms. These axioms are called clauses and they are a series of disjunctions of predicates, or their negations. [3] For example, take the two clauses (¬ ψ ( α ) ∨ φ ( α , ν ) ∨ β ( ν )) and ( ψ ( α ) ∨ ϕ ( α )). In the second clause, we can see the predicate ψ ( α ) appears, and in the first clause, the negation is seen. Because only one predicate with its negation appears within the different clauses, we can resolve the two clauses into one by ‘ removing ’ the two predicates ψ ( α ) and ¬ ψ ( α ) and take the disjunction of the remaining predicates. This is shown below:
(¬ ψ ( α ) ∨ φ ( α , ν ) ∨ β ( ν )) ( ψ ( α ) ∨ ϕ ( α )).
( φ ( α , ν ) ∨ β ( ν ) ∨ ¬ ϕ ( α ))
The lines (or sometimes arrows) help improve readability and show which axioms have been used. This is particularly handy when resolution becomes more complicated, as the clauses above were chosen to make the explanation easier. Take, for example, the predicates ¬ β ( ρ, f ( υ )) and β ( υ , α ) that appear in two arbitrary clauses. In order to begin resolving these clauses, we have to perform unification on the two
227
Made with FlippingBook - Online catalogs