A kommutativitás bizonyítása - A részletezés jobbra nyitható!
Értelmezés sikertelen (ismeretlen „\textup” függvény): {\displaystyle \begin{array}{rcll} PA\cup \{(0+x)=x\} & \vdash & (0+x)=x & \textup{premissza levezethető} \\ PA\cup \{(0+x)=x\} & \vdash & s(0+x)=sx & \textup{elsőrendű logikai törvény}\\ PA\cup \{(0+x)=x\} & \vdash & s(0+x)=(0+sx) & \textup{3. axióma} \\ PA\cup \{(0+x)=x\} & \vdash & (0+sx)=sx & \textup{Az azonosságokból } \\ PA & \vdash & (0+x)=x\rightarrow (0+sx)=sx & \textup{Dedukciótétel} \\ PA & \vdash & \forall x ((0+x)=x\rightarrow 0+sx=sx) & \textup{Univerzális generalizáció}\\ PA & \vdash & F_x[0] \rightarrow \forall x( F \rightarrow F_x[sx]) \rightarrow F & \textup{7. axióma} \\ PA & \vdash & ((0+x)=x)_x[0]\forall x ((0+x)=x ((0+x)=x)_x[sx])((0+x)=x) & F:=(0+x=x) \\ PA & \vdash & (0+0)=0\rightarrow \forall x ((0+x)=x \rightarrow (0+sx)=sx )\rightarrow (0+x)=x & \textup{behelyettesítés} \\ PA & \vdash & (0+0)=0 & \textup{3. axióma} \\ PA & \vdash & \forall x ( (0+x)=x\rightarrow (0+sx)=sx)\rightarrow (0+x)=x & \textup{modus ponens}\\ PA & \vdash & (0+x)=x & \textup{modus ponens}\\ PA & \vdash & (x+0)=x & \textup{3.axióma}\\ PA & \vdash & (0+x)=(x+0) & \textup{Az azonosságokból } \\ PA & \vdash & \forall x (0+x)=(x+0) & \textup{Univerzális generalizáció}\\ PA \cup \{ (x+y)=(y+x) \}&\vdash & (x+y)=(y+x) & \textup{premissza levezethető} \\ PA \cup \{ (x+y)=(y+x) \}&\vdash & s(x+y)=s(y+x) & \textup{Elsőrendű logikai törvény} \\ PA \cup \{ (x+y)=(y+x) \}&\vdash & s(x+y)=(x+sy) & \textup{4. axióma}\\ PA\cup \{ (x+y)=(y+x) \}&\vdash & s(y+x)=(y+sx) & \textup{4. axióma}\\ PA\cup \{ (x+y)=(y+x) \}&\vdash & (x+sy)=(sy+x) & \textup{Az azonosságokból} \\ PA &\vdash & (x+y)=(y+x) \rightarrow (x+sy)=(sy+x) & \textup{Dedukciótétel} \\ PA &\vdash & \forall x (x+y)=(y+x) \rightarrow (x+sy)=(sy+x) & \textup{Univerzális generalizáció} \\ PA &\vdash & \forall x (x+y)=(y+x) \rightarrow \forall x ((x+ sy= (sy+x)) & \textup{2.axióma} \\ PA &\vdash & \forall y \forall x((x+y)=(y+x)\rightarrow \forall x (x+sy)=(sy+x) & \textup{Univerzális generalizáció} \\ PA & \vdash & F_x[0] \rightarrow \forall x( F \rightarrow F_x[ sx] \rightarrow F & \textup{7. axióma} \\ PA & \vdash & (\forall x (x+y)=(y+x))_x[0] \rightarrow \forall x( \forall x (x+y)=(y+x) \rightarrow (\forall x (x+y)=(y+x))_x[ sx] \rightarrow \forall x (x+y)=(y+x) & F :=\forall x (x+y)=(y+x)\\ PA & \vdash & \forall x (0+y)=(y+0) \rightarrow \forall x( \forall x (x+y)=(y+x) \rightarrow \forall x (sx+y)=(y+sx)) \rightarrow \forall x (x+y)=(y+x) & \textup{terminuscsere} \\ PA & \vdash & \forall y \forall x (x+y)=(y+x) \rightarrow \forall x (x+sy)=(sy+x) \rightarrow \forall x (x+y)=(y+x) & \textup{modus ponens}\\ PA & \vdash & \forall x (x+y)=(y+x) & \textup{modus ponens}\\ PA & \vdash & \forall y \forall x (x+y)=(y+x) & \textup{Univerzális generalizáció}\\ PA & \vdash & \forall x \forall y (x+y)=(y+x) & \textup{kvantorcsere} \\ \end{array} }
Peano-aritmetikai fogalmak és egyebek.
formulák osztálya
|
Bázis
|
|
|
|
|
Rekurzió
|
|
|
|
|
|
- Ha i meg j egyenlő k-val, akkor , ahol -ben i darab jel van, stb.
- Ha i-szer j egyenlő k-val, akkor , ahol -ben i darab jel van, stb.
- Ha egy változót nem tartalmazó terminus és i-t jelöli, akkor
- Ha és változót nem tartalmazó terminusok és ugyanazt jelölik, akkor
- j < i
formulák osztálya
|
Bázis
|
|
Rekurzió
|
|
*Ha i kisebb, mint j, akkor
- Ha i más, mint j, akkor
- Ha i nem kisebb, mint j, akkor
- Egy formula pszeudoterminus, ha
. A pszeudoterminusokat így szokás jelölni: . Minden pszeudoterminus egy n-argumentumú függvényt definiál.
Ha igaz, akkor
- tartalmazza az összes atomi formulát és a , , , alakú formulákat, zárt a Boole-műveletekre, a korlátos kvantifikációkra és a pszeudoterminusok bármely helyettesítésére.
- és pszeudoterminus
tételek S5-ből
|
|
|
|
|
|
S4-hez szép diagram a modalitások sorrendjéhez.
\[{\Huge \textbf{S4}} \begin{array}{c}\xymatrix{
\Box A \ar[r]\ar[dd]
& \Box \Diamond \Box A \ar[r]\ar[d] & \Diamond \Box A\ar[d]
\\ & \Box \Diamond A \ar[r] & \Diamond \Box \Diamond A\ar[d]
\\ A\ar[rr] && \Diamond A}\end{array}\]
K-s tételek:
Azaz:
haakkor:
és:
vagy:
érvényes formulák K-ból
|
|
|
|
|
|
|
|
|
|
|
|
|
Ez meg azért érvényes K-ban, mert nincsenek ilyen alakú tételei:
modalitásredukciók:
Ezek lennének a lehetségesek
Ezek vannak T-ben:
A hiányzók egyelőre nem tudjuk hol érvényesek:
K-ban viszont igazak a következő következtetések:
T-ben pedig még ez is:
Ja meg még ez a három is:
K4-ben meg igaz: