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.
|
No comments:
Post a Comment