03 - elsőrendű logika - még pár jelölés

previously on Heroes

Nézzünk pár fogalmat, aztán megpróbálunk kiértékelni egy "egyszerű"(nek tűnő) struktúrában formulákat.

Az előző postban a kvantoros formula kiértékelésekor érezhettük, hogy a "kvantoron belül" a változó már a "kvantortól kapja" az értéket legalábbis abban az értelemben, hogy mire odajut a kiértékelés, már nem számít, hogy mit adott neki eredetileg a struktúrában a $\varphi$ függvény. Most ezt formalizáljuk le egy kicsit (főleg azért, mert később a bizonyításokban szükség lesz ezekre a fogalmakra és állításokra).

Egy formulában minden változó minden egyes előfordulása vagy szabad lesz, vagy egy kvantorelőfordulás fogja kötni (az "előfordulás" tkp azt jelenti, hogy nem "az $x$ változó" lesz szabad a formulában, hanem a "hatodik karakteren álló $x$ változó", és lehet, hogy a formulában egy máshol levő $x$ meg nem lesz szabad. Kvantorokra ugyanez: fontos lesz, hogy melyik kötött változóelőfordulást melyik kvantor köti le). Informálisan (avagy konyhanyelven): ha egy $x$ változóelőfordulás egy $\exists x$ vagy egy $\forall x$ kvantor hatáskörén belülre (azaz a mögötte álló formulába, amivel konstruáltuk) esik, akkor az az $x$ kötve van; mégpedig, ha több ilyen kvantorelőfordulásnak is beleesik a hatáskörébe, akkor a legbelső ilyen fogja kötni.

Például: $\color{blue}{\exists x}\Bigl(~p(y)~\wedge~\color{red}{\exists y}(q(\color{blue}{x},\color{blue}{x}))~\wedge~\color{brown}{\exists x}(p(\color{brown}{x}))~\Bigr)$ a formulában az egyes kvantor-előfordulások az ő színükre színezett változóelőfordulásokat kötik. A fekete változóelőfordulás szabad. Note: a kvantor mellett álló változó nem "változóelőfordulás"!

Formálisan: az $F$ formula szabad előfordulásai (persze, hogy $F$ felépítése szerinti indukcióval):

ha $F$ atomi formula, akkor benne minden változóelőfordulás szabad; ha $F=\uparrow$ vagy $F=\downarrow$ alakú formula, akkor benne nincs szabad változóelőfordulás; ha $F=(\neg G)$ alakú formula, akkor benne $G$ összes szabad változóelőfordulása szabad; a kötött változóelőfordulásokat ugyanazok a kvantorok kötik $F$-ben, mint akik $G$-ben kötötték őket ha $F=(G\vee H)$,  $(G\wedge H)$, $(G\to H)$ vagy $(G\leftrightarrow H)$ alakú, akkor benne mind a $G$, mind a $H$ összes szabad változóelőfordulása szabad; a kötött változóelőfordulásokat ugyanazok a kvantorok kötik $F$-ben, mint akik $F$-ben / $G$-ben kötötték őket; ha $F=(\exists xG)$ vagy $F=(\forall xG)$ alakú, akkor a $G$-beli kötött változóelőfordulások $F$-ben is kötöttek, ugyanazon kvantor által; a $G$-beli szabad $x$ változóelőfordulások $F$-ben kötöttek, az $F$ elején álló kvantor által; a többi változó $G$-beli előfordulásai $F$-ben is szabadok.

