CS157 - Frequently Asked Questions

Table of Contents

Problem set FAQs will be posted on the main page in the problem sets section.

Propositional Logic

Propositional Resolution

On page 20 (page 10 in the PDF) of the slides entitled "Introduction" it says that only one pair of symbols that are repeated on both sides of the inferred implication can be dropped. What is the reasoning behind this? Why not more?

Answer:
A rule of inference must be valid, i.e. if the rule tells you that from phi you can infer psi, then it should be that indeed phi |= psi (semantically). Propositional resolution as stated is valid, but not if you drop more than one pair.
E.g. from the premises:
p & q => r
s => p|q
we cannot drop both p and q and infer s=>r
(if we know s, we know p or q, but not p & q, so we cannot infer r)
(an interpretation which shows this: assigns true to s,p and false to q,r)

Confusion: Set of sentences versus a clause

Refer to the definition of logical entailment. Notice that the thing on the left of the |= is just a set of sentences, NOT a clause, as used in Resolution. A set of sentences on the left of |= behaves like a conjunction of all the sentences in the set, whereas a clause in Resolution has the meaning of a disjunction (and besides, a clause may only include literals, i.e. propositional constants and their negations). So, {p,q} |= (p & q) does NOT mean (p | q) |= (p & q). See also section "Empty Clause vs. Empty Set of Sentences".

"Unless"

A message from Mike:

Sorry to everyone for bobbling the "unless" example in class. As we discovered together, the version on the slide I showed was incorrect. I have since fixed this and placed the correct translation in the slides on the website.

The "unless" construct in English is complex. There is a basic (weak) meaning that pretty much everyone agrees to, and there is an extended (stronger) version that is occasionally but not always intended.

The statement that "p is true unless q is true" can be rephrased as "p is true if q is not true", i.e. -q => p. In the weak interpretation, that is the entire meaning; the statement says nothing at all about the case when q is true; p may be true or p may be false in that case.

In the strong interpretation, p is furthermore required to be false when q is true, i.e. q => -p. The strong interpretation is equivalent to the sentence "p unless q" as "p is true unless q is true in which case p is false". Note that, in this case, the interpretation is (p <=> -q) or, equivalently, (p xor q), as someone mentioned in class.

Example of weak interpretation: A raven can fly unless it is sick, in which case it may or may not be able to fly well depending on how hardy it is.

Example of strong interpretation: A raven is black unless it is an albino. Equivalent sentence: A raven is black unless it is an albino in which case it is white (i.e. no black).

You will not pass this course unless you understand these examples.

Relational Logic

Functions and Relations

It's been mentioned in class and in the texts that "a function is a special kind of relation". In some sense, I can see why this is true.. a n-ary function is *like* an (n+1)-ary relation, etc. However, in another important sense it seems false, since when we apply a function to a set of terms, the result is a functional term and *not* a relational sentence. On the other hand, when we apply a relation to a set of terms, the result *is* a relational sentence. Is this true, and is this one (important) distinction between functions and relations?

Answer: You got it exactly right.

Determining the truth value of a sentence

Added 2006-10-19.

When evaluating whether a sentence is true or false, be sure to keep in mind that the truth value of a sentence only makes sense in the context of a particular universe, interpretation and variable assignment. This is particularly important when you are trying to see if sentences are contingent, valid or unsatisfiable.

Empty domain of discourse?

Added 2007-10-24.

∀x. p(x) is true in the empty domain (it is true of all objects, doesn't matter if there aren't any -- it is trivially true). It is true in much the same way as an empty conjunction is true. That said, we do not allow for empty domains of discourse, since it wouldn't make for terribly interesting logical reasoning.

You can get the same effect, though, by doing something like:

∀x. (type(x) ⇒ quality(x))

where you are talking about objects typed by 'type', with some given 'quality'. Then, if type(x) is true of nothing, you end up with a true universal sentence.

Implicit Universal Quantification

Added 2007-10-24.

Universal quantification is semantically, not syntactically, implicit. Just because you see a free variable in a sentence doesn't mean you can add a universal quantifier in front of the sentence and obtain the exact same thing. The implicit quantifier is semantic: it is implicit only because the semantic rules require us to iterate over all variable assignments when we want to check truth in some interpretation i.

