Talk:Herbrandization

Skolemization paragraph

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

$F^{S}=\forall y\forall z[R(y,f_{x}(y))\wedge \neg S(f_{x}(y),z)].$

Step by step:

$F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]$ (original formula)

$F:=\forall y\exists x[R(y,x)\wedge \forall z\neg S(x,z)]$ (replace negated existence with all quantor with negated statement)

$F:=\forall y\exists x\forall z[R(y,x)\wedge \neg S(x,z)]$ (move all quantifier to begin to formula to get prenex normal form)

$F:=\forall y\forall z[R(y,f_{x}(y))\wedge \neg S(f_{x}(y),z)]$ (replace variable bound by existence quantifier with function depending on preceding all quantors)

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