07 - a helyettesítési algoritmus

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ű.

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): ha $u$ egy változó és $u=x$, akkor $u[x/t]:=t$. ha $u$ egy változó és $u\neq x$, akkor $u[x/t]:=u$. ha $u=f(t_1,\ldots,t_n)$ egy összetett term, akkor $u[x/t]:=f(t_1[x/t],\ldots,t_n[x/t])$.

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*}$

ez általában is igaz: ha egy $u$ termen egy $[x/t]$ helyettesítést hajtunk végre, akkor az eredmény $u\cdot[x/t]$ termet úgy kapjuk, hogy simán kicseréljük az összes $u$-beli $x$-et $t$-re.
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: ha $F=p(t_1,\ldots,t_n)$ atomi formula, akor $F[x/t]:=p(t_1[x/t],\ldots,t_n[x/t])$. tehát: atomi formulában ha az $x$-et $t$-re helyettesítjük, akkor csak kicseréljük az összes $x$-et $t$-re ha $F=\neg G$, akkor $F[x/t]:=\neg(G[x/t])$ ha $F=(G\bullet H)$, ahol $\bullet\in\{\vee,\wedge,\to,\leftrightarrow\}$, akkor $F[x/t]:=(G[x/t])\bullet(H[x/t])$ tehát: a logikai konnektívákon keresztül simán csak "migráljuk lefelé" a helyettesítést ha $F=\uparrow$ vagy $F=\downarrow$, akkor $F[x/t]:=F$ tehát: a logikai konstansok nem változnak meg attól, hogy egy változót helyettesítünk ha $F=Q xG$, $Q\in\{\exists,\forall\}$ (tehát: a kötött változó épp az, amit most helyettesítünk), akkor $F[x/t]:=F$ tehát: kötött változóelőfordulást nem helyettesítünk le ha $F=Q yG$, $Q\in\{\exists, \forall\}$, $y\neq x$ és $y$ nem fordul elő $t$-ben, akkor $F[x/t]:=\exists yG[x/t]$ tehát: ha más változót kötünk, akinek köze nincs $t$-hez, akkor nem kell semmi extrát csinálni ha $F=QyG$, $Q\in\{\exists,\forall\}$, $y\neq x$ és $y$ előfordul $t$-ben, akkor legyen $z$ egy új változó, aki nem $x$, nem $y$ és nem szerepel $G$-ben sem és $F[x/t]:=Qz(G[y/z][x/t])$. tehát, ha olyan kötött változón belül helyettesítjük $x$-et, aki szerepel a $t$ termben, akire helyettesítjük épp $x$-et, akkor át kell nevezzük a kötő kvantor változóját valami zsír újra.

Nézzük csak meg ezt egy példán:

$\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.

A kövi posztban megnézzük, hogy ez a helyettesítési értékadás tulajdonképpen ugyanaz, mint egy értékadás, de szemantikai helyett a szintaktikai szinten.

folytköv

06 - Elsőrendű normálformák

previously on Heroes

Tehát most a célunk az, hogy egy következtető rendszert adjunk meg, ami elsőrendű logikai formulák egy $\Sigma$ halmazára és egy $F$ célformulára ha $\Sigma\vDash F$ igaz, akkor arra előbb-utóbb rájön, ha meg nem következmény, akkor nem jön ki azzal a válasszal, hogy "következménye".

(Olyan algoritmus matematikailag igazoltan nincs, ami arra is garantáltan rájönne, hogy nem következménye egy formula egy másiknak, itt a legjobb amit remélhetünk, az az, hogy vagy rájön az algoritmus, hogy nem következmény, vagy végtelen ciklusba esik.)

Erre a problémára (ezen a kurzuson) kétféle rezolúciós algoritmust fogunk nézni: az egyiknek a neve "alap rezolúció" lesz, a másiké meg (ravasz módon) "elsőrendű rezolúció". Mindkettő, hasonlóan az ítéletkalkulus-beli változatukhoz, arra lesz jó, hogy egy input formulahalmazról megmutassa, hogy kielégíthetetlen, azzal, hogy levezeti belőle az üres klózt.

Ugyanúgy, ahogy a ítéletkalkulus rezolúciós algoritmusához is egy ottani normálformára (CNF-re) kellett hozni az inputot, itt is: ezt a normálformát zárt Skolem (ejtsd: Szkólem) alaknak hívják.

Ebben a posztban megnézzük, hogy hogyan hozunk egy formulát zárt Skolem alakúra, az eredmény "magját" pedig CNF-re, a következőben pedig bebizonyítjuk, hogy amit csinálunk, az jó lesz, ha az input kielégíthetetlenségét akarjuk bizonyítani. (Ez most nem lesz ekvivalens az inputtal, amit gyártunk, de "majdnem". Ezt a következőből megértjük.)

