# 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 it in SystemOnTPTP using Vampire.

### 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. 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.