Szerkesztő:Thuluviel/firka

Firkák

Peano-aritmetika

A kommutativitás bizonyítása - A részletezés jobbra nyitható!

<math>
\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}
</math>

Peano-aritmetikai fogalmak és egyebek.

$\scriptstyle {\Sigma _{1}}$ formulák osztálya
Bázis	$\scriptstyle {0=su\in \Sigma _{1}}$
	$\scriptstyle {su=v\in \Sigma _{1}}$
	$\scriptstyle {u+v=w\in \Sigma _{1}}$
	$\scriptstyle {u\cdot v=w\in \Sigma _{1}}$
Rekurzió	$\scriptstyle {F,G\in \Sigma _{1}\Rightarrow (F\land G)\in \Sigma _{1}}$
	$\scriptstyle {F,G\in \Sigma _{1}\Rightarrow (F\vee G)\in \Sigma _{1}}$
	$\scriptstyle {F\in \Sigma _{1}\Rightarrow \exists xF\in \Sigma _{1}}$
	$\scriptstyle {F\in \Sigma _{1}\Rightarrow (\forall x<y)F\in \Sigma _{1}}$
	$\scriptstyle {F,G\in \Sigma _{1}\Rightarrow (F\land G)\in \Sigma _{1}}$

• $\scriptstyle {PA\vdash \forall x\forall y(x+y)=(y+x)}$
• $\scriptstyle {PA\vdash \forall x\forall y\forall z((x+y)+z)=(x+(y+z))}$
• $\scriptstyle {PA\vdash \forall x\forall y\forall z(x\cdot (y+z))=((x\cdot y)+(x\cdot z))}$
• $\scriptstyle {PA\vdash \forall x\forall y\forall z((x\cdot y)\cdot z)=(x\cdot (y\cdot z))}$
• $\scriptstyle {PA\vdash \forall x\forall y(x\cdot y)=(y\cdot x)}$
• $\scriptstyle {PA\vdash \forall x\forall y(x+y)=(y+x)}$
• Ha i meg j egyenlő k-val, akkor $\scriptstyle {PA\vdash (i+j)=k}$ , ahol $\scriptstyle {i}$-ben i darab $\scriptstyle {s}$ jel van, stb.
• Ha i-szer j egyenlő k-val, akkor $\scriptstyle {PA\vdash (i\cdot j)=k}$ , ahol $\scriptstyle {i}$-ben i darab $\scriptstyle {s}$ jel van, stb.
• Ha $\scriptstyle {t}$ egy változót nem tartalmazó terminus és i-t jelöli, akkor

$\scriptstyle {PA\vdash t=i}$

• Ha $\scriptstyle {t}$ és $\scriptstyle {t'}$ változót nem tartalmazó terminusok és ugyanazt jelölik, akkor $\scriptstyle {PA\vdash t=t'}$
• $\scriptstyle {x\leq y\iff _{def}\exists z(x+z=y)}$
• $\scriptstyle {x<y\iff _{def}x\leq y\land x\neq y}$
• $\scriptstyle {x>y\iff _{def}\lnot x\leq y}$
• $\scriptstyle {x\geq y\iff _{def}\lnot x<y}$
• $\scriptstyle {PA\vdash \forall x\lnot x<0}$
• $\scriptstyle {\bigvee \{x=j:}$j < i $\scriptstyle {\}}$
• $\scriptstyle {PA\vdash (\forall x(\forall y(y<x\rightarrow F(y))\rightarrow F(x))\rightarrow F(x))}$
• $\scriptstyle {PA\vdash (F(x)\rightarrow \exists x(F(x)\land \forall y(y<x\rightarrow \lnot F(y))))}$
• $\scriptstyle {PA\vdash \lnot x<x}$
• $\scriptstyle {PA\vdash ((x<y\land y<z)\rightarrow x<z)}$
• $\scriptstyle {PA\vdash ((x<y\vee x=y)\vee x>y)}$
• $\scriptstyle {PA\vdash (x<y\rightarrow (x+z)<(y+z))}$
• $\scriptstyle {PA\vdash ((x<y\land 0<z)\rightarrow (x\cdot z)<(y\cdot z))}$

