Content deleted Content added
Line 30:
we get after quantifier elimination (i.e. [[Skolemization]], with ''f'' being a Skolem function for ''y''):
:''f''(''x'')>''x'' ∧ ''p''(''f''(''x'')
which has the ground instances (assuming, e.g., natural numbers' constructors - I'm not sure about this point):
:''f''(0)>0 ∧ ''p''(''f''(0)
:''f''(''s''(0))>''s''(0) ∧ ''p''(''f''(''s''(0))
:''f''(''s''(''s''(0)))>''s''(''s''(0)) ∧ ''p''(''f''(''s''(''s''(0)))
:''f''(''s''(''s''(''s''(0))))>''s''(''s''(''s''(0))) ∧ ''p''(''f''(''s''(''s''(''s''(0))))
:...
(that is the meaning of "one by one": there may be infinitely many ground instances, all of which have to be checked in succession until an unsatisfiable one is found).
To check e.g. the first one, convert it into a propositional formula by introducing ''A'' for ''f''(0)>0, and ''B'' for ''p''(''f''(0)
:''A'' ∧ ''B''
| |||