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:
|
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:
$(F(0)\wedge(\forall x(F(x)\to F(x'))))\to\forall x F(x)$
|
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:
$\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...
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...
No comments:
Post a Comment