First-order (predicate) 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 first 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". A second 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.

1st order logic overcomes these two 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. 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:

V is a set of variables (for our purposes, infinite)
F is a set of functors, each of which has an arity. The arity specifies the number of arguments they take (see below). Functors of arity 0 are constants.
P is a set of predicate symbols, each of which has an arity. Predicate symbols of arity 0 are propositions.

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 }

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:

A functor of arity 0 (a constant) is a term
A variable is a term
A functor with the appropriate number of terms as arguments, is a term.

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:

A predicate symbol of arity 0 (a proposition) is an atom
A predicate symbol with the appropriate number of terms as arguments, is an atom.

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:

~ for negation.
∧ or & for conjunction.
∨ or | for disjunction.
=> for implication.
<=> for equivalence.
<~> for exclusive or.
∀ or ! for universal quantification. This corresponds to saying "for all" in English, e.g., ∀X (man(X) => mortal(X)) says "for all objects X, X is a man implies X is mortal". It is easy to remember that ∀ means "for all" by noticing that the ∀ is an upside down A from for All.
∃ or ? for existential quantification. This corresponds to saying "there exists" in English, e.g., ∃X (prime(X) & greater(X,27)) says "There exists an object X such that X is a prime number and X is greater than 27". It is easy to remember that ∃ means "there exists" by noticing that the ∃ is a backwards E from there Exists.

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

Atoms are formulae
If P and Q are formulae then ~P, P & Q, P | Q, P => Q, P <=> Q, and (P) are formulae.
If P is a formula and X is a variable, then ∀X P and ∃X P are formulae. The ∀X and ∃X are called quantifications of X, and they quantify all occurrences of X in P. The quantification has precedence over any earlier (to the left) quantification of X. Variables with the same name but which are quantified by different quantifiers, are different variables.

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)

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)

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))

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))

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))

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))))

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".

Substitutions

A substitution θ is a finite set of the form {X₁/t₁,...,X_n/t_n} where each X_i is a distinct variable and each t_i is a term (or more generally, a member of some given set of objects) not containing X_i. Each element X_i/t_i is called a binding for X_i. θ may be applied to an formula F to obtain Fθ, the expression obtained from F by similtaneously replacing each occurrence of the X_is in F by t_i. Similarly Sθ may be obtained from a set S of formulae.

A substitution can be applied to another substitution to form their composition. Let θ = {X₁/t₁,...,X_n/t_n} and σ = {Y₁/s₁,...,Y_n/s_n} The variables X_i must be distinct from the variables Y_i, and no X_i can appear in a s_i. The composition θσ is formed by applying σ to the t_i, and combining the two sets. For example, let
    θ = {P1/jim,P2/brother_of(P4)}
and
    σ = {P3/brother_of(P5),P4/geoff}.
Then
    θσ = {P1/jim,P2/brother_of(geoff),P3/brother_of(P5),P4/geoff}.

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. In order to make such a translation, it is necessary to:

Determine the predicates and functors of the 1st order language.
- Objects often correspond to constants
- Relationships that identify exactly one thing often correspond to functors
- Properties and activities often correspond to predicates. Relationships that identify a set of things often correspond to predicates.
Translate the axioms.
Make appropriate definitions for the predicates and functors.
Translate the conjecture.

Example
There is a barbers' club that obeys the following three conditions:

Four of the members are named Guido, Lorenzo, Petrucio, and Cesare.
If any member A has shaved any other member B - whether himself or another - then all members have shaved A.
Guido has shaved Cesare.
Prove Petrucio has shaved Lorenzo

V = { V : V starts with uppercase } F = { guido/0, lorenzo/0, petrucio/0, cesare/0 } P = { member/1, shaved/2, all_shaved/1 }

Four of the members are named Guido, Lorenzo, Petrucio, and Cesare.
member(guido)
member(lorenzo)
member(petrucio)
member(cesare)

If any member A has shaved any other member B - whether himself or another - then all members have shaved A.
∀M1∀M2 ( (member(M1) & member(M2) & shaved(M1,M2)) => all_shaved(M1) )

Guido has shaved Cesare.
shaved(guido,cesare)

Definitions
∀M1 ( all_shaved(M1) <=> ( member(M1) & ∀M2 (member(M2) => shaved(M2,M1)) ) )

Petrucio has shaved Lorenzo.
shaved(petrucio,lorenzo)

