Predicate (1st order) Logic

It is relatively easy to check for logical consequence in proposition logic because propositional logic is not very expressive. It is desirable to have a more expressive logic in which to write the axioms and conclusions. A primary weakness of propositional logic is the lack of syntax for representing objects in the domain of interest; propositional logic only permits statements about the domain of interest, e.g., it is not possible to have a symbol for Socrates, rather it is possible only to make statements about Socrates. Associated with this is the absence of functional abstraction, e.g., it is not possible to refer to the brother of Socrates. A second weakness of propositional logic is that it does not provide variables which can be quantified over, e.g., it is not possible to represent the all men in All men are mortal by a variable which can range of the possible values of specific men. Similarly, it is not possible to claim the existence of something with a given property by representing that something by a variable, as in "There exists a prime number greater than 27".

1st order logic overcomes these weaknesses of propositional logic by providing a richer language. The cost of this increased expressivity is the loss of decidability for logical consequence. 1st order logic is semi-decidable, which means that if a formula is a logical consequence of a set of axioms, it is possible to show that it is. However, if a formula is not a logical consequence of a set of axioms, it may not be possible to show that it is not. In addition, 1st order logic requires more complex mechanisms for checking for logical consequence.

The Language of 1st order logic

A 1st order language consists of three sets of symbols: Prolog syntax is used here: variables start with upper case alphbetic, and functors and predicate symbols start with lower case alphabetic. Functors and predicate symbols are distinguished by the context, as described below. When referring directly to a functor or predicate symbol, its arity is given after a , e.g., in blah/2, blah is the functor or predicate symbol and the arity is 2.

Example 
V = { V : V starts with uppercase }
F = { geoff/0, jim/0, brother_of/1 }
P = { wise/1, taller/2 }

From the components of the language, two types of expressions are built. This is in contrast to propositional logic where only propositions exist. The first type of expression is terms. Terms are used to denote (possibly arbitrary) objects in the domain of interest. Terms thus correspond roughly to data in conventional programming. Terms are defined recursively by:

Example 
geoff
Person
brother_of(jim)
brother_of(brother_of(X))

Note that if there is a functor of arity greater than 0, then there is an infinite number of terms. As might be expected, ATP for 1st order logic is much easier if the number of terms is finite (in fact it reduces to ATP for propositional logic). For this reason, it is desirable to formulate ATP problems without any functors of arity greater than 0.

The second type of expression is atoms, which correspond to the propositions of propositional logic. Atoms decribe relationships between terms (objects in the domain). Atoms are defined by:

Example 
wise(geoff)
taller(Person,brother_of(jim))
wise(brother_of(brother_of(X)))

If the number of terms is infinite (which occurs if there is a functor of arity greater than 0), and there is a predicate symbol of arity greater than 0, then there is an infinite number of atoms.

Connectives are used to combine atoms into the formulae of 1st order logic. The connectives include all those used in propositional logic, and two new quantifiers:

Denoting arbitary 1st order formulae by uppercase variable letters, e.g., P, 1st order formulae are defined recursively by:

The precedence order of the above operators is ∀ ∃ ~ & | => <=>, i.e., ∀ and ∃ bind most tightly, down to <=>. This precedence ordering allows some brackets to be omitted, e.g., ∀X (clever(X) => pass(X) | lazy(X)) means ∀X (clever(X) => (pass(X) | lazy(X))). Note that the ()s round the (clever(X) => pass(X) | lazy(X)) are necessary, for otherwise the quantification would apply to only the clever(X).

Example 
wise(geoff)
~taller(Person,brother_of(jim))
wise(geoff) & wise(brother_of(brother_of(Person)))
~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person)))
wise(brother_of(brother_of(Person)) =>  wise(geoff)
wise(geoff) <=>  ~taller(Person,brother_of(jim))
(wise(geoff) & wise(brother_of(brother_of(Person)))) | wise(geoff)
∀Person ~taller(Person,brother_of(jim))
∃Person wise(brother_of(brother_of(Person)) => wise(geoff)

Atoms and the negations of atoms are called literals.

Example 
wise(brother_of(X))
~taller(geoff,jim)

Ground formulae are formulae that contain no variables.

Example 
wise(geoff)
wise(geoff) <=> ~taller(geoff,brother_of(jim))

The scope of a quantification is the formula which follows the quantification, e.g., the scope of ∃Person in
    ∃Person wise(brother_of(brother_of(Person)) => wise(geoff)
is
    wise(brother_of(brother_of(Person)).
A variable is bound if it occurs in a quantification or it is within the scope of a quantification of that variable. Otherwise a variable is free. A formulae that has no free variables is a closed formula; otherwise a formula is open.

Example
Person is bound in in the closed formula:
∀Person ~taller(Person,brother_of(jim))

Person is free in the open formula:
~taller(Person,brother_of(jim))

Person is bound and free in the open formula:
∀Person ~taller(Person,jim) | wise(Person)

Person is bound in the closed formula:
∀Person(~taller(Person,jim) | wise(Person))

A free variable in a expression can be instantiated with a term, thus binding the variable to that value and forming an instance of the expression.

Example
The free variable Person in:
~taller(Person,brother_of(jim))

can be instantiated with brother_of(geoff) to form the instance:
~taller(brother_of(geoff),brother_of(jim))

For ATP open formulae are not useful, because it is not possible to interpret (in the sense of giving meaning) open formulae. Open formulae can be closed by universal or existential quantification. This is done by placing either a universal or existential quantifier in front of the bracketed formula. The free standing quantifier notation is shorthand for a universal or existential quantification of every free variable in the formula.

Example
~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person)))

can be closed either universally:
∀(~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person))))