Tehát, induljunk ki egy formulából, az algoritmust példán keresztül is visszük végig. Legyen mondjuk ez: $\forall x(\exists yp(f(x),y)~\to r(x))~\wedge~\exists x\forall y(p(y,f(x))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z\neg r(z)$.

1. Elimináljuk a $\to$ és $\leftrightarrow$ konnektívákat a szokásos $\begin{align*}F\to G&\equiv\neg F\vee G&F\leftrightarrow G&\equiv(\neg F\vee G)\wedge(F\vee\neg G)\end{align*}$ azonosságokkal.

   
   

   Most ennek az eredménye ezen a formulán  az egyetlen $\to$ konnektíva kiütése után: $\forall x(\neg\exists yp(f(x),y)~\vee r(x))~\wedge~\exists x\forall y(p(y,f(x))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z\neg r(z)$

2. Kiigazítás: Átnevezzük a változókat, hogy különböző kvantor előfordulások különböző változókat kössenek le, és ne legyen olyan változó sem, ami szabadon is és kötötten is előfordul. A szabad változókat nem nevezhetjük át. Ennek egy módja pl (ha az input formulánkban amúgy nincsenek indexelve a változók), hogy indexeljük az összes kötött változót, akár $1$-től kezdve sorfolytonosan, minden egyes kvantornál növelve az indexet, akár változónként külön-külön indexet vinni, mindegy, csak ne legyen névütközés. Arra persze figyeljünk oda, hogy ha egy kvantor mellett álló változót átnevezünk valamire, akkor pontosan azokat a változóelőfordulásokat kell átneveznünk ugyanerre, melyeket ez a kvantorelőfordulás köt.

   
   

   A munkaformulánkon ennek a lépésnek ez lesz (pl) az eredménye: $\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$ Itt most minden kvantorelőfordulás egy közös indexet növelt. Látszik, hogy a $z$ az egyetlen változó, mely előfordul szabadon is, de azt kétszer teszi. Nem baj.

3. Prenex alakra hozás: ennek a lépésnek az a célja, hogy az összes kvantor a formula elejére kerüljön. Ezt tehetjük pl. a következő kvantorkihúzási azonosságokkal, amik akkor igazak, ha a formula kiigazított: $\begin{align*}(Qx F)\bullet G&\equiv Qx(F\bullet G)\tag{minden $Q\in\{\exists,\forall\}$, $\bullet\in\{\vee,\wedge\}$ esetén}\\F\bullet(QxG)&\equiv Qx(F\bullet G)\tag{minden $Q\in\{\exists,\forall\}$, $\bullet\in\{\vee,\wedge\}$ esetén}\\\neg\exists xF&\equiv\forall x\neg F\\\neg\forall xF&\equiv \exists x\neg F\end{align*}$

   Ha ezeket a szabályokat alkalmazgatjuk a munkaformulánkon, akkor ilyesmi lépéseket kapunk: $\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$  $\forall x_1(\forall y_2\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$  $\forall x_1\forall y_2(\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$ és ezen a ponton van négy formulánk éselve, mindnek az elején kvantorok, kihozzuk mindet:  $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$

   
   
   Egy másik módszer, ami kézzel végrehajtva gyorsabb kicsit, ha az ember átlátja a formulát (programmal mindenképp gyorsabb, ha a formulánkat fában reprezentáljuk):
   

   • fogjuk az eredeti kigazított, nyílmentesített formulát
   • a benne levő kvantált változókat balról jobbra, az eredeti deklarációs sorrendben kötjük le
   • egy változót lekötő kvantor "megfordul" ($\exists$-ből $\forall$ lesz és fordítva), ha páratlan sok $\neg$ jel hatáskörébe esik; ha pároséba, akkor nem fordul meg
   • végül, a formula magját (így hívják a prenex formuláknak azt a részformuláját, amelyikben már épp nincs kvantor) úgy kapjuk, hogy az eredeti formulából kitöröljük a kvantorokat.

   Ezt végrehajtva az előzőre: kiindulunk ebből
   

   $\forall x_1(\neg\exists y_2p(f(x_1),y_2)~\vee r(x_1))~\wedge~\exists x_3\forall y_4(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\forall z_5\neg r(z_5)$

   a sorrend $x_1$, $y_2$, $x_3$, $y_4$, $z_5$ lesz; három negálás van a formulában, nincsenek egymásba ágyazva, így ezt most egyszerű látni, hogy csak az $\exists y_2$ az egyetlen kvantált változó, aki páratlan sok (egy) negálás belsejében van, így ő az egyetlen, aki megfordul. A kvantor prefix tehát $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5$ lesz. Utánaírjuk a formulánkat úgy, hogy kitöröljük a kvantorokat éééés:
   

   $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$

   yep, ugyanaz lett, mint az előbb.

4. Skolem alakra hozás: ennek a lépésnek a célja, hogy csak $\forall$-kvantorok maradjanak a formulában (és persze maradjon prenex alakban). Az előző lépések ekvivalens átalakítások voltak, ez már nem lesz az. Ahogy csináljuk: kiindulunk a prenex, kiigazított alakból minden egyes $\exists y$-ra kitöröljük az $\exists y$-t a formula elejéről és $y$ minden előfordulásának helyébe a magban egy $f(x_1,\ldots,x_n)$ termet írunk ahol is $f$ egy teljesen új függvényjel (amit Skolem függvénynek is hívnak), amit most generáltunk -- ha egyszerre több formulát hozunk Skolem alakra, akkor meg kell nézni, hogy egyikben sem szerepelhet! Ha több Skolem függvényjelet generálunk, akkor mind egymástól is különböző kell legyen! az $x_1,\ldots,x_n$ változók pedig azok, akik az $y$ előtt (attól balra) vannak $\forall$ kvantorral kötve a formulában.

   nézzük ezt a munkaformulánkon, itt tartunk: $\forall x_1\forall y_2\exists x_3\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(x_3))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$ sok dolgunk nincs ezzel most, egyetlen $\exists$ kvantor van benne, ami $x_3$-at köti. Keresünk egy új függvényjelet, amit még nem használunk, ez pl most lehet $g$ ($f$ viszont nem), és függni fog $x_1$-től és $y_2$-től, mert azok vannak $x_3$ előtt univerzálisan deklarálva. Tehát, töröljük a $\exists x_3$ részt és a formulában $x_3$ minden előfordulása helyébe $g(x_1,y_2)$-t írunk: $\forall x_1\forall y_2\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(g(x_1,y_2)))\vee q(z))~\wedge~\neg q(z)~\wedge~\neg r(z_5)\Bigr)$ ez így most kész is, a formula Skolem alakú.

5. Lezárás: ennek a lépésnek a célja, hogy ne legyen szabad változónk. Ezt úgy érjük el, hogy minden $x$ szabad változóelőfordulás helyébe egy új, $x$-től függő konstanst, pl. $c_x$-et írunk. Szintén fontos, hogy a konstans új legyen, itt viszont ha több formulában is szerepel szabadon ugyanaz az $x$, akkor mindegyikben ugyanazt a $c_x$-et kell írjuk a helyébe!

   
   

   Folytatva az előző példánkat: $z$ az egyetlen szabadon előforduló változó, ő kétszer is szerepel, helyére bekerül a $c_z$ konstans: $\forall x_1\forall y_2\forall y_4\forall z_5\Bigl((\neg p(f(x_1),y_2)~\vee r(x_1))~\wedge~(p(y_4,f(g(x_1,y_2)))\vee q(c_z))~\wedge~\neg q(c_z)~\wedge~\neg r(z_5)\Bigr)$

6. A mag CNF-re hozása: teljesen ugyanazzal a módszerrel, mint ítéletkalkulusban, a zárt Skolem alakú formulánk magját CNF-re hozzuk. Most literál minden atomi formula (ők pozitívak) és azok negáltjai (ők negatívak), vagyis a predikátumjellel kezdődő, vagy esetlegesen negált predikátumjellel kezdődő részek klóz továbbra is véges sok literál vagyolása a CNF pedig továbbra is klózok éselése

Ha megnézzük, a mostani munkaformulánkban literálok pl. a $\neg p(f(x_1),y_2)$, az $r(x_1)$, a $p(y_4,f(g(x_1,y_2)))$, a $q(c_z)$, a $\neg q(c_z)$ és a $\neg r(z_5)$, de most teljesen jól vannak, literálok vannak vagyolva egy- vagy kéttagú klózokká, és ilyen klózból van négy. Akár le is írthatjuk őket egy $\Sigma$ klózhalmazba, ugyanúgy halmazként reprezentálva mindent, mint ítéletkalkulusban tettük: $\left\{\{\neg p(f(x_1),y_2),r(x_1)\},~\{p(y_4,f(g(x_1,y_2))),q(c_z)\},~\{\neg q(c_z)\},~\{\neg r(z_5)\}\right\}$.

Ez minden; mindkét rezolúciós algoritmus ebben a formátumban, zárt Skolem alakú formulákként, melyeknek a magját CNF-re hoztuk és az összes klózt egy $\Sigma$ halmazba tesszük. Hogy mit tesznek vele, azt meglátjuk, miután megnézzük, hogy ezek az átalakítások tényleg jók lesznek nekünk.

A kapcsolódó gyakanyag a hetedik és a nyolcadik és érdemes lehet nyomkodni itt a "Generálj Skolemest!" gombot, hogy biztos értsük a zárt Skolem normálformára hozás minden részletét. (Itt nem kell CNF-re hozni a magot.)

folytköv

05 - a Peano axiómák

previously on Heroes

Addig tehát megvagyunk, hogy hiába tűnnek faék egyszerűnek a természetes számok a szorzással meg az összeadással, már erre a struktúrára sincs algoritmus, ami ki tudna benne értékelni egy input formulát.

Olyan algoritmus viszont lesz, ami arra alkalmas, hogy egy input elsőrendű $\Sigma$ formulahalmazra és egy elsőrendű $F$ formulára igaz, hogy $\Sigma\vDash F$, akkor erre véges idő alatt rá is jöjjön.

Persze ezek a jelek itt is ugyanazt jelentik, mint ítéletkalkulusban:

hogy az $\mathcal{A}$ struktúrában az $F$ formula értéke $1$, azt írjuk úgy is, hogy $\mathcal{A}(F)=1$, úgy is, hogy $\mathcal{A}\vDash F$, úgy is, hogy $\mathcal{A}\in\mathrm{Mod}(F)$, úgy is mondjuk, hogy $\mathcal{A}$ kielégíti $F$-et és úgy is, hogy $\mathcal{A}$ egy modellje az $F$-nek ha $F$ formula, akkor $\mathrm{Mod}(F)$ az összes olyan struktúra osztálya (note: az osztály olyan, mint egy halmaz, csak lehet nagyobb is; struktúrákból simán lehet olyan sok, hogy nem férnek bele egy halmazba, ezért $\mathrm{Mod}(F)$ officially "osztály", nem "halmaz" de a mi szempontunkból nem lesz különbség), amik kielégítik $F$-et: $\mathrm{Mod}(F)~:=~\{\mathcal{A}:~\mathcal{A}\vDash F\}$ ha $F$ és $G$ formulák, akkor $F\vDash G$ azt jelöli, hogy $\mathrm{Mod}(F)\subseteq\mathrm{Mod}(G)$, úgy mondjuk, hogy $F$-nek következménye $G$ (és továbbra is azt jelenti tehát, hogy ha egy $\mathcal{A}$ struktúrában $F$ igaz, akkor $G$ is) formulák helyett föntebb mindenhol írhatunk formulahalmazt is: $\mathcal{A}\vDash\Sigma$ akkor igaz, ha $\mathcal{A}$ modellje $\Sigma$ összes elemének $\mathrm{Mod}(\Sigma)$-ban azok a struktúrák vannak benne, melyek modelljei $\Sigma$ összes elemének $\Sigma\vDash F$ azt rövidíti, hogy $\mathrm{Mod}(\Sigma)\subseteq\mathrm{Mod}(F)$, azaz hogy $\Sigma$-nak $F$ következménye $\Sigma\vDash\Gamma$ azt, hogy $\mathrm{Mod}(\Sigma)\vDash F$ minden $F\in\Gamma$-ra

Mivel itt megint a $\vDash$ által meghatározott Galois-kapcsolatról beszélünk, így az abból kijövő dolgok, amiket néztünk ítéletkalkulusban, itt is megmaradnak, majd amikor szükség lesz rájuk, listázom őket.

Tehát, ha az ember a számokról akar bizonyítani egy formulát, azaz a természetes számok szokásos $\mathcal{N}=(\mathbb{N}_0,I)$ struktúrájában akarja megmutatni egy $F$ mondatra, hogy $\mathcal{N}\vDash F$, akkor erre egy módszer az, hogy felírunk egy csomó formulát egy $\Sigma$ halmazba, melyekről tudjuk, hogy igazak a természetes számokra, és eztán az $F$ formulánkra megpróbáljuk bebizonyítani, hogy $\Sigma\vDash F$. A logikai következmény fogalma miatt ha ez sikerül, akkor mivel $\mathcal{N}\vDash\Sigma$, ezért ekkor $\mathcal{N}\vDash F$ is igaz lesz és a formula tényleg igaz ebben a struktúrában.

(Ilyen bizonyítást majd a Floyd-Hoare kalkulusban fogunk látni, ott visszatérünk erre még.)

A természetes számokra nagyon gyakran használt ilyen $\Sigma$ formulahalmaz a Peano-féle axiómarendszer. Ebben a struktúrában használjuk a $+/2$, $\times/2$ és $'/1 $ függvényjeleket, előbbieket infix, utóbbit posztfix szoktuk írni, interpretációjuk rendre az összeadás, szorzás és növelés eggyel, a $0/0$ konstansjelet, aki a $0$ számot jelöli és a $\leq/2$ predikátumjelet (az $=/2$ mellett), ami pedig a szokásos kisebb-egyenlő relációt. Az axiómák:

$\forall x(\neg(x'=0))$. ez igaz, hiszen azt állítja, hogy minden $n\in\mathbb{N}_0$ természetes számra $n+1\neq 0$. $\forall x\forall y(x'=y'~\to~x=y)$ ez meg azt, hogy ha $n+1=m+1$, akkor $n=m$. Persze, az eggyel növelés függvény injektív. $\forall x(x+0=x)$ hát igen, ha valamihez nullát adunk, nem változik $\forall x\forall y(x+y'=(x+y)')$ eszerint meg $n+(m+1)=(n+m)+1$, ez is stimmel $\forall x(x\times 0=0)$ yep, bármit nullával szorozva nullát kapok $\forall x\forall y(x\times y'=x\times y+x)$ disztributivitás: tetszőleges $n,m$ természetes számokra $n\times(m+1)=n\times m+n$, oké $\forall x(x\leq 0~\to~x=0)$ ez is stimmel, ha egy természetes szám legfeljebb nulla, akkor az nulla $\forall x\forall y(x\leq y'~\to~(x\leq y\vee x=y'))$ ez azt mondja, hogy ha $n\leq m+1$, akkor vagy $n\leq m$, vagy pedig $n=m+1$. Stimmel, hiszen ha $n>m$, és $n\leq m+1$, akkor $n$ csak $m+1$ lehet. Ez az axióma lényegében azt állítja, hogy $n$ és $n+1$ között nincs több természetes szám. $\forall x\forall y(x\leq y\vee y\leq x) stimmel ez is, ezpz és az indukciós axióma séma: $(F(0)\wedge(\forall x(F(x)\to F(x'))))\to\forall x F(x)$  ahol $F=F(x)$ egy olyan formula, amiben csak az $x$ változó szerepel szabadon, az $F(0)$ az $F$-ből úgy áll elő, hogy a szabad $x$-ek helyére $0$-t írunk mindenhol, az $F(x')$ meg úgy, hogy $x'$-t. ez azt állítja, hogy ha egy formula igaz $0$-ra és az is igaz, hogy tetszőleges $n$ esetén ha a formula igaz $n$-re, akkor igaz $n+1$-re is, akkor a formula igaz minden természetes számra. Ez is igaz, ezen alapszik a teljes indukció.

Tehát azt, hogy valami igaz a természetes számok struktúrájában, sokszor úgy szoktuk megmutatni, hogy "mert következménye a Peano axiómáknak". Egyelőre következtető algoritmusunk nincs az elsőrendű logikában, de nézünk egyet, amit ha valaki nem ért meg elsőre, nem baj:

Meg akarjuk mondjuk mutatni, hogy $\forall x\forall y\forall z(z\times(y+x)=z\times y+z\times x)$. Ez a teljes disztributivitás, az ilyesmiről szóló Peano axióma az csak $x=1$-re mondja, hogy teljesül.  Ha levágjuk a formula elejéről az első kvantort: $F=\forall y\forall z(z\times(y+x)=z\times y+z\times x)$ pont egy olyan formulát kapunk, amiben egy szabad változó szerepel, ez történetesen most épp $x$, de lehetne más is. Ha ezzel az $F=F(x)$-szel az indukciós axióma sémát akarjuk powerelni, akkor először is meg kell néznünk, hogy $F(0)$ következik-e e a Peano axiómákból: $F(0)=\forall y\forall z(z\times(y+0)=z\times y+z\times 0)$ ez kéne következzen belőlük. Ugyan még nem ismerünk következtetési szabályt, de a következők elég validnak tűnnek: $\begin{align*}\forall x(x+0=x)&\vDash\forall y(y+0=y)\tag{változó átnevezés}\\\forall x(x\times 0=0)&\vDash\forall z(z\times 0=0)\tag{változó átnevezés}\\\forall y(y+0=y)&\vDash\forall y\forall z(z\times(y+0)=z\times y)\\\forall x(x+0=x)&\vDash\forall y\forall z(z\times y=z\times y+0)\\\{\forall y\forall z(z\times (y+0)=z\times y),~\forall y\forall z(z\times y=z\times y+0)\}&\vDash\forall y\forall z(z\times(y+0)=z\times y+0)&\tag{az egyenlőség tranzitív}\\\forall z(z\times 0=0)&\vDash\forall y\forall z(z\times y+0=z\times y+z\times 0)\\\{\forall y\forall z(z\times(y+0)=z\times y+0), \forall y\forall z(z\times y+0=z\times y+z\times 0)\}&\vDash\forall y\forall z(z\times(y+0)=z\times y+z\times 0)&\tag{az egyenlőség tranzitív}\end{align*}$ ami épp $F(0)$. Tehát ez seems kijön a Peano axiómákból. Vajon az indukciós axióma séma középső része, $\forall x(F(x)\to F(x'))$ is következik belőlük? Írjuk ki: $\forall x\Bigl(\forall y\forall z(z\times (y+x)=z\times y+z\times x)\to\forall y\forall z(z\times (y+x')=z\times y+z\times x')\Bigr)$ hm. Ezt már az olvashatóság kedvéért informálisabban írom, hogy hogy megy: $z\times (y+x)=z\times y+z\times x$-ből indulunk. Az $x\times y'=x\times y+x$ axiómát használva kapjuk, hogy $z\times(y+x)'=z\times (y+x)+z$, majd ezen a jobb oldali $z\times (y+z)=z\times y+z\times x$-et átírva kapjuk, hogy $z\times(y+x)'=z\times y+z\times x+z$. Ennek a jobb oldalán a $x\times y'=x\times y+x$ axiómát "alkalmazva" "jobbról balra" kapjuk, hogy$z\times(y+x)'=z\times y+z\times x'$. A bal oldalán még alkalmazzuk az $(x+y)'=x+y'$ axiómát is, és kapjuk, hogy $z\times(y+x')=z\times y+z\times x'$. És pont ezt akartuk kihozni, ez a $F(x)\to F(x')$ implikáció jobb oldala erre az $F$-re! Ezért mivel az indukciós axióma séma bal oldalán lévő éselés mindkét tagja kijön a Peano axiómákból, így le tudjuk vezetni a jobb oldalát is és kapjuk, hogy következményük a $\forall x\forall y\forall z(z\times(y+x)=z\times y+z\times x)$ formula is. weeee.

Érdemes észrevenni, hogy a levezetés közben semmilyen plusz tudást nem vetettünk be a számokról, kizárólag az axiómákat használtuk és (valamiféle) logikai követktetéseket, amik a formulák szintaktikus átirkálásával készültek, azok jelentésének ismerete nélkül!
Ez pedig azért lesz jó, mert így van rá esély, hogy algoritmizálható.
Mindenesetre, levezettük, hogy a természetes számok struktúrájában az $x\times(y+z)=(x\times y)+(x\times z)$ azonosság teljesül, hiszen következménye a Peano axiómáknak.
Felmerül a kérdés, hogy mit lehet tenni, ha nem sikerül levezetnünk, hát, ilyenkor vagy az van, hogy nem is igaz a mondat a természetes számokra és meg lehet próbálni levezetni az ellentétét; ha ez se jön össze, akkor vagy csak nem vártunk eleget, hogy kijöjjön a következtetés, vagy fel kell venni még axiómát, ami garantáltan igaz a természetes számokra, hátha azzal együtt már ki tudja hozni a következtető rendszer...

folytköv

04 - elég a szabad változók értékét megadni - bizonyítás

previously on Heroes

Tehát, most nézzük meg formálisan, hogy tényleg kijön a "formula értékét egy struktúrában csak a benne szabadon elődorduló változók alapértéke befolyásolja, a többié nem" állítás.

Mivel a szokásos módon indukcióval látjuk be, ezért előbb a termekkel kezdjük. Ott minden változó "szabad", aki csak előfordul, hiszen termben nincs kvantor. Másrészt, azt, hogy "nem befolyásolja", azt úgy mondhatjuk matekul, hogy "ha két struktúra megegyezik mindenben, kivéve esetleg olyan változók alapértékét, ami nincs is a termben, akkor bennük a term értéke ugyanaz lesz", hiszen ez jelenti azt, hogy tkp mindegy, milyen alapértéket adunk ezeknek a változóknak.

Formálisan:

Legyen $t$ term, $\mathcal{A}=(A,I,\varphi)$ és $\mathcal{A}'=(A,I,\varphi')$ pedig két struktúra, melyekben minden $t$-ben előforduló $x$ változó esetén $\varphi(x)=\varphi'(x)$.  Akkor $\mathcal{A}(t)=\mathcal{A}'(t)$.

A bizonyítás $t$ felépítése szerinti indukcióval zajlik ofc:

ha a $t$ term egy $x$ változó, akkor $t$-ben persze hogy előfordul $x$, ezért a feltétel szerint $\varphi(x)=\varphi'(x)$. Másrészt az $\mathcal{A}$ struktúrában a term kiértékelés definíciója szerint $\mathcal{A}(t)=\varphi(x)$, a másikban pedig $\mathcal{A}'(t)=\varphi'(x)$. Összerakva kijön az egyenlőség: $\mathcal{A}(t)=\varphi(x)=\varphi'(x)=\mathcal{A}'(t)$ . ha pedig $t=f(t_1,\ldots,t_n)$ egy összetett term, akkor ugye tudjuk az állítás feltételéből, hogy minden $x$-re, aki $t$-ben bárhol szerepel, igaz, hogy $\varphi(x)=\varphi'(x)$. Persze aki bármelyik $t_i$-ben szerepel, az $t$-ben is, ezért az is igaz, hogy minden $i$-re minden $t_i$-beli $x$ változóra $\varphi(x)=\varphi'(x)$. Ezért a $t_i$-kre, akik egyszerűbb termek, mint $t$, alkalmazhatjuk az indukciós feltevést, ebből azt kapjuk, hogy minden $i$-re $\mathcal{A}(t_i)=\mathcal{A}'(t_i)$. Összerakva az összetett term kiértékelésének definíciójával a két struktúrában kijön az egyenlőség: $\begin{align*}\mathcal{A}(f(t_1,\ldots,t_n))&=I(f)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n))\tag{term kiértékelés def}\\&=I(f)(\mathcal{A}'(t_1),\ldots,\mathcal{A}'(t_n))\tag{indukció}\\&=\mathcal{A}'(f(t_1,\ldots,t_n)).\tag{term kiértékelés def}\end{align*}$

