Forma normal de Skolem

En lògica matemàtica, la reducció a la forma normal de Skolem (FNS) és un mètode per eliminar els quantificadors existencials dels enunciats de lògica, i sovint aquest és un primer pas en la demostració automàtica de teoremes.

Una fórmula de lògica de primer ordre es diu que està en forma normal de Skolem (anomenada així en honor de Thoralf Skolem) si està en forma normal prenexa conjuntiva amb només quantificadors universals de primer ordre. Tota fórmula ben formada es pot convertir en forma normal de Skolem sense alterar-ne la satisfactibilitat, mitjançant un procés anomenat skolemització. La fórmula que en resulta no és necessàriament equivalent a l'original, però hi és equisatisfactible: és satisfactible si i només si la fórmula original és satisfactible.

La forma més senzilla de skolemització es dona en el cas de variables amb quantificació existencial que no estan dins l'àmbit d'un quantificador universal. Aquestes variables es poden substituir per noves constants. Per exemple, $\exists xP(x)$ es pot canviar a $P(c)$, on $c$ és una nova constant (ja que no apareix enlloc més de la fórmula).

Més en general, la skolemització es realitza mitjançant la substitució de tota variable quantificada existencialment $y$ per un terme $f(x_{1},\ldots ,x_{n})$, on la funció $f$ és nova. Les variables d'aquest terme són de la següent forma: si la fórmula està en forma normal prenexa, $x_{1},\ldots ,x_{n}$ són les variables quantificades universalment per quantificadors situats abans del quantificador de $y$. En general, són les variables que estan quantificades universalment, i tals que $y$ apareix en l'àmbit d'aquests altres quantificadors universals. La funció $f$ introduïda en aquest procés és anomenada funció de Skolem (o constant de Skolem, si té aritat zero), i el terme s'anomena terme de Skolem.

Com a exemple, la fórmula $\forall x\exists y\forall z.P(x,y,z)$ no està en forma normal de Skolem, perquè conté el quantificador existencial $\exists y$. La skolemització substitueix $y$ per $f(x)$, on $f$ és una nova funció, i elimina la quantificació sobre $y$. La fórmula resultant és $\forall x\forall z.P(x,f(x),z)$. El terme de Skolem $f(x)$ conté $x$ però no $z$, perquè el quantificador que s'havia d'eliminar $\exists y$ estava dins l'àmbit de $\forall x$ però no del de $\forall z$; com que aquesta fórmula està en forma normal prenexa, això és equivalent a dir que, en la llista de quantificadors, $x$ precedeix $y$, mentre que $z$ no ho fa. La fórmula obtinguda mitjançant aquest procés és satisfactible si i només si ho és la fórmula original.

Funcionament

La skolemització aplica una equivalència de segon ordre juntament amb la definició de satisfactibilitat de primer ordre. Aquesta equivalència proporciona un mètode per "desplaçar" un quantificador existencial cap al davant d'un d'universal:

$\forall x{\Big (}g(x)\vee \exists yR(x,y){\Big )}\iff \forall x{\Big (}g(x)\vee R(x,f(x)){\Big )}$

on $f(x)$ és una funció que relaciona $x$ amb $y$.

De forma intuïtiva, l'afirmació "per tot $x$ existeix un $y$ tal que es compleix $R(x,y)$" es converteix en la seva forma equivalent "existeix una funció $f$ que porta $x$ cap a $y$ tal que, per tot $x$, es compleix $R(x,f(x))$".

Aquesta equivalència és útil perquè la definició de satisfactibilitat de primer ordre quantifica existencialment de forma implícita l'avaluació dels símbols de funció. En particular, una fórmula de primer ordre $\Phi$ és satisfactible si existeixen un model $M$ i una avaluació $\mu$ de les variables lliures de la fórmula que avalua la fórmula com a certa. El model conté l'avaluació de tots els símbols de funció; per tant, les funcions de Skolem tenen una quantificació existencial implícita. En l'exemple anterior, $\forall x.R(x,f(x))$ és satisfactible si i només si existeix un model $M$, que conté una avaluació per $f$, tal que $\forall x.R(x,f(x))$ és certa per a alguna avaluació de les seves variables lliures (cap, en aquest cas). Això es pot expressar en segon ordre com $\exists f\forall x.R(x,f(x))$. Per l'equivalència anterior, això és el mateix que la satisfactibilitat de $\forall x\exists y.R(x,y)$.