Ha ezt így végigjátsszuk a fönti formulára: $p(y)$-ban az $y$ szabadon fordul elő, $q(x,x)$-ben az $x$ szintén mind a két helyen, $p(x)$-ben az $x$ szabad, mert ezek atomi formulák. $\color{red}{\exists y}(q(x,x))$-ben a két $x$ előfordulás szabad, más változó nem fordul elő benne (így, mivel $y$ nincs szabadon $q(x,x)$-ben, a $\exists y$ kvantor nem köt le semmit). $\color{brown}{\exists x}(p(\color{brown}(x))$-ben $p(x)$-ben az $x$ eredetileg szabad előfordulás volt, most pont az $x$ változót kötöttük le, így ezt a szabad előfordulást ez az (ebben a formulában) legkülső kvantor leköti. Ebben a formulában nincs szabad változóelőfordulás. $p(y)~\wedge~\color{red}{\exists y}(q(x,x))~\wedge~\color{brown}{\exists x}(p(\color{brown}(x))$-ben, mivel ez egy éselés, az marad szabad, aki eredetileg is az volt: az első $y$ előfordulás, és a középső részformula két $x$-e. (A fekete változóelőfordulások.) A többieket az a kvantor köti, aki eddig is. végül, $\color{blue}{\exists x}\Bigl(~p(y)~\wedge~\color{red}{\exists y}(q(\color{blue}{x},\color{blue}{x}))~\wedge~\color{brown}{\exists x}(p(\color{brown}{x}))~\Bigr)$ az előzőhöz képest még leköti a szabad $x$ előfordulásokat, vagyis a középső részformula két $x$-ét. Az $y$ szabad marad. És tényleg pont azt kaptuk vissza, mint amit az előbb az informális def alapján színeztünk, great.

Az éselés harmadik tagjában nem volt szabad változóelőfordulás, az ilyeneket mondatnak nevezzük.

Egy formula mondat, ha nincs benne szabad változóelőfordulás.

Ha egy $F$ formulában az  $x_1,\ldots,x_n$ változók fordulnak elő szabadon, azt úgy is jelezzük, hogy $F=F(x_1,\ldots,x_n)$. Például az előző formulára $F=F(y)$, mert benne $y$-nak volt szabad előfordulása.

A szabad változóelőfordulások például azért érdekesek, mert egy $\mathcal{A}=(A,I,\varphi)$ struktúrában ha egy $F=F(x_1,\ldots,x_n)$ formulát akarunk kiértékelni, akkor $\mathcal{A}(F)$ értéke $\varphi$-nek csak a $\varphi(x_1),\ldots,\varphi(x_n)$ részétől függ, az $F$-ben szabadon nem szereplő változóknak mindegy, mi az értéke, ezért azt nem is kell megadni. Ezt a következő posztban be is bizonyítjuk, egyelőre fogadjuk el és nézzük a megígért kiértékelés példát, hosszú lesz:

A jelkészlet, amink van: vannak a $+/2$ és $\times/2$ függvényjelek, az $1$ konstansjel, az $=/2$ predikátumjel. A struktúra, amiben ki akarunk értékelni: $\mathbb{N}=(\mathbb{N}_0,I,\varphi)$, azaz az alaphalmaz a természetes számok, $I(+)$ és $I(\times)$ a szokásos összeadás és szorzás, $I(1)=1$ (azaz az $1$-es jel tényleg az $1$-es számot jelöli) $I(=)$ az egyenlőség (más nem is lehet). A formulák, amiknek megnézzük a szemantikáját ebben a struktúrában (infix írva a bináris függvény- és predikátumjeleket): $\exists z(x\times z=y)$. Ez a formula pontosan akkor igaz, ha létezik olyan $c$ természetes szám, melyre $\varphi(x)\times c=\varphi(y)$, azaz pontosan akkor, ha $\varphi(x)$ osztója $\varphi(y)$-nak. Ezt a formulát rövidítsük úgy, hogy $x|y$. $\exists z(x+z=y)$. Ez a formula pontosan akkor igaz, ha létezik olyan $c$ természetes szám, melyre $\varphi(x)+c=\varphi(y)$, azaz pontosan akkor, ha $\varphi(x)\leq\varphi(y)$. Ezt a formulát rövidítsük úgy, hogy $x\leq y$. Az $(x\leq y)\wedge\neg(x=y)$ formulát pedig úgy, hogy $x<y$. $1<x~\wedge~\neg\exists z(1<z~\wedge~z<x~\wedge~z|x)$ akkor igaz, ha $\varphi(x)$ egy $1$-nél nagyobb természetes szám, melynek nem létezik olyan osztója, aki szigorúan $1$ és $x$ közé esne -- tehát pontosan akkor, ha $\varphi(x)$ prímszám. Jelölje ezt a formulát $\mathrm{prime}(x)$. $\exists x( y<x~\wedge~\mathrm{prime}(y)~\wedge~\mathrm{prime}(y+1+1) )$ pontosan akkor igaz, ha $\varphi(y)$-nél létezik egy olyan nagyobb $a$ természetes szám, aki prímszám és a nála kettővel nagyobb szám is prímszám. Itt a $\mathrm{prime}(y+1+1)$ formula azt jelenti, hogy a $\mathrm{prime}$ formulába, aminek eredetileg $x$ volt a szabad változója, a szabad változója helyébe mindenhová az $y+1+1$ termet írjuk be és átnevezzük a belső kvantált változókat úgy, hogy ne ütközzön a nevük az $y$-nal. Ahogy a $\mathrm{prime}(y)$ is azt, hogy $y$-t írjunk a szabad változó, $x$ helyébe. Ezért paraméterezzük fel a szabad változókkal a formulákat, mint $\mathrm{prime}(x)$: általában ezeket mint "shorthand"eket használjuk és a szabad $x$-ek helyére valami más termet írunk. $\forall y\exists x( y<x~\wedge~\mathrm{prime}(y)~\wedge~\mathrm{prime}(y+1+1) )$ ezek szerint pontosan akkor igaz, ha minden természetes számnál van nagyobb prímszám, akinél a kettővel nagyobb szám is prímszám. Ez a legutolsó pedig egy mondat, tehát a $\varphi$ nem is kell hozzá, azaz neki "a" természetes számok struktúrájában van egy igazságértéke: igaz akkor, ha végtelen sok "ikerprím" (a $2$ különbségű prímeket így hívják) van és hamis, ha csak véges sok. Pl. ikerprímek az $(5,7)$, $(11,13)$, $(17,19)$, $(101,103)$. Ha megpróbáljuk kiértékelni, hogy ez vajon igaz vagy hamis, akkor (vélhetően) falba ütközünk: a mai napig senki nem tudja, hogy ez az állítás vajon igaz-e.

A rövidítés jó dolog: ha kiírjuk ezt az előző formulát fullosan, rövidítés nélkül az eredeti jelekkel, akkor ezt kapjuk kb:

$\begin{align*}\forall y\exists x( \exists z(y+z=x)&~\wedge~\neg\exists z(\exists w(1+1+w=z)\wedge\exists w(z+1+w=x)\wedge\exists w(z\times w=x))\\&\wedge\neg\exists z(\exists w(1+1+w=z)\wedge\exists w(z+1+w=x+1+1)\wedge\exists w(z\times w=x+1+1)))\end{align*}$

Rövidítéseket használva azért eggyel olvashatóbb volt.
De miért nem adja oda senki egy kiértékelő algoritmusnak ezt a formulát akkor és várja ki a választ? Azért, mert matematikailag be van bizonyítva, hogy ilyen kiértékelő algoritmus nem létezik. Ha ebben a struktúrában (természetes számok, összeadás, szorzás) akarunk kiértékelni egy formulát, arra nem lehet programot írni, ami mindig helyes válasszal jönne vissza és minden formulára megállna.

Ez pedig nagyon függ a struktúrától, amiben számolni akarunk:

• a valós számok struktúráján az összeadással és a szorzással van ilyen algoritmus. Lassú, de van.
• a természetes számok struktúráján csak az összeadással, szorzás nélkül, szintén van ilyen algoritmus.
• a valós számok struktúráján az összeadással, a szorzással és az $x\mapsto e^x$ függvénnyel nem tudjuk, hogy van-e ilyen algoritmus.

Ezért, mivel a kiértékelés nagyon könnyen kiszámíthatatlanul bonyolulttá válik, ahelyett, hogy egy formulát megpróbálnánk kiértékelni, inkább azt próbáljuk automatikusan bebizonyítani, hogy a formula kielégíthetetlen. Erre érdekes módon több esélyünk van: van olyan algoritmus, ami

• ha az input $F$ formula kielégíthetetlen, akkor arra véges sok idő alatt rájön;
• ha meg kielégíthető, akkor vagy arra jön rá véges sok idő alatt, vagy végtelen ciklusba esik.

 Ez ugyan nem hangzik annyira fényesen, de a helyzet az, hogy ennél jobbat nem lehet csinálni: nincs olyan algoritmus (read as: matematikailag be van bizonyítva, hogy ilyen algoritmus nem létezik), ami véges idő alatt garantáltan megáll és mindig helyes választ adna arra a kérdésre, hogy az input $F$ formula kielégíthetetlen-e vagy kielégíthető.
A kapcsolódó gyakanyag a hetedik, érdemes hozzáolvasni.

folytköv