Ez nem volt nehéz, de csak azért csináltuk, hogy a formulákra vonatkozó ugyanilyen állítás (ami viszont fontos, hogy csak a szabad változókra vonatkozzon!) atomi formulákra vonatkozó részét be tudjuk látni. Lássunk neki:

Legyen $F$ formula, $\mathcal{A}=(A,I,\varphi)$ és $\mathcal{A}'=(A,I,\varphi')$ pedig két struktúra, melyekben minden, $F$-ben szabadon előforduló $x$ változóra $\varphi(x)=\varphi'(x)$. Akkor $\mathcal{A}(F)=\mathcal{A}(F)$.

A bizonyítás (surprise) $F$ felépítése szerinti indukcióval zajlik, sok eset van:

ha az $F$ formula egy $p(t_1,\ldots,t_n)$ atomi formula, akkor benne minden változóelőfordulás szabad. Tehát a feltétel azt mondja, hogy minden $F$-beli $x$ változóra $\varphi(x)=\varphi'(x)$. Persze ami egy $t_i$ termben előfordul, az az őt tartalmazó $F$-ben is, ezért az is igaz az állítás feltétele szerint, hogy minden $i$-re igaz, hogy minden, a $t_i$-ben előforduló $x$ változóra $\varphi(x)=\varphi'(x)$. Ezért, alkalmazhatjuk a termekre vonatkozó, az imént belátott állításunkat és azt kapjuk, hogy minden $i$-re $\mathcal{A}(t_i)=\mathcal{A}'(t_i)$. Ezt kombinálva az atomi formula kiértékelésének definíciójával a két struktúrában, kijön az egyenlőség: $\begin{align*}\mathcal{A}(p(t_1,\ldots,t_n))&=I(p)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n))\tag{atomi szemantika def}\\&=I(p)(\mathcal{A}'(t_1),\ldots,\mathcal{A}'(t_n))\tag{indukció}\\&=\mathcal{A}'(p(t_1,\ldots,t_n)).\tag{atomi szemantika def}\end{align*}$ Nyilván ha $F=\uparrow$ vagy $F=\downarrow$, akkor $\mathcal{A}(F)=\mathcal{A}'(F)$, bármi is van. Konstans $1$ vagy konstans $0$. (most jönnek az unalmas részek) Ha $F=(\neg G)$, akkor ami $G$-ben szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben szabadon előfordul, $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit a negálás szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(\neg G)&=\neg\mathcal{A}(G)\tag{$\neg$ kiértékelés def}\\&=\neg\mathcal{A}'(G)\tag{indukció}\\&=\mathcal{A}'(G)\tag{$\neg$ kiértékelés def}\end{align*}$ Ha $F=(G\vee H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit a vagyolás szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\vee H)&=\mathcal{A}(G)\vee\mathcal{A}(H)&\tag{$\vee$ kiértékelés def}\\&=\mathcal{A}'(G)\vee\mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\vee H)\tag{$\vee$ kiértékelés def}\end{align*}$ Ha $F=(G\wedge H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit az éselés szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\wedge H)&=\mathcal{A}(G)\wedge \mathcal{A}(H)&\tag{$\wedge $ kiértékelés def}\\&=\mathcal{A}'(G)\wedge \mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\wedge H)\tag{$\wedge $ kiértékelés def}\end{align*}$ Ha $F=(G\to H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit az implikáció szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\to H)&=\mathcal{A}(G)\to \mathcal{A}(H)&\tag{$\to $ kiértékelés def}\\&=\mathcal{A}'(G)\to \mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\to H)\tag{$\to $ kiértékelés def}\end{align*}$ Ha $F=(G\leftrightarrow H)$, akkor ami akár $G$-ben, akár $H$-ban szabadon előfordul, az $F$-ben is, tehát minden olyan $x$ változóra, ami $G$-ben (ill. $H$-ban) szabadon előfordul, igaz az állítás feltétele szerint, hogy $\varphi(x)=\varphi'(x)$. Ezért alkalmazhatjuk az indukciós hipotézist, amit a kettősnyíl szemantikájával kombinálva kijön: $\begin{align*}\mathcal{A}(G\leftrightarrow H)&=\mathcal{A}(G)\leftrightarrow \mathcal{A}(H)&\tag{$\leftrightarrow $ kiértékelés def}\\&=\mathcal{A}'(G)\leftrightarrow \mathcal{A}'(H)&\tag{indukció}\\&=\mathcal{A}'(G\leftrightarrow H)\tag{$\leftrightarrow $ kiértékelés def}\end{align*}$ Ha $F=\exists xG$ vagy $F=\forall xG$ alakú formula, akkor elég azt belátnunk, hogy minden $a\in A$ objektum esetén $\mathcal{A}_{[x\mapsto a]}(G)=\mathcal{A}'_{[x\mapsto a]}(G)$, hiszen ezekből az értékekből számítjuk ki $\mathcal{A}(F)$-et és $\mathcal{A}'(F)$-et. A $G$ formulában kik fordulhatnak elő szabadon? Ugyanazok, mint akik $F$-ben, plusz esetleg $x$. (Ha $G$-ben nincs szabadon $x$, azaz ha a kvantor le se kötött senkit, akkor csak azok, akik $F$-ben, egyébként még $x$ is pluszban.) No de akkor a $G$-beli szabadon előforduló összes (mondjuk) $y$ változóra vagy $y$ szabadon előfordult $F$-ben is, ezért az állítás feltétele miatt $\varphi(y)=\varphi'(y)$ volt és mivel $x\neq y$ (az $x$ mindenhol kötve van $F$-ben, hiszen kvantált $x$-szel kezdődik), ezért a két $[x\mapsto a]$-val származtatott struktúrában nem írtuk át az értékeiket, így azokban is megegyezik a default értékük; vagy $y=x$, de annak meg a default értéke $\mathcal{A}_{[x\mapsto a]}$-ban is és $\mathcal{A}'_{[x\mapsto a]}$-ban is $a$, tehát megegyezik. Ezért az indukciós feltevést alkalmazhatjuk $G$-re a két származtatott struktúrában és kapjuk, hogy minden $a\in A$-ra $\mathcal{A}_{[x\mapsto a]}(G)=\mathcal{A}'_{[x\mapsto a]}(G)$. Ami miatt persze $\begin{align*}\mathcal{A}(\exists G)=1&\Leftrightarrow\hbox{van olyan }a\in A\hbox{, melyre }\mathcal{A}_{[x\mapsto a]}(G)=1&\tag{$\exists$ def}\\&\Leftrightarrow\hbox{van olyan }a\in A\hbox{, melyre }\mathcal{A}'_{[x\mapsto a]}(G)=1\tag{ezt láttuk be az előbb}\\&\Leftrightarrow\mathcal{A}'(\exists G)=1\tag{$\exists$ def}\end{align*}$ és $\begin{align*}\mathcal{A}(\forall G)=1&\Leftrightarrow\hbox{minden }a\in A\hbox{-ra }\mathcal{A}_{[x\mapsto a]}(G)=1&\tag{$\forall$ def}\\&\Leftrightarrow\hbox{minden }a\in A\hbox{-ra }\mathcal{A}'_{[x\mapsto a]}(G)=1\tag{ezt láttuk be az előbb}\\&\Leftrightarrow\mathcal{A}'(\forall G)=1\tag{$\forall$ def}\end{align*}$.

