First-Order Logic

Motivation

Consider WaterWorld proofs of "F-has-1, D-has-1 |- C-safe" and "Z-has-1, X-has-1 |- W-safe".

• Proofs would be structurally identical.
• Would like to abstract the similarities into a single theorem.
• How to generalize this argument in English?
• Can't express this in propositional, so let's add relations and quantifiers.

WaterWorld relations

• Add: "loc1 is a neighbor of loc2", nhbr(loc1,loc2)
• Note: one way to understand relations is as functions that return booleans.
• Replace propositions with relations:
  • Replace loc-safe with safe(loc)
  • Replace loc-unsafe with ¬(safe(loc))
    • We'll avoid the unnecessary redundancy that was included in the propositional WaterWorld model
  • How to replace loc-has-n?
• Interpretation
  • Informally: the meaning/semantics of the relations
  • Formally: the domain and the relations' definitions
  • Domain
  • Relations as sets
  • What are the definitions of the WaterWorld relations?

First-order logic syntax

• New features: domain constants, domain variables, relations, quantifiers
• Terms
• Formulas

More examples — generalizing WaterWorld domain axioms

• E.g., A-has-0 ⇒ B-safe ∧ G-safe
• E.g., "nhbr" is anti-reflexive and symmetric

More examples from English to logic

• Everyone likes everyone.
• Noone likes everyone.
• Somebody doesn't like everyone.
• Somebody likes everyone that you like.
• Somebody likes somebody else.
• If I like someone, and that person likes somebody else, I like that person, too.

Some limitations of this logic

• Only have one domain of elements.
  • E.g., if we had a domain of locations AND 0…3, we could have the relation safe(loc,num).
  • What problems arise from this?
  • A possible way to cope with those problems — essentially type predicates
• We don't have functions in this logic
  • E.g., safe(left-nhbr(H))
  • How to encode functions as relations
• Can only quantify over domain elements
  • E.g., can't say ∀x.(x⇒x)
  • E.g., can't say ∀R.∃x.(R(x)⇒R(x))

An aside on terminology

• "First-order", since can only quantify over elements in the domain. Some other logics are even more flexible. Won't discuss.
• "Predicate", since relations are also known as predicates.

Towards "truth" and proving things

• Some formulas are "truer" than others
  • valid -- true in all interpretations (compare to "tautology")
  • E.g., ∀x.(R(x)→R(x))
• Next two classes: Proving things with first-order logic.

We covered this material, but not in this order.