Vés al contingut

Forma normal de Skolem

De la Viquipèdia, l'enciclopèdia lliure

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 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, es pot canviar a , on é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 per un terme , on la funció és nova. Les variables d'aquest terme són de la següent forma: si la fórmula està en forma normal prenexa, són les variables quantificades universalment per quantificadors situats abans del quantificador de . En general, són les variables que estan quantificades universalment, i tals que apareix en l'àmbit d'aquests altres quantificadors universals. La funció 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 no està en forma normal de Skolem, perquè conté el quantificador existencial . La skolemització substitueix per , on és una nova funció, i elimina la quantificació sobre . La fórmula resultant és . El terme de Skolem conté però no , perquè el quantificador que s'havia d'eliminar estava dins l'àmbit de però no del de ; com que aquesta fórmula està en forma normal prenexa, això és equivalent a dir que, en la llista de quantificadors, precedeix , mentre que 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]

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:

on és una funció que relaciona amb .

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

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 és satisfactible si existeixen un model i una avaluació 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, és satisfactible si i només si existeix un model , que conté una avaluació per , tal que és certa per a alguna avaluació de les seves variables lliures (cap, en aquest cas). Això es pot expressar en segon ordre com . Per l'equivalència anterior, això és el mateix que la satisfactibilitat de .

En metallenguatge, la satisfactibilitat d'una fórmula de primer ordre es pot escriure com , on és un model, és una avaluació de les variables lliures, i significa que és una conseqüència lògica de i . Com que els models de primer ordre contenen l'avaluació de tots els símbols de funció, qualsevol funció de Skolem contiguda a està quantificada existencialment de forma implícita per . 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 com es pot realitzar perquè les funcions estan quantificades existencialment de forma implícita per 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 : aquesta fórmula és satisfeta per un model si i només si, per tot valor possible de dins el domini del model, existeix un valor de en el domini del model que fa que sigui certa. Per l'axioma de l'elecció, existeix una funció tal que . Com a resultat, la fórmula és satisfactible, perquè té el model obtingut per addició de l'avaluació de a . Això demostra que és satisfactible només si també ho és. Recíprocament, si és satisfactible, llavors existeix un model que la satisfà; aquest model inclou una avaluació per la funció tal que, per a qualsevol valor de , la fórmula és certa. Com a resultat, és satisfeta pel mateix model, perquè hom pot escollir, per a cada valor de , el valor , on està avaluada d'acord amb .

Usos de la skolemització

[modifica]

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 apareix en un tableau, on són les variables lliures de , llavors 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 , 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.[3]

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

[modifica]

En general, si és una teoria, i per a tota fórmula amb variables lliures existeix una funció de Skolem, llavors hom diu que é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]
  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]
  • Hodges, Wilfrid. A shorter model theory. Repr.. Cambridge [u.a.]: Cambridge Univ. Press, 2002. ISBN 978-0-521-58713-6. 

Enllaços externs

[modifica]