$\scriptstyle {\Sigma _{1}}$ formulák osztálya
Bázis	$\scriptstyle {\begin{array}{r}\scriptstyle {0=su\in \Sigma _{1}}\\\scriptstyle {su=v\in \Sigma _{1}}\\\scriptstyle {u+v=w\in \Sigma _{1}}\\\scriptstyle {u\cdot v=w\in \Sigma _{1}}\end{array}}$
Rekurzió	$\scriptstyle {\begin{array}{rcr}\scriptstyle {F,G\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {(F\land G)\in \Sigma _{1}}\\\scriptstyle {F,G\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {(F\vee G)\in \Sigma _{1}}\\\scriptstyle {F\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {\exists xF\in \Sigma _{1}}\\\scriptstyle {F\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {(\forall x<y)F\in \Sigma _{1}}\end{array}}$

*Ha i kisebb, mint j, akkor $\scriptstyle {PA\vdash i<j}$

• Ha i más, mint j, akkor $\scriptstyle {PA\vdash i\neq j}$
• Ha i nem kisebb, mint j, akkor $\scriptstyle {PA\vdash \lnot i<j}$
• Egy $\scriptstyle {F(x_{1},x_{2},\dots x_{n},y)}$ formula pszeudoterminus, ha

$\scriptstyle {PA\vdash \exists !yF(x_{1},x_{2},\dots x_{n},y)}$. A pszeudoterminusokat így szokás jelölni: $\scriptstyle {f(x_{1},x_{2},\dots x_{n})}$. Minden pszeudoterminus egy n-argumentumú függvényt definiál.

$\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))}$

Ha $\scriptstyle {F\in \Sigma _{1}}$ igaz, akkor $\scriptstyle {PA\vdash F}$

• $\scriptstyle {F\in \Pi _{1}\iff _{def}\lnot F\in \Sigma _{1}}$
• $\scriptstyle {\Delta =\Sigma _{1}\cap \Pi _{1}}$
• $\scriptstyle {\Delta }$ tartalmazza az összes atomi formulát és a $\scriptstyle {t<t'}$, $\scriptstyle {u|v}$, $\scriptstyle {Irreducible(p)}$,$\scriptstyle {RelativelyPrime(a,b)}$ alakú formulákat, zárt a Boole-műveletekre, a korlátos kvantifikációkra és a pszeudoterminusok bármely helyettesítésére.
• $\scriptstyle {d|x\iff _{def}\exists q(q\cdot d)=x}$
• $\scriptstyle {PA\vdash (\exists q(q\cdot d)=x\rightarrow \exists q(q\leq x\land (q\cdot d)=x))}$
• $\scriptstyle {PA\vdash d|d}$
• $\scriptstyle {PA\vdash ((d|x\land x|y)\rightarrow d|y)}$
• $\scriptstyle {PA\vdash (d|x\rightarrow (d|(x+y)\leftrightarrow d|y))}$
• $\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')))))}$
• $\scriptstyle {Rm(x,d,r)\iff _{def}((r<d\land \exists qx=(q\cdot d)+r)\vee (d=0\land r=x))}$
• $\scriptstyle {Rm(x,d,r)\in \Sigma }$ és pszeudoterminus
• $\scriptstyle {PA\vdash rm(x,0}=x$
• $\scriptstyle {PA\vdash (d|x\leftrightarrow rm(x,d)=0)}$
• $\scriptstyle {PA\vdash rm(x+yd,d)=rm(x,d)}$
• $\scriptstyle {PA\vdash y\leq x\rightarrow \exists !zx=y+z}$
• $\scriptstyle {Monus(x,y,z\iff _{def}(x=y+z\vee (x<y\land z=0))}$
• $\scriptstyle {x-y=z\iff _{def}monus(x,y)=z}$
• $\scriptstyle {Irreducible(p)\iff _{def}(p\neq 1\land \forall d(d|p\rightarrow (d=1\vee d=p)))}$
• $\scriptstyle {Prime(p)\iff _{def}(p\neq 1\rightarrow \forall x\forall y(p|xy\rightarrow (p|x\vee p|y)))}$
• $\scriptstyle {PA\vdash (Irreducible(2)\land \forall x(Irreducible(x)\rightarrow x\geq 2))}$
• $\scriptstyle {PA\vdash \forall x(x>1\rightarrow \exists p(Irreducible(p)\land p|x))}$
• $\scriptstyle {RelativelyPrime(a,b)\iff _{def}\forall d((d|a\land d|b)\rightarrow d=1)}$
• $\scriptstyle {PA\vdash RelativelyPrime(a,b)\leftrightarrow \lnot \exists x(Irreducible(x)\land (x|a\land x|b))}$
• $\scriptstyle {PA\vdash \forall a\forall b(((a>1\land b>1)\land RelativelyPrime(a,b))\rightarrow \exists x\exists yax+1=by)}$
• $\scriptstyle {PA\vdash \forall x(Irreducible(x)\rightarrow Prime(x))}$

Modális logika

tételek S5-ből
$\scriptstyle {\Box (A\vee \Box B)\rightarrow (\Box A\vee \Box B)}$
$\scriptstyle {\Box (A\vee \Diamond B)\rightarrow (\Box A\vee \Diamond B)}$
$\scriptstyle {\Diamond (A\land \Diamond B)\leftrightarrow (\Diamond A\land \Diamond B)}$
$\scriptstyle {\Diamond (A\land \Box B)\leftrightarrow (\Diamond A\land \Box B)}$
$\scriptstyle {\Box (\Box A\rightarrow \Box B)\vee \Box (\Box B\rightarrow \Box A)}$

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:

${\begin{array}{l}\Box (A\supset B)\supset (\Box A\supset \Box B)\\\Box (p\land q)\equiv (\Box p\land \Box q)\\\Box p\vee \Box q)\supset \Box (p\vee q)\\\Diamond (p\vee q)\equiv (\Diamond p\vee \Diamond q)\\\Diamond (p\supset q)\equiv (\Box p\supset \Diamond q)\\\Diamond (p\land q)\supset (\Diamond p\land \Diamond q)\\(\Diamond p\land \Box q)\supset \Diamond (p\land q)\\\Box (p\vee q)\supset (\Box p\vee \Diamond q)\end{array}}$

Azaz: haakkor: ${\begin{array}{l}\Box (A\supset B)\supset (\Box A\supset \Box B)\\\Diamond (p\supset q)\equiv (\Box p\supset \Diamond q)\\\Diamond (p\supset q)\supset (\Diamond p\supset \Diamond q)\end{array}}$

és: ${\begin{array}{l}\\\Box (p\land q)\equiv (\Box p\land \Box q)\\\Diamond (p\land q)\supset (\Diamond p\land \Diamond q)\\(\Diamond p\land \Box q)\supset \Diamond (p\land q)\end{array}}$
vagy: ${\begin{array}{l}\\\Box p\vee \Box q)\supset \Box (p\vee q)\\\Diamond (p\vee q)\equiv (\Diamond p\vee \Diamond q)\\\Box (p\vee q)\supset (\Box p\vee \Diamond q)\end{array}}$

érvényes formulák K-ból
$\scriptstyle {\land }$	$\scriptstyle {\Box (A\land B)\leftrightarrow (\Box A\land \Box B)}$
	$\scriptstyle {\Diamond (A\land B)\rightarrow (\Diamond A\land \Diamond B)}$
	$\scriptstyle {(\Box A\land \Diamond B)\rightarrow \Diamond (A\land B)}$
$\scriptstyle {\lor }$	$\scriptstyle {\Box A\vee \Box B)\rightarrow \Box (A\vee B)}$
	$\scriptstyle {\Diamond (A\vee B)\leftrightarrow (\Diamond A\vee \Diamond B)}$
	$\scriptstyle {\Box (A\vee B)\rightarrow (\Box A\vee \Diamond B)}$
$\scriptstyle {\rightarrow }$	$\scriptstyle {\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}$
	$\scriptstyle {\Diamond (A\rightarrow B)\leftrightarrow (\Box A\rightarrow \Diamond B)}$
	$\scriptstyle {\Diamond (A\rightarrow B)\rightarrow (\Diamond A\rightarrow \Diamond B)}$

${\frac {A\supset B}{\Box A\supset \Box B}}\qquad {\frac {A\equiv B}{\Box A\equiv \Box B}}\qquad {\frac {A\supset B}{\Diamond A\supset \Diamond B}}$ Ez meg azért érvényes K-ban, mert nincsenek ilyen alakú tételei: ${\frac {\Diamond A}{A}}\qquad {\frac {\Box \Diamond A}{A}}$

modalitásredukciók: Ezek lennének a lehetségesek ${\begin{array}{l}\\\Diamond p\equiv \Box \Diamond p\\\Box p\equiv \Diamond \Box p\\\Diamond p\equiv \Diamond \Diamond p\\\Box p\equiv \Box \Box p\end{array}}$

Ezek vannak T-ben: ${\begin{array}{l}\Box \Diamond p\supset \Diamond p\\\Box p\supset \Diamond \Box p\\\Diamond p\supset \Diamond \Diamond p\\\Box \Box p\supset \Box p\end{array}}$

A hiányzók egyelőre nem tudjuk hol érvényesek: ${\begin{array}{l}\Diamond p\supset \Box \Diamond p\\\Diamond \Box p\supset \Box p\\\Diamond \Diamond p\supset \Diamond p\\\Box p\supset \Box \Box p\end{array}}$

K-ban viszont igazak a következő következtetések:

${\begin{array}{l}\Diamond \Diamond p\supset \Diamond p\\\hline \hline \Box p\supset \Box \Box p\end{array}}$

${\begin{array}{l}\Diamond p\supset \Box \Diamond p\\\hline \hline \Diamond \Box p\supset \Box p\end{array}}$

T-ben pedig még ez is: ${\frac {\Diamond p\supset \Box \Diamond p}{\Box p\supset \Box \Box p}}$

Ja meg még ez a három is:

${\begin{array}{l}\Box A\supset A\\A\supset \Diamond A\\\Box A\supset \Diamond A\end{array}}$

K4-ben meg igaz: $\Box \Diamond \Box \Diamond A\equiv \Box \Diamond A$