First-order Logic (FOF)

New logic features

Predicates with arguments are true or false (boolean)
Constants and functions with arguments (things in the world)
Universally quantified variables (for all)
Existentially quantified variables (there exists)
Equality as a primitive

Problem

Axioms
- The USA is a country.
- The capital of every country is a beautiful big city
- There is some city that is the capital of the USA
- Every big city has crime.
- A big city is a city.
Conjecture
- Therefore, there is some city that is beautiful but has crime.

Challenge problem

Bob, Maggie, Jill, and Geoff are four distinct people. The oldest sibling of Geoff is Jill (hint - a person has only one oldest sibling). If any person's oldest sibling is good looking then that person is good looking. If any person is good looking then one (or both) of their parents is good looking (hint - think of parent-child as a relationship between two people). Jill is good looking, Bob is not. The (only) parents of Geoff are Bob and Maggie. Therefore, Maggie is good looking.

Non-theorems

Axioms
- Iokaste, Oedipus, Polyneikes, and Thersandros are different people
- Iokaste is a parent of Oedipus and Polyneikes
- Oedipus is a parent of Polyneikes
- Polyneikes is a parent of Thersandros
- Nobody is their own parent
- Oedipus is a patricide
- Thersandros is not a patricide
Conjecture
- Iokaste is a parent of a patricide who is a parent of somebody who is not a patricide

In TPTP format

fof(different_people,axiom,
    ( iokaste != oedipus & iokaste != polyneikes & iokaste != thersandros
    & oedipus != polyneikes & oedipus != thersandros
    & polyneikes != thersandros ) ).
fof(iokaste_oedipus,axiom,
    ( parent_of(iokaste,oedipus) & parent_of(iokaste,polyneikes) ) ).
fof(oedipus_polyneikes,axiom,
    parent_of(oedipus,polyneikes) ).
fof(polyneikes_thersandros,axiom,
    parent_of(polyneikes,thersandros) ).
fof(no_self_parent,axiom,
    ! [X] : ~ parent_of(X,X) ).
fof(oedipus_patricidal,axiom,
    patricide(oedipus) ).
fof(thersandros_not_patricidal,axiom,
    ~ patricide(thersandros) ).
fof(iokaste_parent_particide_parent_not_patricide,conjecture,
    ? [P,NP] :
      ( parent_of(iokaste,P) & patricide(P) & parent_of(P,NP)
      & ~ patricide(NP) ) ).