Satisfiability relation for predicate logic

CIS 301. Satisfiability relation for predicate logic.

Recall the grammar for predicate logic:

phi ::= P(t,t,...,t) | phi | phi  phi | phi  phi | phi  phi | x phi | x phi,

where P is from a set of predicate symbols and t is a term generated by the grammar

t ::= c | x | f(t,t,...,t)

where c is from a set of constant symbols, x is any variable (x,y,z, etc), and f is a function symbol. An example term is

+(1,*(y,+(1,x)))

where 1 is a constant symbol and + and * are function symbols requiring two arguments. An example of an expression of the form P(t,t,...,t) is

<(+(1,*(y,+(1,x))),1)

where < is a predicate sybmbol requiring two arguments. Often we write such predicate expression in infix notation, so the above reads as

1 + y * (1 + x)  <  1.

A model for predicate logic formulas:

A model M for a set of predicate logic formulas requires

a set, A, of values or objects that these formulas "talk about",
an interpretation of all the constant symbols in these formulas; since constant symbols intent to identify fixed values, we need to associate with each such symbol c a value c^M drawn from A,
similarly, for any function symbol, f, of n arguments, we need a concrete function, f^M, that maps n-tuples of values over A to a value in A,
similarly, for any predicate symbol, P, of n arguments, we need a concrete predicate, P^M, which is a subset of the set of all n-tuples of values over A; we say that P "is true" for a tuple, if that tuple is in the set P^M.

As an example, consider the formula

x  y (1 + y * (1 + x)  <  1)

over the "standard" model, N, of all natural numbers (excluding zero), such that all constant, function, and predicate symbols have the meanings that you would expect: 1^N is the number "one", +^N and *^N are the "addition" and "multiplication" of natural numbers, respectively, and <^N is the relation "strictly less than".

Evaluation of formulas in a model:

A basic question is whether a predicate logic formula is "true" with respect to a given model. For example, is the formula above true for the "standard" model N? We say that the formula phi is "true" w.r.t. the model M, if, and only if, the satisfaction relation

M  phi

holds. Our aim is to define this satisfaction relation in an algorithmic way, by structural induction over the parse tree of phi. Returning to our example, to decide whether

N  x  y (1 + y * (1 + x)  <  1)

holds, we mean to decide whether

N  y (1 + y * (1 + x)  <  1)

holds for all choices of x; that is to say, this should hold no matter what value we choose for x. Evidently, we need a tool for binding x to a value k (here: some natural number). We write [x --> k] for such a binding. Therefore, we need to refine our satisfaction relation with such bindings:

M  _{[x --> a]...} phi

The dots indicate that a binding may bind more than one variable. In our example, we need to determine whether

N _{[x --> k]} y (1 + y * (1 + x)  <  1)

holds for all natural numbers k. Let us consider an instance of k, say, 4. Then the relationship

N _{[x --> 4]} y (1 + y * (1 + x)  <  1)

holds if, and only if, we can finds some natural number m, such that

N _{[x --> 4][y --> m]} (1 + y * (1 + x)  <  1)

holds. At this point, we can settle the latter question by consulting the meaning of 1, +, and *; the left hand side, 1 + y * (1 + x), of the inequality evaluates to a number bigger than one, as it adds at least five to one (since x evaluates to four and y has to be at least one). Thus,

N _{[x --> 4][y --> m]} (1 + y * (1 + x)  <  1)

cannot hold for any value m whatsoever. Therefore, we conclude that

N _{[x --> 4]} y (1 + y * (1 + x)  <  1)

does not hold. But since 4 is an instance of x, this leads to the conclusion that

N  x  y (1 + y * (1 + x)  <  1)

does not hold either, since it is false for at least one choice of x (namely "four"). Note that this formula is not so hard to evaluate, for any value for x would defeat this formula.

Exercise:

After reading the above, try to determine whether

N  x  y (1 + y * (1 + x)  <  (x + x) + y)

holds.

Revisiting truth tables:

The above explained, by means of a simply example, how to compute

M  phi

if phi is of the form P(t,t,...,t), or

x phi, or

x phi. Inspecting the grammar for predicate logic, we realize that the only other cases are negation, disjunction, conjunction, and implication. But for these we define the satisfaction relation in accordance with their semantics from chapter 1. For example,

M  phi

holds if, and only if,

M  phi

does not hold. Similary,

M  phi  psi

holds if, and only if,

M  phi

and

M  psi

hold. Can you define the satisfaction relation for disjunctions and
implications?