Skolem normalform

I matematisk logik är en formel för första ordningens logik i Skolem normal form om den är i normal form med endast universella första ordningens kvantifierare .

Varje första ordningens formel kan konverteras till Skolem normalform utan att ändra dess tillfredsställbarhet via en process som kallas Skolemization (ibland stavat Skolemnization ). Den resulterande formeln är inte nödvändigtvis likvärdig med den ursprungliga, men är likvärdig med den: den är tillfredsställbar om och endast om den ursprungliga är tillfredsställbar.

Reduktion till Skolem normalform är en metod för att ta bort existentiella kvantifierare från formella logiska uttalanden, ofta utförd som det första steget i en automatiserad teoremprovare .

Exempel

Den enklaste formen av skolemisering är för existentiellt kvantifierade variabler som inte är inom ramen för en universell kvantifierare. Dessa kan ersättas helt enkelt genom att skapa nya konstanter. Till exempel $\exists xP(x)$ ändras till $P(c)$ , där $c$ är en ny konstant (inte förekommer någon annanstans i formeln).

Mer allmänt utförs skolemisering genom att ersätta varje existentiellt kvantifierad variabel $y$ med en term $f(x_{1},\ldots ,x_{n})$ vars funktionssymbol $f$ är ny. Variablerna för denna term är följande. Om formeln är i prenex normal form är $x_{1},\ldots ,x_{n}$ de variabler som är universellt kvantifierade och vars kvantifierare föregår den för $y$ . I allmänhet är de variabler som kvantifieras universellt (vi antar att vi gör oss av med existentiella kvantifierare i ordning, så alla existentiella kvantifierare före ∃ $\displaystyle \exists y}$ har tagits bort) och sådana att $\ existerar y$ förekommer inom ramen för deras kvantifierare. Funktionen $f$ som introduceras i denna process kallas en Skolem-funktion (eller Skolem-konstant om den är av noll aritet ) och termen kallas en Skolem-term .

Som ett exempel, formeln $\forall x\exists y\forall zP(x,y,z)$ är inte i Skolem normal form eftersom den innehåller den existentiella kvantifieraren $\exists y$ . Skolemisering ersätter $y$ med $f(x)$ , där $f$ är en ny funktionssymbol, och tar bort kvantifieringen över $y$ . Den resulterande formeln är $\forall x\forall zP(x,f(x),z)$ . Skolem-termen $f(x)$ innehåller $x$ , men inte $z$ , eftersom kvantifieraren som ska tas bort $\exists y$ finns i omfattning av $\forall x$ , men inte inom $\forall z$ ; eftersom denna formel är i prenex normal form, motsvarar detta att säga att, i listan över kvantifierare, $x$ föregår $y$ medan $z$ inte gör det. Formeln som erhålls genom denna transformation är tillfredsställbar om och endast om den ursprungliga formeln är det.

Hur skolemisering fungerar

Skolemisering fungerar genom att tillämpa en andra ordningens ekvivalens tillsammans med definitionen av första ordningens tillfredsställelse. Ekvivalensen ger ett sätt att "flytta" en existentiell kvantifierare före en universell.

$\forall x\exists yR(x,y)\iff \exists f\forall xR(x,f (x))$

var

$f(x)$ är en funktion som mappar $x$ till $y$ .

Intuitivt konverteras meningen "för varje $x$ det finns en $y$ så att ${\displaystyle R(x,y)} "$ till den ekvivalenta formen "det finns en funktion $f$ som mappar varje $x$ till en $y$ så att den för varje $x$ innehåller $R (x,f(x))$ ".

Denna ekvivalens är användbar eftersom definitionen av första ordningens tillfredsställelse implicit existentiellt kvantifierar över utvärderingen av funktionssymboler. I synnerhet är en första ordningens formel $\Phi$ tillfredsställbar om det finns en modell $M$ och en utvärdering $\mu$ av de fria variablerna i formeln som utvärderar formeln till sant . Modellen innehåller utvärderingen av alla funktionssymboler; därför är Skolem-funktioner implicit existentiellt kvantifierade. I exemplet ovan, $\forall xR(x,f(x))$ är tillfredsställbar om och endast om det finns en modell $M$ , som innehåller en utvärdering för $f$ , så att $\forall xR(x,f(x))$ är sant för en viss utvärdering av dess fria variabler (ingen i detta fall). Detta kan uttryckas i andra ordningen som $\exists f\forall xR(x,f(x))$ . Med ovanstående ekvivalens är detta detsamma som tillfredsställelsen av $\forall x\exists yR(x,y)$ .

På metanivån kan första ordningens tillfredsställelse av en formel $\Phi$ skrivas med lite missbruk av notation som ${\displaystyle \exists M\exists \mu ~.~(M,\mu \models \Phi )} ,$ där $M$ är en modell, $\mu$ är en utvärdering av de fria variablerna, och $\models$ betyder att $\Phi$ är sant i $M$ under $\mu$ . Eftersom första ordningens modeller innehåller utvärderingen av alla funktionssymboler, kvantifieras alla Skolem-funktioner som ${\displaystyle \Phi } innehåller implicit existentiellt av$$\exists M$ . Som ett resultat, efter att ha ersatt existentiella kvantifierare över variabler med existentiella kvantifierare över funktioner längst fram i formeln, kan formeln fortfarande behandlas som en första ordningens genom att ta bort dessa existentiella kvantifierare. Detta sista steg för att behandla $\exists f\forall xR(x,f(x))$ som $\forall xR(x,f(x))$ kan slutföras eftersom funktioner implicit existentiellt kvantifieras av $\exists M$ i definitionen av första ordningens tillfredsställelse.