Látszik, hogy a bináris konnektívákra vonatkozó esetek tényleg copypaste készíthetőek, meg a két kvantor esete is nagyon hasonló: legközelebb már az ilyeneket összevonjuk úgy, hogy "ha $\bullet\in\{\vee,\wedge,\to,\leftrightarrow\}$, akkor$\ldots$".

Mindenesetre, kijött, hogy a formula értéke tényleg csak a benne szabadon előforduló változók default értékétől függ, a többitől nem.

Ezért:

Egy mondat értéke egy $\mathcal{A}=(A,I,\varphi)$ struktúrában a $\varphi$-től nem függ. Ezért ha mondatok értékéről beszélünk, úgy $\varphi$-t elhagyhatjuk és egy struktúrára úgy tekintünk, mint egy $\mathcal{A}=(A,I)$ párra.

folytköv

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

02 - Elsőrendű logika - szemantika

previously on Heroes
Ítéletkalkulusban ha volt egy formulánk, könnyedén kiértékelhettük: csak adnunk kellett egy változó-értékadást, ami a változóknak beállította az értékét 0-ra vagy 1-re, és ezeket az értékeket alulról felfelé terjesztettük, a végén megkapva az egész formula értékét.

Az alulról felfelé értékelés továbbra is megmarad, de a "változóértékadás" helyett egy sokkal komplexebb dolgot kell megadjunk, ha formulát akarunk kiértékelni: egy struktúrát. ami egy

