First-order Logic (FOF)

New logic features

Predicates
Constants and Functions
Universally quantified Variables with ∀ (for all)
Existentially quantified Variables with ∃ (there exists)

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.

In logic

Axioms
- country(usa)
- ∀ C (country(C) → (big_city(capital_of(C)) ∧ beautiful(capital_of(C)) ))
- ∃ C (city(C) ∧ C = capital_of(usa))
- ∀ C (big_city(C) → has_crime(C))
- ∀ C (big_city(C) → city(C))
Conjecture
- ∃ C (city(C) ∧ beautiful(C) ∧ has_crime(C))

In TPTP format

fof(usa,axiom, country(usa) ).
fof(country_big_city,axiom,
    ! [C] : ( country(C) => ( big_city(capital_of(C)) & beautiful(capital_of(C)) ) ) ).
fof(usa_capital_axiom,axiom, 
    ? [C] : ( city(C) & C = capital_of(usa) ) ).
fof(crime_axiom,axiom,
    ! [C] : ( big_city(C) => has_crime(C) ) ).
fof(big_city_city,axiom,
    ! [C] : ( big_city(C) => city(C) ) ).

fof(some_beautiful_crime,conjecture,
    ? [C] : ( city(C) & beautiful(C) & has_crime(C) ) ).

Check the syntax in SystemB4TPTP using TPTP4X.
Try prove it using Vampire in SystemOnTPTP.
View the derivation using IDV in SystemOnTSTP.
Verify the derivation using GDV in SystemOnTSTP.

Challenge problem

If somone is good looking then one of their parents is good looking. If someone's oldest sibling is good looking then that someone 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

Problem
- 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) ) ).

Check the syntax in SystemB4TPTP using TPTP4X.
Try prove it using Vampire in SystemOnTPTP.
Change the conjecture to "Iokaste is a parent of a patricide who is a parent of somebody who is a patricide"
Try prove it using Vampire in SystemOnTPTP. That produces a saturation as a countermodel.
Disprove it using Paradox SystemOnTPTP. That produces a finite countermodel.
View the finite countermodel using IIV in SystemOnTSTP.
Verify the finite countermodel using AGMV in SystemOnTSTP. Use the concatenation of the problem and the countermodel as input.