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