[Teoria mnogości][Logika matematyczna][Podstawy matematyki] Dowód twierdzenia Russell'a jako przykład dowodu formalnego

Projekty i prace naukowe i badawcze. Nowatorskie idee matematyczne. Literatura specjalistyczna.
foundofmath
Użytkownik
Użytkownik
Posty: 78
Rejestracja: 3 sty 2017, o 19:54
Płeć: Mężczyzna
Podziękował: 33 razy
Pomógł: 4 razy

[Teoria mnogości][Logika matematyczna][Podstawy matematyki] Dowód twierdzenia Russell'a jako przykład dowodu formalnego

Post autor: foundofmath »

Aksjomaty logiczne - właściwe podstawienia tautologij rachunku predykatów oraz aksjomaty charakteryzujące równość:

\(\displaystyle{ Ax_1 \ p\Rightarrow(q\Rightarrow p) \\
Ax_2 \ (p\Rightarrow(q\Rightarrow r))\Rightarrow((p\Rightarrow q)\Rightarrow (p\Rightarrow r)) \\
Ax_3 \ (p\wedge q)\Rightarrow p \\
Ax_4 \ (p\wedge q)\Rightarrow q \\
Ax_5 \ (p\Rightarrow q)\Rightarrow((p\Rightarrow r)\Rightarrow(p\Rightarrow(q\wedge r))) \\
Ax_6 \ p \Rightarrow (p \vee q) \\
Ax_7 \ q\Rightarrow(p \vee q) \\
Ax_8 \ (q \Rightarrow p)\Rightarrow( (r \Rightarrow p)\Rightarrow((q \vee r)\Rightarrow p) ) \\
Ax_9 \ (p \Leftrightarrow q)\Rightarrow (p\Rightarrow q) \\
Ax_{10} \ (p \Leftrightarrow q)\Rightarrow (q \Rightarrow p) \\
Ax_{11} \ (p\Rightarrow q)\Rightarrow((q \Rightarrow p)\Rightarrow(p \Leftrightarrow q)) \\
Ax_{12} \ p\Rightarrow((\neg p)\Rightarrow q) \\
Ax_{13} \ (p\Rightarrow (\neg p))\Rightarrow (\neg p) \\
Ax_{14} \ (\neg(\neg p)) \Rightarrow p \\}\)


\(\displaystyle{ AK1 \ \phi(x)\Rightarrow (\exists x \ (\phi(x))) \\
AK2 \ (\forall x (\phi(x))) \Rightarrow \phi(x) \\}\)


\(\displaystyle{ E1 \ x=x \\ E2 \ x=y\Rightarrow y=x \\ E3 \ x=y \Rightarrow(y=z \Rightarrow x=z) }\)
\(\displaystyle{ B1 \ x=y\Rightarrow(z=w\Rightarrow(x \in z \Rightarrow y \in w))}\)

Właściwe aksjomaty teoriomnogościowe (odpowiednio regularności i pary):

\(\displaystyle{ ATM1 = \forall x ((\exists z \ (z \in x))\Rightarrow (\exists w(w\in x \wedge (\neg(\exists z (z \in x \wedge z \in w) )) )) ) \\
ATM2= \forall x(\forall y(\exists a(\forall w(w \in a \Leftrightarrow (w=x \vee w =y) ) ) ) ) \\}\)


Reguły dowodzenia:

\(\displaystyle{
R1\ \frac{\Psi \Rightarrow \alpha(x)}{\Psi \Rightarrow (\forall x \ (\alpha(x)))},x \ \mbox{nie ma wolnych wystąpień w } \Psi \\
R2\ \frac{\alpha(x) \Rightarrow \Psi }{(\exists x(\alpha(x)) )\Rightarrow \Psi}, x \ \mbox{nie ma wolnych wystąpień w } \Psi\\}\)

\(\displaystyle{ MP \ \frac{\alpha,\alpha \Rightarrow \beta}{\beta} \ \mbox{(reguła odrywania)} \\
RP \ \frac{\alpha(x)}{\alpha(a)}, \mbox{podstawienie jest właściwe} \ \mbox{(reguła podstawiania)}}\)




Twierdzenie: \(\displaystyle{ \forall x(\forall y(\neg(x \in y \wedge y \in x)) )}\)



Zostanie pokazane, że: \(\displaystyle{ \mbox{powyższe aksjomaty} \vdash \forall x(\forall y(\neg(x \in y \wedge y \in x)) )}\)



Dowód podzielony na trzy części zamieszczone kolejno z uwagi na problemy z całościowym załadowaniem treści (warto chwilę odczekać aż załaduje zawartość):

Ukryta treść:    
Ukryta treść:    
Ukryta treść:    
Dodano po 17 godzinach 31 minutach 18 sekundach:
\(\displaystyle{ AK1 \vdash f(296)=(x \in a \wedge x \in w)\Rightarrow(\exists z (z \in a \wedge z \in w) )}\)
- to oczywiście nieprawda (tzn. jest to twierdzenie, ale nie podpada pod \(\displaystyle{ AK1}\)). Powinno być na przykład:

\(\displaystyle{ AK1 \vdash f(296)=(z \in a \wedge z \in w)\Rightarrow(\exists z (z \in a \wedge z \in w) )}\)

\(\displaystyle{ RP,f(296)\vdash f(297)=(x \in a \wedge x \in w)\Rightarrow(\exists z (z \in a \wedge z \in w) )}\)

W takim wypadku należy w pierwotnej wersji zastąpić
\(\displaystyle{ AK1 \vdash f(296)=(x \in a \wedge x \in w)\Rightarrow(\exists z (z \in a \wedge z \in w) )}\)
przez \(\displaystyle{ AK1 \vdash f(296)=(z \in a \wedge z \in w)\Rightarrow(\exists z (z \in a \wedge z \in w) )}\) i bezpośrednio pod tym zastąpieniem umieścić \(\displaystyle{ RP,f(296)\vdash f(297)=(x \in a \wedge x \in w)\Rightarrow(\exists z (z \in a \wedge z \in w) )}\), a poniższe \(\displaystyle{ f(x)}\) zastąpić przez \(\displaystyle{ f(x+1)}\) dla \(\displaystyle{ x \ge 296}\) (dostosowanie numeracji do wprowadzonej zmiany)
ODPOWIEDZ