Skolemigo

Skolemigo estas transformo de predikatlogika formulo, ĉe kiu oni forigas ekzisto-kvantigilojn konservante la verigeblon de la formulo. Ĝi estas nomata laŭ la norvega logikisto Thoralf Skolem.

Kvankam la rezulto de skolemigo estas formulo samverigebla kiel la origina formulo, ĝi kutime ne estas logike samvalora, ĉar ĝi enkondukas novan funkci-simbolojn.

La pruvo de la konvervado de verigeblo ĉe skolemigo dependas de la aksiomo de elekto.

Ekzemplo de skolemigo

$\forall x\exists yR(x,y)$ skolemiĝas al $\forall xR(x,f(x))$. Do la ekziste kvantigita varianto y estas anstataŭigita per funkcio f, kiu dependas de la varianto x, ĉar la kvantigo de y okazas en la regiono de la kvantigo $\forall x$.