Skolemigo

El Vikipedio, la libera enciklopedio

Skolemigo estas transformo de predikatlogika formulo, ĉe kiu oni forigas ekzistajn kvantizantojn, 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[redakti | redakti fonton]

skolemiĝas al . Do la ekziste kvantizita varianto y estas anstataŭigita per funkcio f, kiu dependas de la varianto x, ĉar la kvantizo de y okazas en la regiono de la kvantizo .