Example
There is a barbers' club that obeys the following three conditions: Four of the members are named Guido, Lorenzo, Petrucio, and Cesare. If any member A has shaved any other member B - whether himself or another - then all members have shaved A. Guido has shaved Cesare. Prove Petrucio has shaved Lorenzo
V = { V : V starts with uppercase } F = { guido/0, lorenzo/0, petrucio/0, cesare/0 } P = { member/1, shaved/2, all_shaved/1 }
Four of the members are named Guido, Lorenzo, Petrucio, and Cesare. `member(guido)` `member(lorenzo)` `member(petrucio)` `member(cesare)` If any member A has shaved any other member B - whether himself or another - then all members have shaved A. `∀M1∀M2 ( (member(M1) & member(M2) & shaved(M1,M2)) => all_shaved(M1) )` Guido has shaved Cesare. `shaved(guido,cesare)` Definitions `∀M1 ( all_shaved(M1) <=> ( member(M1) & ∀M2 (member(M2) => shaved(M2,M1)) ) )` Petrucio has shaved Lorenzo. `shaved(petrucio,lorenzo)`

Exercises

Convert the following into 1st order logic:

Osama Bin Laden is a terrorist. If someone is a terrorist and is dangerous, then his leader is a terrorist and is dangerous. There are some terrorists who are their own leader. Dangerous people care about only themselves, or about no-one (not even themselves!). Everyone has one leader, but might care about many people. Prove that if Osama Bin Laden cares about George Bush then Osama Bin Laden is not dangerous.

Wolves, foxes, birds, caterpillars, and snails are animals, and there are some of each of them. Also there are some grains, and grains are plants. Every animal either likes to eat all plants or all animals much smaller than itself that like to eat some plants. Caterpillars and snails are much smaller than birds, which are much smaller than foxes, which in turn are much smaller than wolves. Wolves do not like to eat foxes or grains, while birds like to eat caterpillars but not snails. Caterpillars and snails like to eat some plants. Prove that there is an animal that likes to eat a grain eating animal.

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

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))

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 "maths" 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:

Reflexivity - everything equals itself
Symmetry - If X equals Y then Y equals X
Transitivity - If X equals Y and Y equals Z, then X equals Z

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

Function substitution - If X equals Y then f(X) equals f(Y). For every argument position of every functor.
Predicate substitution - If X equals Y and p(X) is TRUE, then p(Y) is TRUE For every argument position of every predicate.

∀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))

Some 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:

D_I is the domain of the interpretation.
F_I is a mapping from function symbols in F to functions from D_I^* to D_I.
P_I is a mapping from predicate symbols in P to functions from D_I^* to {TRUE,FALSE}.

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_I = { , } F_I = { geoff → , jim → , brother_of() → , brother_of() → } P_I = { wise() → TRUE, wise() → TRUE, taller(,) → FALSE, taller(,) → FALSE, taller(,) → TRUE, taller(,) → FALSE }

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_I = { , } F_I = { geoff → , jim → , brother_of() → , brother_of() → } P_I = { 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:

Map all constants to the domain.
Repeatedly map functions of domain elements to domain elements, until only predicates of domain elements remain.
Map the predicates of domain elements to truth values.
Combine the truth values according to the truth tables for the connectives. Note that as this procedure is for ground formulae, quantifiers do not need to be interpreted here.

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

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:

A universally quantified formula is TRUE iff the unquantified formula is TRUE with the quantified variable instantiated to each of the domain elements.
An existentially quantified formula is TRUE iff the unquantified formula is TRUE with the quantified variable instantiated to at least one of the domain elements.

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 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.

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 positive interpretation maps all atoms to TRUE.
The negative interpretation maps all atoms to FALSE.
A predicate partition, which divides the predicate symbols of the 1st order language into two partitions P₁ and P₂, map atoms whose predicate symbols are in P₁ to TRUE and atoms whose predicate symbols are in P₂ to FALSE.

The Quest for Logical Consequence

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

Show that every model of Ax is a model of C
OR
Show that S' = Ax U {~C} is unsatisfiable.
OR
Show that C can be soundly inferred from Ax.

For every 1st order language there is an infinite number of possible interpretations, so it is not possible to check every interpretation explicitly. It also turns out the searching for C from Ax is not as effective as searching for a contradiction from Ax U {~C}.

Show that S' is unsatisfiable.

Exam Style Questions

What are the two major limitations of propositional logic?
What are the three components of a 1st order logic language?
Which or the following formulae are {ground, closed}?
<insert some formulae here>
What is important about closed formulae?
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.
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.
In what circumstances is it necessary to add the axioms of equality to the formulae of a problem?
Name the five (groups of) axioms of equality.
What axioms of equality are needed with this formula?
p(X) | ~p(f(cat,dog)) | equal(X,cat)
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 } 
```

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 }
R = { 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) ) )

What are the positive and negative interpretations?
Explain why truth tables cannot be used to establish logical consequence in lst order logic.