Translating "John is an adult man" into First Order Logic and Prover9 input

Question

I am working on translating a really simple English statement into First Order Logic, which is- "John is an adult man" My first order logic axioms are the following-

Man(x) -> Person(x).
Adult(x) <-> (Person(x) & Age(x)>=18).
Woman(x) -> Person(x).
Child(x) <-> (Person(x) & Age(x)<18).
Man(John).
Man(x) -> -Woman(x).
Age(John) = 30.

I am trying to prove whether John is an adult by the axiom-

Adult(John)

However Prover9 displays Exhausted and cannot search for a proof. Is there something I am missing?

Answer 1

Welcome to math.SE!

What you're trying to prove is not true. You can ask mace4 to generate a counter-model for you (it will find one of size 31 almost immediately. You will see that in the counter-model, < and >= are both defined as the empty relation.

How is this possible? In the language of Prover9, the symbols < and >= do not refer to the usual order relations $<, \geq$ of the natural numbers: instead, they are just arbitrary relational symbols that are governed by the axioms (and only the axioms) that you give to Prover9.

This is exactly what users of Prover9 want to happen: they work with general structures that come equipped with various orderings (e.g. ones defining an Alexandroff topology on some weak algebraic structure) that have nothing to do with the ordering of the natural numbers.

You should not try to use Prover9 to solve problems that involve natural numbers and the usual order relations $<,\leq$ in this fashion. It is technically possible to use Prover9 to solve problems involving arithmetic, but you'll be fighting an uphill battle.