First-order Reasoning

Truth Tables

• Previously: Had to enumerate all the possible truth assignments of the relevant propositions.
• Enumerating all possible domain elements
  • For domains of more than a few elements, impractical.
  • For infinite domains, impossible.
• Enumerating possible truth assignments — e.g., R(x,y) can only be true or false, regardless of the values of x,y
  • Limited usefulness — mainly for testing validity of ∀-quantified formulas
• In short, not typically used.

Equivalences

(Note: We've already covered quite a bit of this.)

Propositional equivalence still hold, so focus on quantifiers.

A useful analogy

• ∀ is like ∧ over all the domain elements
• ∃ is like ∨ over all the domain elements

The basics

• Interchanging like quantifiers (∀x.∀y, ∃x.∃y)
• Interchanging unlike quantifiers (∀x.∃y, ∃x.∀y)
• Complementation (¬∀x, ¬∃x)
  • Compare to DeMorgan's Laws
• Renaming
  • Explain notation
• Distribution of ∀,∃ over ∧,∨
• Simplification of quantifiers, when body is free of bound variable

A Motivational Aside

Does ∀ x.φ imply ∃ x.φ?

A few more equivalences

• Simplication of quantifiers,, when domain empty

Example

• Simplify ∀x.R(x) ∧ ∀y.∃x.S(x,y)

Not covered in class: distribution of quantifiers over ⇒ — can be derived using φ⇒ψ ≡ ¬φ∨ψ

See the full list.

Inference rules

• All the propositional inference rules still apply
  • E.g., ∀x.R(x) |- ¬¬∀x.R(x)
• The new inference rules
  • Only four of them -- intro and elimination for each quantifier
  • Will introduce them one by one, but can only fully understand them in combination.
  • R(c) |- ?, where c is a domain constant
    • Generalize to ∃Intro
  • ∀x.R(x) |- ?
    • Generalize to ∀Elim
  • ∃x.R(x) |- ?
    • Essentially like the previous example, except that the name chosen has to meet a specific property -- not arbitrary
    • Generalize to ∃Elim
  • ? |- ∀x.R(x)
    • Essentially like ∃Intro, but what's the difference?
    • Generalize to ∀Intro
• Summarizing "arbitrary"
  • Easier to understand "not arbitrary"
  • Name not arbitrary if introduced by applying ∃Elim
  • Name not arbitrary if free in enclosing premise
• Remember, we don't have the equivalences
  • We'll prove versions of renaming and quantification complementation.

Some small, but illustrative, examples

Focus on interesting uses of quantification, since that's what's new.

Prove (or attempt to prove)…

• ∀x.R(x) |- ∀y.R(y)
• ∀x.R(x) |- ∃y.R(y)
• ∃x.R(x) |- ∃y.R(y)
• ∃x.R(x) |- ∀y.R(y)
• Is domain (non-)emptiness relevant to the previous examples?

Proving…

• ∀x.¬R(x) |- ¬∃x.R(x)
• ¬∃x.R(x) |- ∀x.¬R(x)
• Universal version of modus tollens: ∀x.(P(x) → Q(x)), ¬Q(a) |- ¬P(a)
• Some Waterworld examples

See text for larger examples. See online text for list of inference rules.

This material and homework is the last where you have to prove using such small steps.

Proofs

After finishing the current homework, you'll have "graduated" from the first third of the course. You should now know the fundamentals of logic and proofs. You should now be able to prove things in bigger steps, with the confidence that you could should the details, if asked.

How big of steps? A rule of thumb: Small enough that you and your audience both believe that you and your audience can fill in the details easily. However, judging your audience correctly takes experience.

You also have the flexibility of making more proofs more prose-like, integrating the reasoning into formalized English. If done well, this improves readability. But if done poorly, it obscures the logic. See the textbook for examples.

Now we'll concentrate less on how to prove and more on what to prove.