Talk:Herbrandization

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

Skolemization paragraph[edit]

The formula given is not actually in Skolem normal form since it contains an existence quantifier. It should be:

Step by step:

(original formula)
(replace negated existence with all quantor with negated statement)
(move all quantifier to begin to formula to get prenex normal form)
(replace variable bound by existence quantifier with function depending on preceding all quantors)

79.212.0.144 (talk) 18:22, 12 April 2016 (UTC)[reply]