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

If any person is good looking then one (or both) of their parents is good looking. If any person's oldest sibling is good looking then that person is good looking (hint - a person has only one oldest sibling). The (only) parents of Geoff are Bob and Maggie. Bob is not Maggie. The oldest sibling of Geoff is Jill. Geoff is not Jill. Jill is good looking, Bob is not. 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) ) ).