Binding and Substitutability

Question 1

Question: The quantifier that is mentioned in the definition (slide 10, lecture 8) refers specifically to an existential quantifier, right? My impression was that a universal quantifier wound not bind t.

Answer: No. Both the existential and the universal quantifiers are relevant for this definition.

Another way to see the definition of substitutability is: a term tau can be safely substituted for a variable occurrence v in phi iff every variable in tau remains unbound after the substitution.

Question 2

Question: Consider the sentence psi: p(f(g(y),a)) & Ax.q(y,x) & Ey.r(y) (with a object constant, and x,y, variables)
What are the free occurrences of y in psi and what are the bound occurrences (an occurrence of a variable is bound if it is within the scope of a quantifier that binds it; and it is free otherwise).
Answer: The first two occurrences are free, the third is bound by Ey.
Notice: The term f(a,g(x)) is substitutable only in the first free occurrence of y. It is not substitutable in the second occurrence of y, because then x in the term would become bound (i.e. x is bound in Ax.q(f(a,g(x)),x)). And the third occurrence of y in psi is a bound occurrence and so by definition is never substituted.
Notice: We can find another formula phi that is logically equivalent to psi (i.e. phi <=> psi is a logically valid sentence) but in which the term can be substituted, by renaming the bound occurence of x to z: phi = p(f(g(y),a)) & Az.q(y,z) & Ey.r(y). Notice that free occurrences of variables remain the same; it is only bound variables that we rename (this is called "renaming of bound variables" or "alpha-renaming").
Now we can substitute the term for y in the new phi and get: p(f(g(f(a,g(x))),a)) & Az.q(f(a,g(x)),z) & Ey.r(y). Notice that x in the term remains free after the substitution (whereas if we had used psi, x in the term would become bound).

Notice: In Ax.(p(x) & Ex.q(x)), the first occurrence of x is bound by Ax, while the second is bound by Ex. It's like local shadowing in programming languages. (See also comment in Lecture errata on slide 13 of lecture 5).

Question 3

Added 2006-10-17.

Question: Why is mother(x) free for y in the sentence Ax.Ay.l(x,y) & Ez.h(z,y)?

Answer:
Here's the expanded definition of τ being free for ν in φ ("expanded" because I unpacked the 'bound' part):

A term τ is substitutable for ν in φ iff τ does not contain a variable μ OR there is no free occurrence of ν in phi OR the free occurrence of ν in φ does not lie in the scope of a quantifier of μ.

So let's look at the sentence:

φ = Ax.Ay.l(x,y) & Ez.h(z,y)

We're checking that τ=mother(x) is free (substitutable) for y in φ:

Since the third condition is true, mother(x) is free for y in φ.

Searching for a formal proof

When searching for a formal proof (both in propositional and in relational logic), try searching backwards. How would a formal proof look like if the conclusion were on the last line? How would one ore two previous-to-last lines look like? What inference rules could produce the conclusion from other sentences? What axiom parts does the conclusion match? These questions will help you generate subgoals, i.e. other sentences that, if you proved them, you'd have a proof for the desired conclusion. And then keep searching backwards from those subgoals. You can also combine this with searching forward: starting from the premises and axioms and applying rules of inference to get more conclusions.

Exampe translation from English

Translate the following english sentences into relational logic. 
Object constant: 0
Relations:
   W(x): x is a whole number, i.e. 1, 2, 3, ...
   N(x): x is a natural number, i.e. 0, 1, 2, 3, ...
   Q(x): x is a rational number
   R(x): x is a real number
   x > y: x is greater than y

(a) "Every natural number greater than 0 is a whole number."
Ax.(N(x) & x>0 => W(x))

(b) "Some real numbers are rational numbers, but some aren't."
Ex.(R(x) & Q(x)) & Ex.(R(x) & ~Q(x))

(c) "For every pair of natural numbers there is a rational number between them."
Ax.Ay.( N(x) & N(y) => Ez.(Q(z) & ((y > z & z > x) | (x > z & z > y) )))

