„Peano-aritmetika” változatai közötti eltérés
| [ellenőrzött változat] | [ellenőrzött változat] |
Tartalom törölve Tartalom hozzáadva
→Műveleti tulajdonságok: egy példa |
|||
69. sor:
Fontos tétel továbbá a két műveletet összekötő egyik irányú [[Disztributivitás | disztributivitás]]: A <math>\scriptstyle{\cdot}</math> disztributív az <math>\scriptstyle{+}</math>-ra nézve.
<div align="center" style="clear:both;" class="NavFrame">
<div align="center" class="NavHead">Példa levezetésre: ''Kommutativitás'' - <small> ''A részletezés jobbra nyitható!''</small></div>
<div align="center" class="NavContent">
<math>
\begin{array}{rcll}
\scriptstyle PA\cup \{(0+x)=x\} & \scriptstyle \vdash & \scriptstyle (0+x)=x
& \scriptstyle \mathrm{premissza} \\
\scriptstyle PA\cup \{(0+x)=x\} & \scriptstyle \vdash & \scriptstyle s(0+x)=sx
& \scriptstyle \mathrm{taut.}\\
\scriptstyle PA\cup \{(0+x)=x\} & \scriptstyle \vdash & \scriptstyle s(0+x)=(0+sx)
& \scriptstyle \mathrm{3. ax.} \\
\scriptstyle PA\cup \{(0+x)=x\} & \scriptstyle \vdash & \scriptstyle (0+sx)=sx
& \scriptstyle \mathrm{=} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle (0+x)=x\rightarrow (0+sx)=sx
& \scriptstyle \mathrm{Ded.} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \forall x ((0+x)=x\rightarrow 0+sx=sx)
& \scriptstyle \mathrm{Univ. gen.}\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle F_x[0] \rightarrow \forall x( F \rightarrow F_x[sx]) \rightarrow F
& \scriptstyle \mathrm{7. ax.} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle ((0+x)=x)_x[0]\forall x ((0+x)=x ((0+x)=x)_x[sx])((0+x)=x)
& \scriptstyle F:=(0+x)=x \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle (0+0)=0\rightarrow
\forall x ((0+x)=x \rightarrow (0+sx)=sx )\rightarrow (0+x)=x
& \scriptstyle \mathrm{terminuscsere} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle (0+0)=0
& \scriptstyle \mathrm{3. ax.} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \forall x ( (0+x)=x\rightarrow (0+sx)=sx)\rightarrow (0+x)=x
& \scriptstyle \mathrm{modus ponens}\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle
(0+x)=x
& \scriptstyle \mathrm{modus ponens}\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle (x+0)=x
& \scriptstyle \mathrm{3.ax.}\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle (0+x)=(x+0)
& \scriptstyle \mathrm{=} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \forall x (0+x)=(x+0)
& \scriptstyle \mathrm{Univ. gen.}\\
\scriptstyle PA \cup \{ (x+y)=(y+x) \}& \scriptstyle\vdash & \scriptstyle (x+y)=(y+x)
& \scriptstyle \mathrm{prem.} \\
\scriptstyle PA \cup \{ (x+y)=(y+x) \}& \scriptstyle\vdash & \scriptstyle s(x+y)=s(y+x)
& \scriptstyle \mathrm{taut.} \\
\scriptstyle PA \cup \{ (x+y)=(y+x) \}& \scriptstyle\vdash & \scriptstyle s(x+y)=(x+sy)
& \scriptstyle \mathrm{4. ax.}\\
\scriptstyle PA\cup \{ (x+y)=(y+x) \}& \scriptstyle\vdash & \scriptstyle s(y+x)=(y+sx)
& \scriptstyle \mathrm{4. ax.}\\
\scriptstyle PA\cup \{ (x+y)=(y+x) \}& \scriptstyle\vdash & \scriptstyle
(x+sy)=(sy+x)
& \scriptstyle \mathrm{=} \\
\scriptstyle PA & \scriptstyle\vdash & \scriptstyle (x+y)=(y+x) \rightarrow (x+sy)=(sy+x)
& \scriptstyle \mathrm{Ded.} \\
\scriptstyle PA & \scriptstyle\vdash & \scriptstyle \forall x (x+y)=(y+x) \rightarrow (x+sy)=(sy+x)
& \scriptstyle \mathrm{Univ. gen.} \\
\scriptstyle PA & \scriptstyle\vdash & \scriptstyle \forall x (x+y)=(y+x) \rightarrow \forall x ((x+ sy= (sy+x))
& \scriptstyle \mathrm{2. ax.} \\
\scriptstyle PA & \scriptstyle\vdash & \scriptstyle \forall y \forall x((x+y)=(y+x)\rightarrow \forall x (x+sy)=(sy+x)
& \scriptstyle \mathrm{Univ. gen.} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle F_x[0] \rightarrow \forall x( F \rightarrow F_x[ sx] \rightarrow F
& \scriptstyle \mathrm{7. ax.} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle (\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)
& \scriptstyle F :=\forall x (x+y)=(y+x)\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \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)
& \scriptstyle \mathrm{terminuscsere} \\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \forall y \forall x (x+y)=(y+x)
\rightarrow \forall x (x+sy)=(sy+x) \rightarrow
\forall x (x+y)=(y+x)
& \scriptstyle \mathrm{modus ponens}\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \forall x (x+y)=(y+x)
& \scriptstyle \mathrm{modus ponens}\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \forall y \forall x (x+y)=(y+x)
& \scriptstyle \mathrm{Univ. gen.}\\
\scriptstyle PA & \scriptstyle \vdash & \scriptstyle \forall x \forall y (x+y)=(y+x)
& \scriptstyle \mathrm{kvantorcsere} \\
\end{array} </math>
</div>
</div>
=== Rendezés ===
| |||