CS2: Introduction to Proof Systems

Question 1

Lemma

Resolution

Answer 1

Let F be a CNF formula represented as a set of clauses. If R is a resolvent of clauses C₁ and C₂ of F, then F ≡ F ∪ {R}

Question 2

Proof

(Resolution)
Let F be a CNF formula represented as a set of clauses. If R is a resolvent of clauses C₁ and C₂ of F, then F ≡ F ∪ {R}

3 points

Answer 2

• If A ⊧ F ∪ {R}, then clearly A ⊧ F
• Let R = (C₁\{L}) ∪ (C₂\{¬L})
• Consider cases where A ⊧ L or A ⊧ ¬L

Question 3

Theorem

Compactness

Propositional Logic

Answer 3

A set of formulae S is satisfiable if and only if each finite subset of S is satisfiable

Question 4

Lemma

Relevance

Answer 4

Suppose that A and A’ are σ-assignments with the same universe and identical interpretations of the predicate, function and constant symbols in σ. If A and A’ give the same interpretation to each variable ocurring free in some σ-formula F then A ⊧ F if and only if A’ ⊧ F

Question 5

Proof

(Relevance)
Suppose that A and A’ are σ-assignments with the same universe and identical interpretations of the predicate, function and constant symbols in σ. If A and A’ give the same interpretation to each variable ocurring free in some σ-formula F then A ⊧ F if and only if A’ ⊧ F

4 points

Answer 5

• Use structural induction
• Show that for every term t A(t) = A’(t)
• Consider constants, variables and k-ary functions
• For A ⊧ F if and only if A’ ⊧ F, consider predicate symbols, connectives and quantifiers

Question 6

Lemma

Translation

Answer 6

If t is a term and F is a formula such that no variable in t occurs bound in F, then A ⊧ F[t/x] iff A_([x ↦ A(t)]) ⊧ F

Question 6

Proof

(Translation)
If t is a term and F is a formula such that no variable in t occurs bound in F, then A ⊧ F[t/x] iff A_([x ↦ A(t)]) ⊧ F

4 points

Answer 6

• Use structural induction
• Show that for every term u A(u[t/x]) = A_([x ↦ A(t)])(u)
• Consider constants, variables (x and others) and k-ary functions
• For A ⊧ F[t/x] iff A_([x ↦ A(t)]) ⊧ F, consider predicates, connectives and quantifiers (not over x)

Question 6

Theorem

Herbrand

Answer 6

Let F = ∀x₁ ∀x₂ … ∀xₙ F* be a formula in Skolem form. Then F is satisfiable if and only if F has a Herbrand model

Question 7

Warning

Natural Deduction ∀I

Answer 7

Cannot apply if c occurs in an assumption that hasn’t been discharged

Question 7

Warning

Natural Deduction ∃E

Answer 7

c must not occur in C and all assumptions of the form A(c) must be discharged before inference step

Question 7

Warning

Sequent ∀R

Answer 7

Can only be applied if a does not appear elsewhere

Question 8

Warning

Sequent ∃L

Answer 8

Can only be applied if a does not occur elsewhere

Question 9

Theorem

Compactness

First-Order Logic

Answer 9

Let S be a countably infinite set of first-order formulas. Then, S is satisfiable if and only if every finite subset of S is satisfiable