En metallenguatge, la satisfactibilitat d'una fórmula de primer ordre $\Phi$ es pot escriure com $\exists M\exists \mu ~.~(M,\mu \models \Phi )$, on $M$ és un model, $\mu$ és una avaluació de les variables lliures, i $\models$ significa que $\Phi$ és una conseqüència lògica de $M$ i $\mu$. Com que els models de primer ordre contenen l'avaluació de tots els símbols de funció, qualsevol funció de Skolem contiguda a $\Phi$ està quantificada existencialment de forma implícita per $\exists M$. Com a resultat, després de substituir un quantificador existencial sobre variables per quantificadors existencials sobre funcions a l'inici de la fórmula, la fórmula encara es pot tractar com de primer ordre, tot eliminant aquests quantificadors existencials. Aquest pas final de tractar $\exists f\forall x.R(x,f(x))$ com $\forall x.R(x,f(x))$ es pot realitzar perquè les funcions estan quantificades existencialment de forma implícita per $\exists M$ en la definició de la satisfactibilitat de primer ordre.

La correctesa de la skolemització es pot demostrar en la fórmula anterior que ha servit com a exemple $F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)$: aquesta fórmula és satisfeta per un model $M$ si i només si, per tot valor possible de $x_{1},\dots ,x_{n}$ dins el domini del model, existeix un valor de $y$ en el domini del model que fa que $R(x_{1},\dots ,x_{n},y)$ sigui certa. Per l'axioma de l'elecció, existeix una funció $f$ tal que $y=f(x_{1},\dots ,x_{n})$. Com a resultat, la fórmula $F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))$ és satisfactible, perquè té el model obtingut per addició de l'avaluació de $f$ a $M$. Això demostra que $F_{1}$ és satisfactible només si $F_{2}$ també ho és. Recíprocament, si $F_{2}$ és satisfactible, llavors existeix un model $M'$ que la satisfà; aquest model inclou una avaluació per la funció $f$ tal que, per a qualsevol valor de $x_{1},\dots ,x_{n}$, la fórmula $R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))$ és certa. Com a resultat, $F_{1}$ és satisfeta pel mateix model, perquè hom pot escollir, per a cada valor de $x_{1},\ldots ,x_{n}$, el valor $y=f(x_{1},\dots ,x_{n})$, on $f$ està avaluada d'acord amb $M'$.

Usos de la skolemització

Un dels usos de la skolemització és la demostració automàtica de teoremes. Per exemple, en el mètode dels tableaux analítics, sempre que es té una fórmula on el primer quantificador és existencial, hom pot generar per skolemització una nova fórmula mitjançant l'eliminació d'aquest quantificador. Per exemple, si $\exists x.\Phi (x,y_{1},\ldots ,y_{n})$ apareix en un tableau, on $x,y_{1},\ldots ,y_{n}$ són les variables lliures de $\Phi (x,y_{1},\ldots ,y_{n})$, llavors $\Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})$ es pot afegir a la mateixa branca del tableau. Aquesta addició no altera la satisfactibilitat del tableau: qualsevol model de la fórmula original es pot estendre, tot afegint-hi una avaluació adient de $f$, al model de la nova fórmula.

Aquesta forma de skolemització és, de fet, una ampliació de la skolemització "clàssica", en què només les variables lliures a la fórmula se situen al terme de Skolem. Això és una ampliació perquè la semàntica del tableau pot col·locar implícitament la fórmula dins l'àmbit d'alguna variable quantificada universalment que no estigui a la fórmula; aquestes variables no estan al terme de Skolem, mentre que sí que estarien d'acord amb la definició original de la skolemització. Una altra millora que es pot usar és el fet d'emprar el mateix símbol de funció de Skolem per a fórmules que siguin idèntiques llevat de reanomenament de les seves variables.

Un altre ús es dona en el mètode de resolució per lògica de primer ordre, on les fórmules es representen com a conjunts de clàusules, que hom entén quantificades universalment.

Teories de Skolem

En general, si $T$ és una teoria, i per a tota fórmula $F$ amb variables lliures $x_{1},\dots ,x_{n},y$ existeix una funció de Skolem, llavors hom diu que $T$ és una teoria de Skolem. Per exemple, com hem vist abans, l'aritmètica amb l'axioma de l'elecció és una teoria de Skolem.

Tota teoria de Skolem és completa per models, és a dir, tota subestructura d'un model és una subestructura elemental. Donat un model M d'una teoria de Skolem T, la subestructura més petita que conté un cert grup A s'anomena el casc de Skolem de A. El casc de Skolem de A és un model primer atòmic sobre A.

Bibliografia

• Hodges, Wilfrid. A shorter model theory. Repr.. Cambridge [u.a.]: Cambridge Univ. Press, 2002. ISBN 978-0-521-58713-6. 

Enllaços externs

• Michiel Hazewinkel (ed.). Skolem function. Encyclopedia of Mathematics (en anglès). Springer, 2001. ISBN 978-1-55608-010-4. 
• Skolemization on PlanetMath.org Arxivat 2006-02-27 a Wayback Machine.
• Skolemization by Hector Zenil, The Wolfram Demonstrations Project.
• Weisstein, Eric W., «SkolemizedForm» a MathWorld (en anglès).