or existentially:
∃(~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person))))

In English universal quantification is usually meant if no explicit quantification is given, e.g., "Sheep are stupid" usually means "All sheep are stupid", not "There exists a sheep that is stupid".

Equality

Many domains require the use of the notion of equality. In 1st order logic equality statements use the equal/2 predicate, or infix =/2 and !=/2 predicates.

Example
  • Axioms
even(sum(two_squared,b))
two_squared = four
∀X (zero(X) => difference(four,X) = sum(four,X))
zero(b)

  • Conjecture
even(difference(two_squared,b))

Although the conjecture may seem like a logical consequence to humans, that's because humans "know" what equal means (even without knowing what the "math" means). In reality, many modern ATP systems do "know" what equal means, and for such systems it is not necessary to add in the axioms of equality.

Translation from English to 1st Order Logic

There is often a direct translation from a problem stated in a natural language to 1st order logic.

Example
Every student is enrolled in at least one course. Every professor teaches at least one course. Every course has at least one student enrolled. Every course has at least one professor teaching it. The coodinator of a course is a professor who is teaching it. If a student is enrolled in a course then the student is taught by every professor who teaches the course. CSC410 is a course. Michael is a student enrolled in CSC410. Victor is the coordinator of CSC410. Therefore, Michael is taught by Victor. 
V = { V : V starts with uppercase }
F = { michael/0, victor/0, csc410/0, coordinator_of/1 }
P = { student/1, professor/1, course/1, enrolled/2, teaches/2, taught_by/2 }
  • Every student is enrolled in at least one course.

    ! [S] : ( student(S) => ? [C] : ( course(C) & enrolled(S,C) ) )

  • Every professor teaches at least one course.

    ! [P] : ( professor(P) => ? [C] : ( course(C) & teaches(P,C) ) )

  • Every course has at least one student enrolled.

    ! [C] : ( course(C) => ? [S] : ( student(S) & enrolled(S,C) ) )

  • Every course has at least one professor teaching it.

    ! [C] : ( course(C) => ? [P] : ( professor(P) & teaches(P,C) ) )

  • The coodinator of a course is a professor who is teaching it.

    ! [C] : ( course(C) => ( professor(coordinator_of(C)) & teaches(coordinator_of(C),C) ) )

  • If a student is enrolled in a course then the student is taught by every professor who teaches the course.

    ! [S,C] : ( ( student(S) & course(C) & enrolled(S,C) )
             => ! [P] : ( ( professor(P) & teaches(P,C) ) => taught_by(S,P) ) )

  • CSC410 is a course.

    course(csc410)

  • Michael is a student enrolled in CSC410.

    ( student(michael) & enrolled(michael,csc410) )

  • Victor is the coordinator of CSC410.

    coordinator_of(csc410) = victor

  • Victor teaches Michael.

    taught_by(michael,victor)

Educational Example

For many more ideas and suggestions, see Peter Stuber's Translation Tips.

Exercises

Convert the following into 1st order logic:

The basic notion of set theory is membership of a set. Using a member/2 predicate, define set equality, intersection, union, power set, empty set, and diifference. For example, intersection is defined as: 

    ! [X,A,B] :
      ( member(X,intersection(A,B))
    <=> ( member(X,A)
        & member(X,B) ) )
Now write conjectures for transitivity of subset, associativity of set intersection, and distribution of intersection over union.

Equality Axioms

Example
  • Axioms
even(sum(two_squared,b))
two_squared = four
∀X (zero(X) => difference(four,X) = sum(four,X))
zero(b)

  • Conjecture
even(difference(two_squared,b))

Although the conjecture may seem like a logical consequence to humans, that's because humans "know" what equal means (even without knowing what the "math" means). However, there are many models of the axioms that are not a models of the conjecture, e.g., simply by making even(sum(four,b)) be FALSE. Such models are possible because the axioms are missing definitions for equality. These definitions are the axioms of equality, and must be included to force equality to have its usual meaning. They are:

∀X (X = X)
∀X ∀Y (X = Y => Y = X)
∀X ∀Y ∀Z ((X = Y & Y = Z) => X = Z)

∀X ∀Y ∀Z (X = Y => sum(X,Z) = sum(Y,Z))
∀X ∀Y ∀Z (X = Y => sum(Z,X) = sum(Z,Y))
∀X ∀Y ∀Z (X = Y => difference(X,Z) = difference(Y,Z))
∀X ∀Y ∀Z (X = Y => difference(Z,X) = difference(Z,Y))
∀X ∀Y ((X = Y & even(X)) => even(Y))
∀X ∀Y ((X = Y & zero(X)) => zero(Y))

In reality, many modern ATP systems do "know" what equal means, and for such systems it is not necessary to add in the axioms of equality.

Exercises

Convert the following into 1st order logic, and generate the required axioms of equality:

Someone who lives in Dreadbury Mansion killed Aunt Agatha. Agatha, the butler, and Charles live in Dreadbury Mansion, and are the only people who live therein. A killer always hates his victim, and is never richer than his victim. Charles hates no one that Aunt Agatha hates. Agatha hates everyone except the butler. The butler hates everyone not richer than Aunt Agatha. The butler hates everyone Aunt Agatha hates. No one hates everyone. Agatha is not the butler. Therefore : Agatha killed herself.

Interpretation

Interpretation of 1st order formulae requires a more complex structure than for propositional logic, because there are "component parts" of 1st order formulae. If the Herbrand base is finite (due to a finite Herbrand universe) then it is possible to assign truth values to elements of the Herbrand base. In this case logical consequence can be decided as for propositional logic, using a truth table. Otherwise, as is the case when the full expressive power of 1st order logic is used, a more complex structure is required. Henceforth only the latter, more complex, 1st order languages are considered.

An interpretation of a 1st order logic consists of three parts:

Example
One possible interpretation of the language 
V = { V : V starts with uppercase }
F = { geoff/0, jim/0, brother_of/1 }
P = { wise/1, taller/2 }
is 
D = { ,  }
F = { geoff → ,
      jim → ,
      brother_of() → ,
      brother_of() →  }
P = { wise() → TRUE,
      wise() → TRUE,
      taller(,) → FALSE,
      taller(,) → FALSE,
      taller(,) → TRUE,
      taller(,) → FALSE }

As with propositional logic, all the possible Rs can be presented as a truth table or a semantic tree.

Given an interpretation, the truth value of a closed formula can be determined, with respect to that interpretation. The procedure for ground formula is:

Example
Using the interpretation above, the ground formula
wise(geoff) <=> ~taller(geoff,brother_of(jim))

is interpreted as follows 

wise(geoff) <=> ~taller(geoff,brother_of(jim))
wise()  <=> ~taller(, brother_of())
wise()  <=> ~taller(, )
TRUE        <=> ~FALSE
TRUE        <=> TRUE
TRUE

Non-ground closed formulae are interpreted as follows:

Example
To interpret the universally quantified formula ∀Person (~taller(Person,jim) | wise(Person)), the universally quantified variable Person is instantiated to all the domain elements.
  • Person = 
    ~taller(,jim) | wise()
~taller(,) | wise()
~FALSE | TRUE
TRUE | TRUE
TRUE
  • Person = 
    ~taller(,jim)  | wise()
~taller(,) | wise()
~FALSE | TRUE
TRUE | TRUE
TRUE
The unquantified formula is TRUE with the quantified variable instantiated to each of the domain elements, thus the universally quantified formula is TRUE.

