First-Order Predicate Logic(FOPL)

First-Order Predicate Logic

The type of predicate calculus that we have been referring to is also called firstorder predicate logic (FOPL).

A first-order logic is one in which the quantifiers and can be applied to objects or terms, but not to predicates or functions.

So we can define the syntax of FOPL as follows. First,we define a term: A constant is a term.

A variable is a term. f(x1, x2, x3, . . . , xn) is a term if x1, x2, x3, . . . , xn are all terms.

Anything that does not meet the above description cannot be a term.

For example, the following is not a term: x P(x). This kind of construction we call a sentence or a well-formed formula (wff), which is defined as follows.

In these definitions, P is a predicate, x1, x2, x3, . . . , xn are terms, and A,B are wff ’s. The following are the acceptable forms for wff ’s:

P(x1, x2, x3, . . . , xn)

ï¿¢A

A ∧ B

A ∨ B

A→B

A↔ B

(  x)A

( x)A

An atomic formula is a wff of the form P(x1, x2, x3, . . . , xn).

Higher order logics exist in which quantifiers can be applied to predicates and functions, and where the following expression is an example of a wff:

(  P)(  x)P(x)

Soundness

We have seen that a logical system such as propositional logic consists of a syntax, a semantics, and a set of rules of deduction.

A logical system also has a set of fundamental truths, which are known as axioms.

The axioms are the basic rules that are known to be true and from which all other theorems within the system can be proved.

An axiom of propositional logic, for example, is A→(B→A)

A theorem of a logical system is a statement that can be proved by applying the rules of deduction to the axioms in the system.

If A is a theorem, then we write ├ A

A logical system is described as being sound if every theorem is logically valid, or a tautology.

It can be proved by induction that both propositional logic and FOPL are sound.

Completeness

A logical system is complete if every tautology is a theorem—in other words, if every valid statement in the logic can be proved by applying the rules of deduction to the axioms. Both propositional logic and FOPL are complete.

Decidability

A logical system is decidable if it is possible to produce an algorithm that will determine whether any wff is a theorem. In other words, if a logical system is decidable, then a computer can be used to determine whether logical expressions in that system are valid or not.

We can prove that propositional logic is decidable by using the fact that it is complete.

We can prove that a wff A is a theorem by showing that it is a tautology. To show if a wff is a tautology, we simply need to draw up a truth table for that wff and show that all the lines have true as the result. This can clearly be done algorithmically because we know that a truth table for n values has 2n lines and is therefore finite, for a finite number of variables.

FOPL, on the other hand, is not decidable. This is due to the fact that it is not possible to develop an algorithm that will determine whether an arbitrary wff in FOPL is logically valid.

Monotonicity

A logical system is described as being monotonic if a valid proof in the system cannot be made invalid by adding additional premises or assumptions.

In other words, if we find that we can prove a conclusion C by applying rules of deduction to a premise B with assumptions A, then adding additional assumptions Aï¿¢ and Bï¿¢ will not stop us from being able to deduce C.

Monotonicity of a logical system can be expressed as follows:

If we can prove {A, B} ├ C,

then we can also prove: {A, B, A_, B_} ├ C.

In other words, even adding contradictory assumptions does not stop us from making the proof in a monotonic system.

In fact, it turns out that adding contradictory assumptions allows us to prove anything, including invalid conclusions. This makes sense if we recall the line in the truth table for →, which shows that false → true. By adding a contradictory assumption, we make our assumptions false and can thus prove any conclusion.