Translating the english verbatim gives you what is above. If you translated the mathematical fact that for every pair of distinct natural numbers there is a rational number between them, you would conjoin (x>y | y>x) to the left hand side of the implication.

Universal Generalization

Note: If you want to apply Universal Generalization on phi, the result is just Ax.phi (for any x, no matter if it appears in phi or not). Make sure you apply the rule on the entire phi, not just on part of it. This is true for all other rules of inference as well (like Modus Ponens).

How to determine validity

General way: Assume the sentence is not valid and can be false in some interpretation and assignment, and then either reach a contradiction (in which case it's valid), or reach a counterexample. Work by opening up the definitions (see lecture 6).

Example: Is Ax.Ay.(p(x)=>p(y)) valid?
Answer: No.
Intuitive explanation: It's not true in general that for any two elements, if p is true of one then p is true of the other.
Systematic explanation: Suppose that for some i and v, t_iv(Ax.Ay.(p(x)=>p(y)))=false.
That means (by definition of the meaning of Ax) that for some element alpha in the universe of discourse, t_iv1(Ay.(p(x)=>p(y)))=false, where v1 is like v except v(x)=alpha.
So that means, for some element beta in the universe of discourse, t_iv2(p(x)=>p(y))=false, where v2(x)=alpha and v2(y)=beta.
So that means t_iv2(p(x))=true and t_iv2(p(y))=false.
So that means t_iv2(x) is in i(p) and t_iv2(y) is not in i(p).
So that means alpha is in i(p) and beta is not in i(p).
So this gives as instructions on how to build a countermodel: take |i|={*,%} and i(p)={*}. If you take v2(x)=* and v2(y)=% then t_iv2(p(x)=>p(y))=false. So that means (going backwards) that t_iv2(Ax.Ay.(p(x)=>p(y)))=false.

If instead you tried to start with (Ax.p(x))=>(Ay.p(y)) and assumed it's false under some interpretation and assignment, you'd reach a contradiction, showing the sentence is true under all interpretations and assignments, i.e. valid.

Language equality vs. Meta-equality

Added 2006-10-19.

In relational logic we often speak of equality, e.g. x=x or x+1=s(x). Make sure to distinguish equality in the language from meta-equality. The first is a relation in the interpretation just like any other, and is therefore subject to the normal rules of interpretation; for instance an interpretation could say that 1=2! That said, we generally only use "normal" definitions of equality, unless specified otherwise. The "normal" definition is as follows: τ1 = τ2 iff the terms τ1 and τ2 refer to the same object in the universe of discourse. Meta-equality refers to meta-objects, such as sentences, e.g. φ= α ∨ β, which means that the sentence φ is the literal string of characters α ∨ β.

Strategies

ICE vs. ECE

Added 2006-11-09.

Recall that ICE (identical clause elimination) is a strategy we used in propositional logic where you discard a clause that you have seen before. This prevents unnecessary duplication of work.

ECE (equivalent clause elimination) is the same concept but applied to relational logic. Let's say we start with clause {p(x)}. Later on, we might get a clause like {p(y)}. Note that these are identical clauses modulo the name of the variable. We want therefore a way to remove the second clause, to keep the same advantage as ICE.

ECE works just like ICE except for the following: two clauses φ and ψ are considered to be "identical" (equivalent) if there is a variable renaming τ such that φτ = ψ. (Note that this is syntactic equality, not equivalence.) Recall that a variable renaming is a substitution, except you are only allowed to bind variables to other variables.

You might want to look at the section on variable renaming in general to get more insight into this process.

Unification

General

Added 2006-11-09.

MGU Algorithm

Added 2006-11-09.

For the implementation-minded, some clarifications on the MGU algorithm presented in class:

Variables

Added 2006-11-09.

It's important to realize that if two separate clauses have a variable with the same name, that similarity is completely superfluous: the variables are not the same. Consider these two clauses: {p(a,x)} and {¬p(x,b)}. While doing resolution, we unify straightforwardly to {p(a,b)} by binding the first x to b and the second x to a.

But to do so, you have to distinguish between x1 and x2. That is why variable renaming is a crucial part of the resolution rule, and that is also why we standardize variables before dropping the universal quantifiers during INSEADO.

In general, a variable's name only has meaning with respect to its "lexical scoping". For instance, in the sentence p(x) => ∀x. p(x), the first x is not the same as the second one because the second lies in a different lexical scope.

Note that the process of unification per se does not rename variables; the renaming ("uniquefication" as it were) is a step in the resolution algorithm, not unification.

Substitutions

Cascading substitutions

Added 2006-11-09.

Sometimes you get a substitution of the form σ = {z ← x, x ← a. Suppose you were to apply this substitution to p(z,x). The correct result is p(a,a). The reason is that you need to "cascade" the substitutions; if z takes the value x, you need to make sure that you haven't constrained x to be some other value. It would be incorrect to write p(x,a). This has particularly important consequences anytime you are trying to unify two expressions.

General

Atoms, ground, terms, etc.

Added 2006-11-07.

Some useful definitions:

Empty Clause vs. Empty Set of Sentences

Added 2007-10-16.

The meaning of an empty set depends on the context. In resolution, {} means "empty clause". The definition of the semantics for a clause says that a clause is true when at least one of its disjuncts is true. The empty clause has no disjuncts, and therefore the clause is false.

In the context of entailment, {} means the empty set of sentences. A set of sentences is, basically, imposing constraints on the interpretations that can be models. (For instance, the sentence "A" means that all interpretations must assign true to whatever A is.) So, the empty set of sentences means there are no constraints. Therefore, all interpretations of {} are also models of {}. Therefore, going back to the definition of entailment, to write {} |= φ means that every model of {} is a model of phi. That is, every interpretation is a model of φ. In other words φ is a tautology (true in all interpretations).

Dropping parentheses

Added 2006-12-03.

Question: Are there any axioms that handle the use of parentheses? I.e., something like ∀x. (x) = x, just so that we can eliminate parentheses?

Answer:

You can go from (x) to x as long as nothing is changed in the evaluation of the sentence. Recall that parentheses are just a way of grouping functions to enforce a certain order of evaluation.

To illustrate, I will rewrite this clause:
{~(x + y) = x + (y)}

in prefix notation:
(not (= ((+ x y)) (+ x (y) ) )

If you look at it this way, the (y) is superfluous because there is no other evaluation possible. And similarly, the outer parentheses in ((+ x y)) are superfluous because you can't interpret it any other way.

So, yes, you can drop parentheses, as long as you do not change the evaluation order of the sentence.

If you are happy with compiler concepts, think of it this way: you can drop parentheses as long as it doesn't change the parse tree of the sentence.

The connection between models, validity, |=, and the soundness and completeness theorem

(This explanation relates to, among other things, question 9 in PS1, and question 6 in PS2)

Let's say that if S is a set of sentences, mod(S) is the set of models of S, i.e. the set of interpretations that satisfy S.

(a) Then notice that Gamma |= psi if and only if mod(Gamma) subset-or-eq mod({psi}).

(b) Also notice: if we add sentences to Gamma, then Gamma needs to satisfy more conditions, therefore its set of models shrinks. I.e., if Gamma subset-or-eq Gamma' then mod(Gamma) superset-or-eq mod(Gamma').
Conversely, if we remove sentences from Gamma, then it needs to satisfy fewer conditions, so it has more models.
Consequently, if Gamma is empty, it is satisfied by all possible models! (and not: if Gamma is empty then mod(Gamma) is empty).

(c) A sentence phi is logically valid if and only if it is satisfied by every interpretation and assignment, which is if and only if {} |= phi (phi is logically entailed from the empty set of sentences), which is if and only if mod({phi}) is the set of all interpretations.

(d) A sentence phi has a formal proof using no premises if and only if it is logically valid. How do we know? By the soundness and completeness theorem (slide 26 lecture 8). The theorem says that phi is provable from Gamma iff Gamma |= phi. Therefore, phi is provable from no premises if and only if {} |= phi , which is if and only if phi is a valid sentence.