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ó
|
|
|
|
|
|
![{\displaystyle \scriptstyle {PA\vdash \forall x\forall y(x+y)=(y+x)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/50203e72098dab968b65f8523a70c0a86acbfee8)
![{\displaystyle \scriptstyle {PA\vdash \forall x\forall y\forall z((x+y)+z)=(x+(y+z))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/08beb31701737d1c329afb4e8472fdf9a95ed2a5)
![{\displaystyle \scriptstyle {PA\vdash \forall x\forall y\forall z(x\cdot (y+z))=((x\cdot y)+(x\cdot z))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c5b07f59147b3d54e5f6d42035f4645ac4d80efb)
![{\displaystyle \scriptstyle {PA\vdash \forall x\forall y\forall z((x\cdot y)\cdot z)=(x\cdot (y\cdot z))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/91b4168d8d2eba1709dc7b54ef6899dba8f391cd)
![{\displaystyle \scriptstyle {PA\vdash \forall x\forall y(x\cdot y)=(y\cdot x)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ae617ecb81ea174196f4e21cffdac55039ea53d0)
![{\displaystyle \scriptstyle {PA\vdash \forall x\forall y(x+y)=(y+x)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/50203e72098dab968b65f8523a70c0a86acbfee8)
- 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 ![{\displaystyle \scriptstyle {PA\vdash t=t'}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0ab16192bf59224cdac6d5ee8bdd70a88ff12838)
![{\displaystyle \scriptstyle {x\leq y\iff _{def}\exists z(x+z=y)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cf9de4db346fa5e9c5c26d23bbf8ef5f89cd6618)
![{\displaystyle \scriptstyle {x<y\iff _{def}x\leq y\land x\neq y}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cd8b6d229a0040f1d0926a3949fa4f016112c137)
![{\displaystyle \scriptstyle {x>y\iff _{def}\lnot x\leq y}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ac762c4c2dc52d3eb3b4f56124bf76e2567226a4)
![{\displaystyle \scriptstyle {x\geq y\iff _{def}\lnot x<y}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e1282af156ad6bb730305d6da9db4fb48591421f)
![{\displaystyle \scriptstyle {PA\vdash \forall x\lnot x<0}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/534ae649632344cfe2e346266407465f14ea4165)
j < i ![{\displaystyle \scriptstyle {\}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/99aabfae007d685858b8872644e11b7d444aa4b7)
![{\displaystyle \scriptstyle {PA\vdash (\forall x(\forall y(y<x\rightarrow F(y))\rightarrow F(x))\rightarrow F(x))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1dc83cabcc37112d2f97ff8ef55a0f247bb066b5)
![{\displaystyle \scriptstyle {PA\vdash (F(x)\rightarrow \exists x(F(x)\land \forall y(y<x\rightarrow \lnot F(y))))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/681a0b334cf30e4ff593c6ca4784e159dd2c3f8b)
![{\displaystyle \scriptstyle {PA\vdash \lnot x<x}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9f208cff35a286a2ffc92a0983aea134895a6f35)
![{\displaystyle \scriptstyle {PA\vdash ((x<y\land y<z)\rightarrow x<z)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/86f7e7762152aec8c23781b32db196e2dbe3abff)
![{\displaystyle \scriptstyle {PA\vdash ((x<y\vee x=y)\vee x>y)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7d2e0c403ccc8291c5f5633ed8393025467dd6ed)
![{\displaystyle \scriptstyle {PA\vdash (x<y\rightarrow (x+z)<(y+z))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/83fee663313a0b8805b16fa20a62a5be4114c8b6)
![{\displaystyle \scriptstyle {PA\vdash ((x<y\land 0<z)\rightarrow (x\cdot z)<(y\cdot z))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e04742ec9fb611699b3fb30b67b560d65f519177)
formulák osztálya
|
Bázis
|
|
Rekurzió
|
|
*Ha i kisebb, mint j, akkor
- Ha i más, mint j, akkor
![{\displaystyle \scriptstyle {PA\vdash i\neq j}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/438afc6c8678298b99c46e3e1f24b5ead6706eac)
- Ha i nem kisebb, mint j, akkor
![{\displaystyle \scriptstyle {PA\vdash \lnot i<j}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/da80b4260d036c209b7701e6ba40437e92e8367a)
- Egy
formula pszeudoterminus, ha
. A pszeudoterminusokat így szokás jelölni:
. Minden pszeudoterminus egy n-argumentumú függvényt definiál.
![{\displaystyle \scriptstyle {A(f(x_{1},x_{2},\dots x_{n}))\iff _{def}\exists y(F(x_{1},x_{2},\dots x_{n},y)\land A(y))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/96a87b431e925d813d9d942b2a2cdf6cb0f98c57)
Ha
igaz, akkor
![{\displaystyle \scriptstyle {F\in \Pi _{1}\iff _{def}\lnot F\in \Sigma _{1}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1a8d234977873f9edae6894551f8d6545cd4bc9a)
![{\displaystyle \scriptstyle {\Delta =\Sigma _{1}\cap \Pi _{1}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/77924074852cddbded8721ad1d38fa1e0a3523ed)
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.
![{\displaystyle \scriptstyle {d|x\iff _{def}\exists q(q\cdot d)=x}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0378c89f2687c6c91c5d277b49a34448bcc31356)
![{\displaystyle \scriptstyle {PA\vdash (\exists q(q\cdot d)=x\rightarrow \exists q(q\leq x\land (q\cdot d)=x))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/be0bc74baeef0437657660af5b605c264c845228)
![{\displaystyle \scriptstyle {PA\vdash d|d}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/daa8905c0e109e976dd0448e8b9153fd0764811a)
![{\displaystyle \scriptstyle {PA\vdash ((d|x\land x|y)\rightarrow d|y)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6393b82e7ec4bee69613ff78fbdd133d67d2336a)
![{\displaystyle \scriptstyle {PA\vdash (d|x\rightarrow (d|(x+y)\leftrightarrow d|y))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d62e3d1eac8b5d32c8aabc46c82cee790c0044c7)
![{\displaystyle \scriptstyle {PA\vdash (d\neq 0\rightarrow \exists q\exists r(((x=q\cdot d+r\land r<d)\land \forall q'\forall r'((x=(q'\cdot d)+r'\land r<d)\rightarrow (q=q'\land r=r')))))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a2b76386f64b16a232c369886845f326a5bfcc53)
![{\displaystyle \scriptstyle {Rm(x,d,r)\iff _{def}((r<d\land \exists qx=(q\cdot d)+r)\vee (d=0\land r=x))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/95158a03bb26a0bee0285d64d873955f508137af)
és pszeudoterminus
![{\displaystyle \scriptstyle {PA\vdash rm(x,0}=x}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f2df2a948ea02d23d2c0b307d019a90b647f7d85)
![{\displaystyle \scriptstyle {PA\vdash (d|x\leftrightarrow rm(x,d)=0)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6918edebd51656d7721a557b3ff7da9cea61226c)
![{\displaystyle \scriptstyle {PA\vdash rm(x+yd,d)=rm(x,d)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a2482451af0f46041ae9b7a8458754b770134417)
![{\displaystyle \scriptstyle {PA\vdash y\leq x\rightarrow \exists !zx=y+z}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a88196aa757713b158f59b82346f8b7f953d8587)
![{\displaystyle \scriptstyle {Monus(x,y,z\iff _{def}(x=y+z\vee (x<y\land z=0))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e87ee70f26af8e8fbdb97c7a2d559edddcce0149)
![{\displaystyle \scriptstyle {x-y=z\iff _{def}monus(x,y)=z}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6cfcd83daa0acfedc76c805ae5cb8dbdc659133e)
![{\displaystyle \scriptstyle {Irreducible(p)\iff _{def}(p\neq 1\land \forall d(d|p\rightarrow (d=1\vee d=p)))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc6f24f346b7a2192fec5a98a6308604b9bdc969)
![{\displaystyle \scriptstyle {Prime(p)\iff _{def}(p\neq 1\rightarrow \forall x\forall y(p|xy\rightarrow (p|x\vee p|y)))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ea9e7aeca4c4f9cc31e503182a52e7bf8c32def)
![{\displaystyle \scriptstyle {PA\vdash (Irreducible(2)\land \forall x(Irreducible(x)\rightarrow x\geq 2))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3f83aca14bfeb9c771f657e47a525cc54c222fa9)
![{\displaystyle \scriptstyle {PA\vdash \forall x(x>1\rightarrow \exists p(Irreducible(p)\land p|x))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/142ecd9f2ff933ff350c14fe889077187acc141c)
![{\displaystyle \scriptstyle {RelativelyPrime(a,b)\iff _{def}\forall d((d|a\land d|b)\rightarrow d=1)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d5829ad23d8866a086ecf736d0f3228ddefd08a9)
![{\displaystyle \scriptstyle {PA\vdash RelativelyPrime(a,b)\leftrightarrow \lnot \exists x(Irreducible(x)\land (x|a\land x|b))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/91268047182e509b3ffe82572c3bcc02aa924ebd)
![{\displaystyle \scriptstyle {PA\vdash \forall a\forall b(((a>1\land b>1)\land RelativelyPrime(a,b))\rightarrow \exists x\exists yax+1=by)}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ce6423acb0ac66d9c9d933a09bda2b96b64edcb0)
![{\displaystyle \scriptstyle {PA\vdash \forall x(Irreducible(x)\rightarrow Prime(x))}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1e076b65e24452c752c2a0e806617cb263656c61)
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: