Logic/FirstOrder

FOL

First-Order Logic (FOL)

First-Order Logic (FOL) is a formal deductive system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: First-Order Predicate Calculus (FOPC), the Lower Predicate Calculus, the Language of First-Order Logic or Predicate Logic.

While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification. Whereas propositional logic assumes world contains facts, FOL (like natural language) assumes the world contains...

  • Objects - women, houses, numbers, theories, colours, and of course George Bush.
  • Relations - red, round, bogus, prime, multi-storied, brother-of, bigger-than, inside, part-of, has-colour, occurred-after, owns, comes-between, etc.
  • Functions - father-of, best-friend, third-inning-of, one-more-than, end-of, etc.

 <<<— TODO: Finish Reading Chapter 8 —>>> 

Syntax

  • Constants - DooshBag, GiantTurdSandwich, GeorgeBush
  • Predicates - e.g. isBrother, >, ...
  • Functions - e.g. Sqrt, LeftLegOf, ...
  • Variables - e.g. x, y, etc.
  • Connectives - ⋀, ⋁, ¬, ⇒, ⇔
  • Equality - =
  • Qualifiers - ∀, ∃

Atomic Sentences

 <<<— TODO: Definition Missing —>>> 

Complex Sentences

Complext sentences are made from atomic sentences using connectives...

¬S, S1 ⋀ S2, S1 ⋁ S1, S1 ⇒ S1, S1 ⇔ S1

  • e.g. Spouse(PierreCurie, MarieCurie) ⇒ Spouse(MarieCurie, PierreCurie)

The Truth

  • Sentences in FOL are true with respect to a model and an interpretation
  • Interpretation specifies referents for...
    • constant symbols → objects
    • predicate symbols → relations
    • function symbols → functional relations

Quantifications

Properties of Qualifiers

  • Commutativity
    • ∀x∀y = ∀y∀x
    • ∃x∃y = ∃y∃x
    • ∃x∀y != ∀y∃x
      • ∃x ∀y Loves(x, y) - There exists at least one person who loves everyone in the world
      • ∀y ∃x Loves(x, y) - Everyone in the world is loved by at least one person
  • Duality
    • ∀x Loves(x, Women) = ¬∃x ¬Loves(x, Women)
    • ∃x Loves(x, Men) = ¬∀x ¬Loves(x, Men)
  • Symetry
    • ∀xy Sibling(x, y) ⇔ Sibling(y, x)
Universal Quantification (∀, main connective ⇒)

 <<<— TODO: Define —>>> 

Existential Quantification (∃, main connective ⋀)

 <<<— TODO: Define —>>> 

English to FOL Translations
English FOL
Everyone at Google is smart ∀x At(x, Google) ⇒ isSmart(x)
At least one person at UNSW is smart ∃x At(x, UNSW) ⋀ isSmart(x)
Everybody loves women ∀x Loves(x, Women)
Nobody doesn't love women ¬∃x ¬Loves(x, Women)
There exists at least one person that admires Hitler ∃x Admires(x, Hitler)
Not everybody doesn't admire Hitler ¬∀x ¬Admires(x, Hitler)
Brothers are(implied) siblings ∀x,y Brother(x, y) ⇒ Siblings(x, y)
One's mother is one's female parent, and vise versa ∀x,y Mother(x, y) ⇔ (isFemale(x) ⋀ isParent(x, y))
A cousin is the child of a parent's sibling ∀x,y Cousin(x, y) ⇔ ∃p0, p1 isParent(p0, x) ⋀ isSibling(p0, p1) ⋀ isParent(p1, y)
Some students took French in Spring 2001 ∃xy (didStudy(x, French, Sprint2001) ⋀ didStudy(y, French, Sprint2001) ⋀ (x != y))
Every student who takes French passes it ∀x,t (didStudy(x, French, t)) ⇒ didPass(x, French, t)
Only one student took Greek in Spring 2001 ∀x,y (didStudy(x, Greek, Spring2001) ⋀ didStudy(y, Greek, Spring2001)) ⇒ (x = y)
The best score in Greek is always higher than the best score in French ∃x(doesStudy(x, Greek, t) ⋀ ∀y(doesStudy(y, French, t) ⇒ score(y, French) < score(x, Greek)
Every person who buys a policy is smart ∀x (doesBuy(x, Policy)) ⇒ isSmart(x)
No person buys an expensive policy ¬∃x,p (doesBuy(x, p) ⋀ isExpensive(p))
There is an agent who sells policies only to people who are not insured ∃x,y,p (isPolicy(p) ⋀ doesSell(x, y, p) ⋀ ¬isInsured(y))
There is a barber who shaves all men in town who do not shave themselves ∃b(∀x(¬doesShave(x, x) ⇒ (doesShave(b, x)))
A person born in the UK, each of whose parents is a UK citizen or a UK resident, is a UK citizen by birth ∀x p1,p2 (isBornIn(x, UK) ⋀ isParent(p1, x) ⋀ isParent(p2, x) ⋀ (isResident(p1, UK) ⋁ isCitizen(p1, UK)) ⋀ (isResident(p2, UK) ⋁ isCitizen(p2, UK))) ⇒ isCitizen(x, UK, Birth)
A person born outside the UK, one of whose parents is a UK citizen by birth, is a UK citizen by descent ∀x,p (¬isBornIn(x, UK) ⋀ isParent(p, x) ⋀ isCitizen(p, UK, Birth)) ⇒ isCitizen(x, UK, Descent)
Politicians can fool some of the people all of the time, and they can fool all of the people some of the time, but they can't fool all of the people all of the time ∀p ⇒ ∃x∀t(doesFool(p, x, t)) ⋀ ∃t∀x(doesFool(p, x, t)) ⋀ ¬∀x∀t(doesFool(p, x, t))
All Germans speak the same languages ∀x,y ∃l (German(x) ⋀ German(y) ⋀ Language(l) ⇒ Speaks(x, l) ⋀ Speaks(y, l))

Resources

Logic ☣ Logic/Propositional