$\mathcal{A}~=~(A,I,\varphi)$

hármas. (Ez csak annyit jelent, hogy három dolgot kell megadjunk, az elsőnek a neve $A$ lesz, a másodiké $I$, a harmadiké $\varphi$, mindjárt mondom, hogy minek mi a "típusa" és ezt a hármat együtt elnevezhetjük $\mathcal{A}$-nak is. Általában egy struktúrát nagy "írott" betűvel jelölünk, az első komponensét ugyanannak a betűnek a sima nagybetűs változatával.)

Egy ilyen hármasban

$A$ egy nemüres halmaz, az objektumok halmaza, hívják alaphalmaznak vagy univerzumnak is. (őket veszik majd fel értékül a termek.) $\varphi$ a változóknak egy "default" értékadása, azaz egy olyan függvény, ami minden $x$ változóhoz egy $\varphi(x)\in A$ objektumot rendel. $I$ pedig az interpretációs függvény, ami a függvény- és predikátumjeleknek ad "jelentést": az $f$ függvényjelhez az $I(f)$-fel jelölt függvényt, a $p$ predikátumjelhez az $I(p)$-vel jelölt predikátumot rendeli. Konkrétan: ha $f/n$ egy ($n$-változós) függvényjel, akkor $I(f)$ egy $A^n\to A$ függvény ha $p/n$ egy ($n$-változós) predikátumjel, akkor $I(p)$ egy $A^n\to\{0,1\}$ predikátum. itt van egy megkötés: ha van $=/2$ predikátumjel, akkor $I(=)$ mindenképp tényleg az egyenlőség predikátum kell legyen.

