Content deleted Content added
m Maintain {{WPBS}} and vital articles: 2 WikiProject templates. Create {{WPBS}}. Keep majority rating "Stub" in {{WPBS}}. Remove 2 same ratings as {{WPBS}} in {{WikiProject Computing}}, {{Maths rating}}. Remove 2 deprecated parameters: field, historical. Tag: |
|||
| (4 intermediate revisions by 2 users not shown) | |||
Line 1:
{{WikiProject banner shell|class=Stub|
{{WikiProject Computing|
{{WikiProject Mathematics| importance = low}}
}}
Line 28 ⟶ 23:
:∀''x''. ∃''y''. ''y''>''x'' ∧ ''p''(''y''),
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''
| |||