Korrektheten av skolemisering kan visas på exempelformeln $F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots,x_{n},y)$ enligt följande. Denna formel uppfylls av en modell $M$ om och endast om, för varje möjligt värde för $x_{1},\dots ,x_{n}$ i domänen av modellen, det finns ett värde för $y$ i domänen för modellen som gör $R(x_{1},\dots ,x_{n },y)$ sant. Enligt valets axiom finns det en funktion $f$ så att $y=f(x_{1},\dots ,x_{n})$ . Som ett resultat blir formeln ${\displaystyle F_{2}=\forall x_{1 }\dots \forall x_{n}R(x_{1},\dots,x_{n},f(x_{1},\dots,x_{n}))} är tillfredsställande, eftersom den har den erhållna$ modellen genom att lägga till utvärderingen av $f$ till $M$ . Detta visar att $F_{1}$ är tillfredsställbar endast om $F_{2}$ också är tillfredsställbar. Omvänt, om $F_{2}$ är tillfredsställbar, så finns det en modell $M'$ som uppfyller den; denna modell inkluderar en utvärdering för funktionen $f$ så att, för varje värde av $x_{1},\dots ,x_{n}$ , formeln $R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n} ))$ håller. Som ett resultat $F_{1}$ uppfylld av samma modell eftersom man kan välja, för varje värde på $x_{1},\ldots ,x_{n }$ , värdet $y=f(x_{1},\dots ,x_{n})$ , där $f$ utvärderas enl. $M'$ .

Användning av skolemisering

En av användningarna av Skolemization är automatiserad satsbevisande . Till exempel, i metoden för analytiska tablåer , närhelst en formel vars ledande kvantifierare är existentiell inträffar, kan formeln som erhålls genom att ta bort den kvantifieraren via Skolemization genereras. Till exempel, om $\exists x.\Phi (x,y_{1},\ldots ,y_{n})$ förekommer i en tablå, där $x,y_{1},\ldots ,y_{n}$ är de fria variablerna för $\Phi (x,y_{1} ,\ldots ,y_{n})$ , sedan $\Phi (f(y_{1},\ldots ,y_ {n}),y_{1},\ldots ,y_{n})$ kan läggas till i samma gren av tablåen. Detta tillägg förändrar inte tablåens tillfredsställelse: varje modell av den gamla formeln kan utökas genom att lägga till en lämplig utvärdering av $f$ till en modell av den nya formeln.

Denna form av skolemisering är en förbättring jämfört med "klassisk" skolemisering genom att endast variabler som är fria i formeln placeras i Skolem-termen. Detta är en förbättring eftersom tablåernas semantik implicit kan placera formeln inom ramen för vissa universellt kvantifierade variabler som inte finns i själva formeln; dessa variabler finns inte i Skolem-termen, medan de skulle finnas där enligt den ursprungliga definitionen av Skolemization. En annan förbättring som kan användas är att tillämpa samma Skolem-funktionssymbol för formler som är identiska upp till variabelbyte.

En annan användning är upplösningsmetoden för första ordningens logik , där formler representeras som uppsättningar av satser som förstås vara universellt kvantifierade. (För ett exempel se drinker paradox .)

Ett viktigt resultat inom modellteorin är Lowenheim-Skolem-satsen, som kan bevisas genom Skolemizing teorin och stängning under de resulterande Skolem-funktionerna.

Skolem teorier

I allmänhet, om $T$ är en teori och för varje formel med fria variabler $x_{1},\dots ,x_{n},y$ finns det en funktionssymbol $F$ som bevisligen är en Skolem-funktion för $y$ , då kallas ${\displaystyle T} en$ Skolem-teori .

Varje Skolem-teori är modellfullständig , dvs varje understruktur i en modell är en elementär understruktur . Givet en modell M av en Skolem-teori T , kallas den minsta understrukturen som innehåller en viss mängd A Skolem- skrovet av A. Skolem-skrovet av A är en atomär prime modell över A .

Historia

Skolem normalform är uppkallad efter den framlidne norske matematikern Thoralf Skolem .

Se även

• Herbrandization , skolmiseringens dual
• Predikatfunktionslogik

Anteckningar

•   Hodges, Wilfrid (1997), A Shorter Model Theory , Cambridge University Press , ISBN 978-0-521-58713-6

externa länkar

• "Skolem function" , Encyclopedia of Mathematics , EMS Press , 2001 [1994]
• Skolemisering på PlanetMath.org
• Skolemization av Hector Zenil, The Wolfram Demonstrations Project .
• Weisstein, Eric W. "SkolemizedForm" . MathWorld .