Például ha a függvényjeleink $f/1$, $g/2$ és $c/0$, predikátumjeleink pedig $p/1$ és $q/2$, akkor egy struktúra lehet pl. az az $\mathcal{A}=(A,I,\varphi)$, ahol $A=\mathbb{N}_0=\{0,1,2,\ldots\}$ a természetes számok ($0$-t is tartalmazó) halmaza; $\varphi(x)=2$, $\varphi(y)=3$, $\varphi(z)=7$, \ldots (nem adom meg az egészet, de mind a végtelen sok változónak van valami alap értéke) az $I$ interpretációs függvényünk pedig $f$-hez egy $\mathbb{N}_0\to\mathbb{N}_0$ függvényt, $g$-hez egy $\mathbb{N_0}^2\to\mathbb{N_0}$ függvényt, $c$-hez egy $\to\mathbb{N}_0$ függvényt, azaz egy $\mathbb{N}_0$-beli értéket kell rendeljen, $p$-hez egy egyváltozós $\mathbb{N}_0\to\{0,1\}$ predikátumot, $q$-hoz pedig egy $\mathbb{N}_0\times\mathbb{N}_0\to\{0,1\}$ predikátumot. Akár így:  $\begin{align*}I(f)(n)&:=n+1&&\hbox{tehát $f$ az ,,adj hozzá egyet'' függvény}\\I(g)(n,m)&:=n+2m&&\hbox{why not, függvény ez is}\\I(c)&=7&&\hbox{konstans, egy eleme az alaphalmaznak}\\I(p)(n)=1&\Leftrightarrow n\hbox{ prímszám}&&\hbox{predikátumról azt adjuk meg pl, hogy mikor igaz}\\I(q)(n,m)=1&\Leftrightarrow n<m\end{align*}$

(note to self: a $\LaTeX$ben lévő text fonttal kezdenem kell valamit.)

Egy ilyen struktúra már elegendő információt szolgáltat ahhoz, hogy minden termnek legyen egy értéke benne és minden formulának is (bár ezt az értéket nem biztos, hogy ki is lehet számítani!). Kezdjük a termekkel, hiszen alulról kifelé akarunk kiértékelni és a termek vannak "belül". Ez lesz az egyszerűbb is, hiszen a termeknek összesen két konstruktora volt:

Ha $t$ egy term és $\mathcal{A}=(A,I,\varphi)$ egy struktúra, akkor $t$ értéke $\mathcal{A}$-ban egy $A$-beli objektum lesz, amit $\mathcal{A}(t)$-vel jelölünk (tehát mintha a termet behelyettesítenénk $\mathcal{A}$-be, mint függvénybe) és felépítés szerinti indukcióval definiálunk (ami még mindig annyit jelent, hogy minden képzési szabályra felírunk egy "ha a termet így építettük fel, akkor ez legyen az értéke, ha úgy, akkor az" szabályt úgy, hogy használhatjuk a "kisebb" termek értékét is. Mégpedig így:

ha a $t$ term egy $x$ változó, akkor $\mathcal{A}(t)~:=~\varphi(x)$ azaz: a változók értékét $\varphi$ mondja meg ha pedig a $t$ term egy $f(t_1,\ldots,t_n)$ alakú összetett term, akkor $\mathcal{A}(t)~:=~I(f)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n))$. azaz: ha egy összetett termet kell kiértékelnünk, akkor rekurzívan értékeljük ki az "argumentumait", majd ezt a kapott $n$ objektumot helyettesítsük be abba a függvénybe, amit $\mathcal{A}$-ban jelöl a term gyökérszimbóluma (a képen ez az $f$, ami jelöli az $I(f)$ függvényt).

és ez minden, mert ez a két konstruktorunk volt.

Például az előző struktúrában a természetes számok fölött: $\mathcal{A}(x)=\varphi(x)=2$, ez volt $x$ alapértéke a példa struktúra $\varphi$-jében $\mathcal{A}(f(x))=I(f)(\mathcal{A}(x))=I(f)(2)=2+1=3$, mert az $f$ ebben a struktúrában az "adj hozzá $1$-et" függvény volt, az argumentum értéke pedig $2$ $\mathcal{A}(g(f(x),y))=I(g)(3,3)=3+2\cdot 3=9$, mert $g$ volt az "add össze az első argumentumot és a második dupláját" függvény, az első argumentumának az értéke $3$, a másodiké pedig $\varphi(y)=3$ szintén

A formulák kiértékelése eggyel komplikáltabb és kell hozzá még egy jelölés, mert a kvantorok megváltoztatják a változók értékét (ha informatikusul akarjuk elképzelni, akkor kb "végighúznak egy ciklust a változó összes lehetséges értékével"):