Example
To interpret the existentially quantified formula ∃Person ( wise(brother_of(brother_of(Person))) => wise(geoff)) the existentially quantified variable Person is instantiated to find a TRUE instance of the formula.
  • Person = 
    wise(brother_of(brother_of()) => wise(geoff)
wise(brother_of()) => wise()
wise() => wise()
TRUE => TRUE
TRUE
The unquantified formula is TRUE with the quantified variable instantiated to at least one of the domain elements, thus the existentially quantified formula is TRUE.

If the domain of the interpretation is finite, interpretation of closed 1st order formulae is a finite process. If the domain is inifinite it is not possible to determine that a universally quantified formula is TRUE, nor is it possible to determine that an existentially quantified formula is FALSE.

Some Interpretations

In general, an interpretation must have the structure discussed above. However, interpreting a formula in such a general structure can be very expensive. There are some simple interpretations in which the interpretation of a literal can be determined syntactically.

The Quest for Logical Consequence

To show that C is a logical consequence of Ax, it is necessary to:

For every 1st order language there is an infinite number of possible interpretations. New interpretations can be constructed by changing the domain and by changing the F and R mappings. Thus it is not possible to use the "table" method from propositional logic, as there is an infinite number of rows to check.

Satisfiability Preserving Transformations

One of the techniques for establishing that C is a logical consequence of Ax is to show that Ax ∪ {~C} is unsatisfiable. Thus the ability to detect that a set of formulae is unsatisfiable, is important. It may be difficult or impossible to show directly that a set is unsatisfiable. A satisfiability preserving transformation (SPT) takes a set of formulae and transforms it to a new set, such that if the original set is satisfiable then so is the transformed set. Conversely, if the transformed set is unsatisfiable then so is the original set.

If, by repetitive use, the application of SPTs produces a set that is obviously unsatisfiable (e.g., containing FALSE) from a set of formulae, then, iteratively, this means that the very original set is also unsatisfiable. If the original set is of the form Ax ∪ {~C}, this establishes that C is a logical consequence of Ax. The process of producing a set that is obviously unsatisfiable is called finding a refutation.

Logical Inference

An inference rule infers formulae from parent formulae.

An inference rule is sound if it infers only logical consequences of its parents.

The operation of applying a sound inference rule to parents from a set, and then adding the inferred formula back into the set, is a SPT (think why!). (There are other SPTs, but this is an important one.) Thus sound inference rules form the basis of a a simple algorithm for establishing logical consequence.

The basic saturation procedure is :

Form the set Ax ∪ {~C}
While a refutation has not been found
    Copy some formulae from the set
    Use sound inference rules to generate logical consequences from the formulae
    Put the logical consequences into the set
Note the "Copy", indicating that a formula may be used multiple times with a new set of variables each time.

An inference system is complete if, by repetitive use, it can infer every logical consequence of its input.

An inference system is refutation complete if, by repetitive use, it can infer FALSE (a contradiction) from every unsatisfiable set.

Note: A complete inference system can infer all logical consequences, while a refutation complete inference system can only check (via the unsatisfiability idea) for logical consequence.

Exam Style Questions

  1. What are the two major limitations of propositional logic?
  2. What are the three components of a 1st order logic language?
  3. Which or the following formulae are {ground, closed}?
    <insert some formulae here>
  4. What is important about closed formulae?
  5. Translate the following into 1st order logic:
    Suming, Yi, and Yury are students, and are the only three students. If a student works hard then they get a good grade. At least one of the students works hard. Therefore at least one student will get a good grade.
  6. Express the following scenario and conclusion in 1st order logic, in a form ready to be converted to clause normal form.
    There are some students who fail. If a student fails, then either there is a lecturer who has taught the student badly, or the student is stupid. No lecturer teaches any student badly. Therefore there is some student who is stupid.
  7. In what circumstances is it necessary to add the axioms of equality to the formulae of a problem?
  8. Name the five (groups of) axioms of equality.
  9. What axioms of equality are needed with this formula?
    p(X) | ~p(f(cat,dog)) | equal(X,cat)
  10. What are the three components of an interpretation of a first order language? Give an example for the language: 
    V = { V : V starts with uppercase }
F = { coke/0, pepsi/0, competitor/1 }
P = { fizzy/1, sells-more/2 }
  11. Given the 1 st order logic language: 
    V = { V : V starts with uppercase }
F = { holden/0, ford/0, honda/0 main_competitor/1 }
P = { fast/1, faster/2 }
    and the interpretation: 
    D = { commodore, laser, prelude }
F = { holden → commodore,
      ford → laser,
      honda → prelude,
      main_competitor(commodore) → prelude,
      main_competitor(laser) → prelude,
      main_competitor(prelude) → commodore }
P = { fast(commodore) → TRUE, 
      fast(laser) → FALSE,
      fast(prelude) → TRUE,
      faster(commodore,commodore) → FALSE,
      faster(commodore,laser) → TRUE,
      faster(commodore,prelude) → TRUE,
      faster(laser,commodore) → FALSE,
      faster(laser,laser) → FALSE,
      faster(laser,prelude) → FALSE,
      faster(prelude,commodore) → FALSE,
      faster(prelude,laser) → TRUE,
      faster(prelude,prelude) → FALSE }
    Show the steps of the interpretation of:
    • faster(main_competitor(laser),commodore)
    • fast(main_competitor(main_competitor(prelude))
    • forall X ( faster(main_competitor(X),laser) & fast(X) )
    • exists X ( fast(main_competitor(main_competitor(X))) | forall Y faster(X,Y) ) )
  12. What are the positive and negative interpretations?
  13. Explain why truth tables cannot be used to establish logical consequence in lst order logic.
  14. What does it mean for an inference system to be {sound, complete, refutation complete}? Which of these properties are desireable in an CNF based ATP system?
  15. Explain how unsatisfiability can be used to establish logical consequence in classical logic.