previously on Heroes
Ugyan maga a "skolemizálás", aka zárt Skolem alakra hozás egy egyszerű algoritmusnak tűnik, formálisan bebizonyítani, hogy "helyes", mégsem olyan egyszerű.
Ugyan maga a "skolemizálás", aka zárt Skolem alakra hozás egy egyszerű algoritmusnak tűnik, formálisan bebizonyítani, hogy "helyes", mégsem olyan egyszerű.
Az outputja pl. nem lesz ekvivalens az eredeti formulával (vagy formulahalmazzal), hanem csak úgynevezett s-ekvivalens lesz (az "s" betű a "satisfiability"-ból, mint "kielégíthetőség" jön) :
Két formula, $F$ és $G$ $s$-ekvivalensek, jelben $F\equiv_s G$, ha
- vagy mindkettő kielégíthető,
- vagy mindkettő kielégíthetetlen.
A terv az, hogy megmutassuk: ha egy formulát skolemizálunk, akkor az eredmény az eredetivel $s$-ekvivalens lesz.
Addig, hogy a nyilakat elimináltuk, nincs gond: ezt az ekvivalenciát már régről ismerjük, tetszőleges $\mathcal{A}$ struktúrára $\mathcal{A}(F\to G)=\mathcal{A}(\neg F\vee G)$, és mindkettő pontosan akkor lesz igaz, ha $\mathcal{A}(F)\leq\mathcal{A}(G)$.
A változóátnevezéssel gondok vannak: érzi az ember, hogy egy egyszerű refaktorral nem lehet gond... vagy mégis? Ha például a $\exists x(x<y)$ formulában az $x$ változót mondjuk épp $y$-ra akarjuk átnevezni, a kapott $\exists y(y<y)$ formula nem lesz vele ekvivalens, hiszen pl. az első igaz az egész számok struktúráján, bármi is $\varphi(y)$, bármilyen egész szánnál van kisebb, a második meg hamis ezen a struktúrán.Vagy egy eggyel összetettebb példa: a $\exists x(p(x)\wedge\exists y(x<y))$ formulában is ha az $x$ változót épp $y$-ra akarjuk átnevezni és csak átírjuk, akkor a kapott $\exists y(p(y)\wedge \exists y(y<y))$ formula megint csak nem lesz ekvivalens az eredetivel...viszont, ha mindenáron $y$-ra akarjuk átnevezni, és a másik $y$-t ezzel egyidőben mondjuk $z$-re átnevezzük, akkor a katpott $\exists y(p(y)\wedge\exists z(y<z))$ formula ekvivalens lesz az eredetivel.
A Skolem alakra hozáskor pedig egy változó helyére egy komplett termet írunk be, jó lenne, ha ezt a két dolgot (változóátnevezés + Skolem függvény bevezetése változó helyébe) egyben tudnánk bebizonyítani, hogy jó ötlet. Erről fog szólni a helyettesítés, aminek először megnézzük a (tádáááá felépítés szerinti indukciós) definícióját, és aztán kiderül, hogy miért is olyan jó. Persze mivel a formulákon belül termek vannak, először termekre nézzük meg, hogy mit is jelent egy termben egy változót egy termre helyettesíteni:
Ha $u$ egy term, $x$ egy változó és $t$ egy term, akkor $u[x/t]$ egy termet jelöl, melyet a következőképp kapunk ($u$ felépítése szerinti indukcióval):
|
Nézzük meg ezt egy példán: ha az $u=g(c,f(x,y),g(x))$ termen hajtjuk végre az $[x/h(z)]$ helyettesítést, akkor az $u[x/h(z)]$ termet így kapjuk: $\begin{align*}g(c,f(x,y),g(x))[x/h(z)]&=g(c[x/f(z)],f(x,y)[x/h(z)],g(x)[x/h(z)])&&\hbox{összetett term subst def}\\&=g(c,f(x[x/h(z)],y[x/h(z)]),g(x[x/h(z)]))&&\hbox{összetett term subst, note konstans: eltűnik}\\&=g(c,f(h(z),y),g(h(z)))&&\hbox{változó substok} \end{align*}$ |
Más lesz a helyzet a formuláknál:
Ha $F$ egy formula, $x$ egy változó és $t$ egy term, akkor $F[x/t]$ egy formulát jelöl, melyet a következőképp kapunk $F$ felépítése szerinti indukcióval:
|
$\begin{align*}&\Bigl(\exists x p(x,y)~\wedge~\forall y q(x,y)~\wedge~\exists z r(x,y)\Bigr)[x/f(y)]\\&=(\exists xp(x,y))[x/f(y)]~\wedge~(\forall yq(x,y))[x/f(y)]~\wedge~(\exists z r(x,y))[x/f(y)]&&\hbox{éselésen átmegy}\\&=(\exists xp(x,y))~\wedge~(\forall yq(x,y))[x/f(y)]~\wedge~(\exists z r(x,y))[x/f(y)]&&\hbox{a kötött előfordulások békén maradnak}\\&=(\exists xp(x,y))~\wedge~(\forall z(q(x,y)[y/z][x/f(y)]))~\wedge~(\exists z r(x,y)[x/f(y)])&&\hbox{kötő $t$-beli kvantor változóját átnevezzük, másikon átmegyünk}\\&=(\exists xp(x,y))~\wedge~(\forall z(q(x,z)[x/f(y)]))~\wedge~(\exists z r(x[x/f(y)],y[x/f(y)]))\\&=(\exists xp(x,y))~\wedge~(\forall z(q(f(y),z)))~\wedge~(\exists z r(f(y),y))\end{align*}$
|
Ez ugyanazt eredményezi, mint ha:
- a szabad $x$ előfordulásokat mindet $t$-re cseréljük,
- és ha így egy "lecserélt" $t$-ben egy változó "lekötődne", akkor az őt "véletlenül" lekötő kvantor változóját (ilyen több is lehet, ha $t$-ben van több változó is) átnevezzük valami egészen újra.
folytköv