Skolemizacja

Skolemizacja

Skolemizacja to technika w logice matematycznej, która umożliwia eliminację kwantyfikatorów egzystencjalnych oraz ogólnych w formułach rachunku predykatów pierwszego rzędu zapisanych w formie preneksowej. Metoda została opracowana przez norweskiego matematyka Thoralf Skolema.

Proces ten polega na zastępowaniu kwantyfikatorów egzystencjalnych nowymi symbolami funkcyjnymi, których argumentami są zmienne wprowadzone przez kwantyfikatory ogólne oraz zmienne wolne. Po skolemizacji formuła zawiera jedynie kwantyfikatory ogólne, które można pominąć, traktując wprowadzone zmienne jako zmienne wolne.

Przykład skolemizacji

Rozważmy formułę:

$\backslash forall\; x\; .\; \backslash exists\; y\; .\; \backslash forall\; w\; .\; \backslash exists\; z\; .\; R(x,y)\; \backslash lor\; \backslash neg\; R(x,z)\; \backslash lor\; Q(y,w,z)$

Skolemizacja tej formuły przebiega w następujący sposób:

• $\backslash exists\; y\; .\; \backslash forall\; w\; .\; \backslash exists\; z\; .\; R(x,y)\; \backslash lor\; \backslash neg\; R(x,z)\; \backslash lor\; Q(y,w,z)$ (gdzie $x$ jest zmienną wolną)
• $\backslash forall\; w\; .\; \backslash exists\; z\; .\; R(x,y(x))\; \backslash lor\; \backslash neg\; R(x,z)\; \backslash lor\; Q(y(x),w,z)$ (gdzie $y$ jest funkcją jednoargumentową)
• $\backslash exists\; z\; .\; R(x,y(x))\; \backslash lor\; \backslash neg\; R(x,z)\; \backslash lor\; Q(y(x),w,z)$ (gdzie $w$ jest zmienną wolną)
• $R(x,y(x))\; \backslash lor\; \backslash neg\; R(x,z(x,w))\; \backslash lor\; Q(y(x),w,z(x,w))$ (gdzie $z$ jest funkcją dwuargumentową)

Istotne jest, że jeśli oryginalna formuła jest sprzeczna lub spełnialna, to jej forma po skolemizacji zachowa te same właściwości. Formuła X jest spełnialna wtedy i tylko wtedy, gdy formuła Skol(X) również jest spełnialna. Oznacza to, że formuły te są równoważne pod względem spełnialności, jednak nie w sensie semantycznym.

Kategoria: Logika matematyczna