Ha $\mathcal{A}=(A,I,\varphi)$ egy struktúra, $x$ egy változó, $a\in A$ pedig egy objektum, akkor $\mathcal{A}_{[x\mapsto a]}$ azt a struktúrát jelöli, ami összesen annyiban tér el $\mathcal{A}$-tól, hogy benne $x$ default értéke $a$, minden más ugyanaz. Vagyis: $\mathcal{A}_{[x\mapsto a]}=(A,I,\varphi')$, tehát ugyanaz marad az objektumok halmaza és minden függvény- és predikátumjel is ugyanazt jelenti, csak a változók default értékadása változik $\varphi'$-vé, ahol  $\varphi'(x)=a$ (erre változott) és minden másik $y\neq x$-re $\varphi'(y)=\varphi(y)$ (a többi változó értéke nem változik).

Most, hogy ez a jelünk megvan, definiálhatunk: ha $F$ egy formula és $\mathcal{A}$ egy struktúra, akkor $F$ értéke $\mathcal{A}$-ban egy $\{0,1\}$-beli igazságérték lesz, amit $\mathcal{A}(F)$-fel jelölünk és $F$ felépítése szerinti indukcióval definiálunk. Csak most sok eset van, mert formulákat szintaktikailag is sokféleképp építhettünk fel. Mégpedig:

Ha $F=p(t_1,\ldots,t_n)$, akkor $\mathcal{A}(F)~:=~I(p)(\mathcal{A}(t_1),\ldots,\mathcal{A}(t_n)).$ azaz: ha atomi formulát kell kiértékelnünk, akkor először is kiértékeljük benne a termeket, aztán megnézzük, hogy milyen predikátumot jelöl ebben a struktúrában a gyökérszimbólum (ami itt most $p$), és ebbe a predikátumba behelyettesítjük az $n$ darab termünk értékeit a megfelelő sorrendben. Ha $F=\uparrow$, akkor $\mathcal{A}(F)~:=~1$ (az $\uparrow$ formula igaz, ok) Ha $F=\downarrow$, akkor $\mathcal{A}(F)~:=~0$ (a $\downarrow$ formula hamis, ok) Ha $F=(\neg G)$, akkor $\mathcal{A}(F)~:=~\neg\mathcal{A}(G)$ (ha egy $\neg G$ alakú formulát kell kiértékelnünk, akkor értékeljük ki a $G$-t és negáljuk az eredményt, ok) Ha $F=(G\vee H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\vee\mathcal{A}(H)$ (ha egy vagyolást, akkor értékeljük ki a két közvetlen részformulát és vagyoljuk az eredményeket) Ha $F=(G\wedge H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\wedge\mathcal{A}(H)$ (éselésre ugyanez) Ha $F=(G\to H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\to\mathcal{A}(H)$ (implikációra ugyanez) Ha $F=(G\leftrightarrow H)$, akkor $\mathcal{A}(F)~:=~\mathcal{A}(G)\leftrightarrow\mathcal{A}(H)$ (duplanyílra ugyanez, eddig semmi meglepetés nem történt) Ha $F=\exists xG$, akkor $\mathcal{A}(F):=\begin{cases}1&\hbox{ha van olyan }a\in A\hbox{, melyre }\mathcal{A}_{[x\mapsto a]}(G)=1\\0&\hbox{ha nincs}\end{cases}$ azaz: mintha végigmennénk egy "ciklussal" az $x$ összes lehetséges értékén, és ha találunk egyet is, melyre beállítva $x$-et a formula "magja" igaz lesz, akkor ez a formula is igaz, ha meg mindenre hamis lesz, akkor hamis. Ha $F=\forall xG$, akkor $\mathcal{A}(F):=\begin{cases}1&\hbox{ha minden }a\in A\hbox{-ra }\mathcal{A}_{[x\mapsto a]}(G)=1\\0&\hbox{ha nem}\end{cases}$ azaz: mintha végigmennénk egy "ciklussal" az $x$ összes lehetséges értékén, és ha találunk egyet is, melyre beállítva $x$-et a formula "magja" hamis lesz, akkor ez a formula is hamis ha meg mindenre igaz lesz, akkor igaz.

Például ebben az előző struktúrában $\mathcal{A}(p(f(x)))=I(p)(\mathcal{A}(f(x)))=I(p)(3)=1$, mert $I(p)(n)$ akkor volt $1$, ha $n$ prímszám és a $3$ egy prímszám. $\mathcal{A}(\forall xp(f(x)))$ akkor igaz, ha minden $a\in\mathbb{N}_0$-ra $\mathcal{A}_{[x\mapsto a]}(p(f(x))=1$. De mivel pl. az $a=3$-ra $\mathcal{A}_{[x\mapsto 3]}(p(f(x)))=I(p)(I(f)(3))=I(p)(4)=0$, mert ebben a struktúrában $x$ értéke $3$, $3+1$ az $4$ és a $4$ nem prímszám, ezért van olyan $a$, melyre a mag hamis lesz, ha erre állítjuk $x$ értékét, ezért $\mathcal{A}(\forall x p(f(x)))=0$.

A következő posztban majd látjuk, hogy ez azért nem megy mindig ilyen könnyen.
A kapcsolódó gyakanyag a hetedik, érdemes hozzáolvasni.

folytköv

01 - Elsőrendű logika - szintaxis

Ítéletkalkulusban egyszerű volt a dolgunk: voltak a $p_1,p_2,\ldots$ ítéletváltozóink, amiket lehetett összekötni a szokásos konnektívákkal, és ennyi: ami így felépült, az formula volt, ami meg nem, az nem, ennyi volt a szintaxis.

Elsőrendű logikában viszont a változók (amiket "individuum"változóknak nevezünk teljes néven, de mostantól őket illeti a default "változó" kifejezés) nem egy szimpla 1/0 (avagy igaz/hamis) értéket vesznek fel kiértékeléskor, hanem egy objektumot valamiféle alaphalmazból. Adja magát, hogy máris kétféle "szintaktikus kategóriára" lesz szükségünk: egy olyanra, ami objektumot vesz majd fel értékül (ők lesznek majd a "term"-ek), és egy olyanra, ami egy 1/0 bitet, igazságértéket (ők meg a "formulák").

Sőt, lesznek függvényjeleink és predikátumjeleink is: amikor aláteszünk egy "melyik jel mit is jelent"-et (egy struktúrát, ez lesz a szemantika része), akkor mindkettő objektumokat vár majd inputként, nullát, egyet, kettőt vagy többet, a különbség az output lesz: a függvényjelhez rendelt tényleges függvény objektumot ad vissza, a predikátumjelhez rendelt predikátum pedig igazságértéket.

Egyelőre amíg a szintaxist adjuk meg, addig csak azt mondjuk meg, hogy milyen stringeket fogadunk el valamilyen típusú kifejezésnek (termnek vagy formulának), addig persze a jelentésükkel nem foglalkozunk, ez a szemantika része lesz (de azért valami intuíció nem árthat).

Szóval, elsőrendű logikában ami féle jeleket használunk:

• (individuum)változókat: nekik "hivatalosan" $\{x_1,x_2,x_3,\ldots \}$ a halmazuk, de azért, hogy a példák könnyebben parsolhatóak legyenek, fogunk használni betűket az ábécé környékéről is változónak, pl $x$, $y$, $z$, $w$, vesszőzve, indexelve ízlés szerint.
• függvényjeleket: az ő halmazuk az $\{f_1,f_2,f_3,\ldots\}$, de az ábécé elejét kb. $h$-ig megint csak függvényjeleknek fogjuk lefoglalni a példákban. Minden függvényjelnek van egy aritása, ami "változószámot" jelent, természetes szám (lehet $0$ is), azt adja meg, hogy hány változós ez a függvény; ha az $f$ függvényjel $n$-változós, azt $f/n$ fogja jelölni.
• például a jól ismert "összeadás" az egy kétváltozós függvény, a "szorzás kettővel" meg egyváltozós függvény, így az őket jelölő függvényjelek aritása 2, ill. 1 lesz. 
• Nullaváltozós függvény egy konstans: nem kap semmi inputot és kiad egy objektumot, az tkp maga az objektum lesz. A nulla aritású függvényjeleket konstansjelnek hívjuk.
• A példákban  $a$-tól $d$-ig fogjuk általában a konstansjeleket, $f$-től $h$-ig a nem-konstans függvényjeleket jelölni. $e$-t nem használunk :D
• predikátumjeleket: az ő halmazuk a $\{p_1,p_2,p_3,\ldots\}$ (pont úgy, mint eddig az ítéletváltozóké volt; ez nem véletlen), de az ábécénak a $p,q,r$ betűit erre fogjuk használni. A predikátumjeleknek is van aritásuk, ha $p$ egy $n$-változós predikátumjel, azt $p/n$ jelöli.
• például az "egyenlőség" az egy bináris predikátum lesz: bejön két objektum, eredmény akkor igaz, ha ugyanaz a két objektum, egyébként hamis. Ennek a predikátumnak a jele = lesz. A (valós, mondjuk) számok közt a "kisebb" szintén egy bináris predikátum: bejön két szám, igaz, ha a bal oldali kisebb, mint a jobb oldali, ezt a predikátumot jelölheti például a $</2$  predikátumjel.
• Nullaváltozós predikátum is lehet: nem kap semmi inputot és kiad egy igazságértéket.. ilyet már láttunk, a nulla aritású predikátumjeleket ítéletváltozóknak hívjuk majd.
• logikai konnektívákat: $\neg$, $\vee$, $\wedge$, $\to$, $\leftrightarrow$, $\uparrow$, $\downarrow$, az utolsó kettőt "logikai konstansjelnek" is hívjuk.
• nyitójelet $($, csukójelet $)$, vesszőt $,$ szeparátornak.

Ezekből a jelekből megint csak szintaktikai szabályokkal építhetünk fel valid stringeket, csak most kétfélét:  az első a termek szintaktikus kategóriája, aminek a képzési szabályai:

minden változó term ha $f/n$ függvényjel és $t_1,\ldots,t_n$ termek, akkor $f(t_1,\ldots,t_n)$ is term más term nincs.

Például ezek szerint ha $x$ és $y$ változók, $c/0$ konstansjel, $f/1$ (egyváltozós) függvényjel és $g/2$ (kétváltozós) függvényjel, akkor $x$ term, mert változó. $y$ is term, mert változó. $f(x)$ is term, mert $f$ egyváltozós függvényjel és belehelyettesítettünk egy termet, $x$-et. $g(y,f(x))$ is term, mert $g/2$ függvényjel, amibe behelyettesítettünk két termet, $y$-t és $f(x)$-et. $c()$ is term, mert $c/0$ függvényjel (konstansjel) és belehelyettesítettünk nulla termet. $g(c(),c())$ is term, mert $g/2$ függvényjel és belehelyettesítettünk két termet, $c()$-t és aztán megint $c()$-t.

A könnyebb olvashatóság kedvéért

• a konstansjeleknél $c()$ helyett csak $c$-t írunk (fontos, hogy így "külsőre" úgy néznek ki, mint a változók! ezért fontos, hogy lássuk, hogy az ábécé elején van a betű - akkor konstans -, vagy a végén - akkor változó -, ha élünk ezzel az egyszerűsítéssel)
• "megszokott" függvényjeleknél, mint pl a $+/2$, infix is írjuk a függvényt: $+(x,y)$ helyett $x+y$ alakban.

 A formuláknak több képzési szabálya van:

ha $p/n$ predikátumjel és $t_1,\ldots,t_n$ termek, akkor $p(t_1,\ldots,t_n)$ egy formula. Ezeket atomi formulának is nevezzük. ha $F$ és $G$ formulák, akkor formulák még $(F\vee G)$, $(F\wedge G)$, $(F\to G)$, $(F\leftrightarrow G)$, $(\neg F)$ is. $\uparrow$ és $\downarrow$ is formulák. ha $x$ változó és $F$ formula, akkor $(\exists x F)$ és $(\forall x F)$ is formulák. más formula nincs.

Például ezek szerint ha $x$ és $y$ változók, $c/0$ konstansjel, $f/1$ és $g/2$ függvényjelek, $p/1$ (egyváltozós) predikátumjel, $r/2$ (kétváltozós, bináris) predikátumjel és $q/0$ nulla változós predikátumjel, azaz konstans, akkor  $p(x,f(y))$ egy (atomi) formula, mert $p/2$ predikátumjel, amibe behelyettesítettünk két termet, $x$-et és $f(y)$-t. $q()$ is atomi formula: $q/0$ predikátumjel, amibe behelyettesítettünk nulla darab termet. A zárójelet itt is elhagyhatjuk és maradhat csak $q$ is. $r(g(c,x))$ is atomi formula: $r/1$ predikátumjel, amibe behelyettesítettünk egy darab termet, $g(c,x)$-et. $(p(x,f(y))\wedge r(g(c,x)))$ két formula éselése, ez is formula. $\exists x(p(x,f(y))\wedge r(g(c,x)))$ egy formula elé betett kvantált változó, ez is formula. $\exists x(p(x,f(y))\wedge r(g(c,x)))\to q$ is formula, két formula van összekötve egy implikációval. (note: elhagytuk a kvantált rész körüli zárójelet, megint elhagyhatunk zárójeleket precedencia alapon. A kvantorok kötnek erősebben, mint a logikai konnektívák!) $\forall x(\exists x(p(x,f(y))\wedge r(g(c,x)))\to q)$ is formula, egy formula elé tettünk egy kvantált változót. (igen, ugyanazt, ami már le volt kötve. ez nem baj, szabadnak szabad, csak ritkán van értelme.) Nem valid string viszont például $x\vee\neg x$, mert negálni-vagyolni formulát lehet, de az $x$ az változó, tehát term  $\exists x(f(x))$, mert kvantálni formulát lehet, de az $f(x)$ term. $g(c)$ (az előző jelkészlet mellett), mert $g/2$-be két termet kéne helyettesíteni, nem csak egyet. $f(p(x))$, mert $x$ term, $p(x)$ formula, de $f/1$-be aki függvényjel, formulát nem helyettesíthetünk, csak termet.

Ennyi az elsőrendű logika szintaxisa. A következő a szemantika lesz, amiben megmondjuk, hogy ha az alap jeleknek adunk egy jelentést, hogy lesz abból értéke egy egész termnek, vagy egy egész formuláknak.
Önellenőrzésként érdemes lehet nyomkodni itt párszor a "Generálj Szintaktikus Elemzőset!" gombot, és megpróbálni eltalálni, hogy a string valid-e vagy sem, és ha nem, akkor hol is hibás, hogy biztos értünk-e minden képzési szabályt :)
A kapcsolódó gyakanyag a hatodik, érdemes hozzáolvasni.

folytköv