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