Forma normal de Skolem

De Viquipèdia
Dreceres ràpides: navegació, cerca

En lògica matemàtica, la reducció a la forma normal de Skolem (FNS)[1] é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ó.[1] 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.[2]

La forma més senzilla de skolemització es dóna 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 x P(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[modifica | modifica el codi]

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 y  R(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 y R(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ó[modifica | modifica el codi]

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 es 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.[3]

Un altre ús es dóna 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[modifica | modifica el codi]

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.[4] 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.

Referències[modifica | modifica el codi]

  1. 1,0 1,1 Binefa, Xavier. Lògica computacional. 1a ed.. Bellaterra: Servei de Publicacions de la Universitat Autònoma de Barcelona, 1998, p. 111. ISBN 8449013844 [Consulta: 5 octubre 2013]. 
  2. «Normal Forms and Skolemization». max planck institut informatik. [Consulta: 5 octubre 2013].
  3. editors; Robinson, Alan; Voronkov, Andrei. Handbook of automated reasoning. Amsterdam: Elsevier, 2001. ISBN 0444508139 [Consulta: 6 octubre 2013]. 
  4. Moerdijk, I.; van Oosten, J. «Sets, models and proofs» (en anglès). Department of Mathematics, Utrecht University, 2006. [Consulta: 6 octubre 2013].

Bibliografia[modifica | modifica el codi]

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

Enllaços externs[modifica | modifica el codi]