Talk:Herbrandization

Latest comment: 8 years ago by 79.212.0.144 in topic Skolemization paragraph

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