Logiczny zapis matematyki: Różnice pomiędzy wersjami
Przejdź do nawigacji
Przejdź do wyszukiwania
BartekChom (dyskusja | edycje) (liczby, funkcje, pary) |
BartekChom (dyskusja | edycje) (grupy, paradoks) |
||
| Linia 1: | Linia 1: | ||
| − | + | Częścią [[logiczny język|logicznego języka]] jest zapis matematyczny. W jednej z wersji: | |
Używa się 84 znaków (dostępnych bezpośrednio z klawiatury): | Używa się 84 znaków (dostępnych bezpośrednio z klawiatury): | ||
| Linia 528: | Linia 528: | ||
Poprawa definiowania podzbiorów | Poprawa definiowania podzbiorów | ||
( \A_ zbior ( \l x ( \A_ ( \l y ( formula ( \l z ( lub ( \w x z ) ( y z ) ) ) ) ) ( \l y ( = ( {f y x ) ( {f ( \l z ( & ( \w x z ) ( y z ) ) ) x ) ) ) ) ) ) | ( \A_ zbior ( \l x ( \A_ ( \l y ( formula ( \l z ( lub ( \w x z ) ( y z ) ) ) ) ) ( \l y ( = ( {f y x ) ( {f ( \l z ( & ( \w x z ) ( y z ) ) ) x ) ) ) ) ) ) | ||
| + | ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( zbior ( {ff x ) ) ) ) ) | ||
| + | ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( \A ( \l z ( = ( \w ( {ff x ) z ) ( x z ) ) ) ) ) ) ) | ||
Od razu przedziały liczb naturalnych: | Od razu przedziały liczb naturalnych: | ||
| − | ( \A_ naturalna ( \l x ( \A_ naturalna ( \l y | + | ( \A_ naturalna ( \l x ( \A_ naturalna ( \l y ( = ( [N x y ) ( {f ( \l z ( & ( >= x z ) ( >= z y ) ) ) \N ) ) ) ) ) ) |
( = \N+ ( {f ( > . ) \N ) ) | ( = \N+ ( {f ( > . ) \N ) ) | ||
| Linia 545: | Linia 547: | ||
( formula wBudowie_{n ) | ( formula wBudowie_{n ) | ||
( \A_ ( \w \N+ ) ( \l x ( & ( & ( wBudowie_{n ( {n x ) ) ( = {} ( juz ( {n x ) ) ) ) ( = x ( ile ( {n x ) ) ) ) ) ) | ( \A_ ( \w \N+ ) ( \l x ( & ( & ( wBudowie_{n ( {n x ) ) ( = {} ( juz ( {n x ) ) ) ) ( = x ( ile ( {n x ) ) ) ) ) ) | ||
| − | ( \A_ wBudowie_{n ( \l x ( => ( > 1. ( ile x ) ) ( \A ( \l y ( = ( \u ( juz x ) ( { y ) ) ( juz ( x y ) ) ) ) ) ) ) ) | + | ( \A_ wBudowie_{n ( \l x ( => ( > 1. ( ile x ) ) ( \A ( \l y ( & ( = ( 'N ( ile ( x y ) ) ) ( ile x ) ) ( = ( \u ( juz x ) ( { y ) ) ( juz ( x y ) ) ) ) ) ) ) ) |
( \A_ wBudowie_{n ( \l x ( => ( = 1. ( ile x ) ) ( \A ( \l y ( = ( \u ( juz x ) ( { y ) ) ( x y ) ) ) ) ) ) ) | ( \A_ wBudowie_{n ( \l x ( => ( = 1. ( ile x ) ) ( \A ( \l y ( = ( \u ( juz x ) ( { y ) ) ( x y ) ) ) ) ) ) ) | ||
| Linia 582: | Linia 584: | ||
( formula wBudowie_(n ) | ( formula wBudowie_(n ) | ||
( \A_ ( \w \N+ ) ( \l x ( & ( & ( wBudowie_(n ( (n x ) ) ( n-ka . ( juz ( (n x ) ) ) ) ( = x ( ile ( (n x ) ) ) ) ) ) | ( \A_ ( \w \N+ ) ( \l x ( & ( & ( wBudowie_(n ( (n x ) ) ( n-ka . ( juz ( (n x ) ) ) ) ( = x ( ile ( (n x ) ) ) ) ) ) | ||
| − | ( \A_ wBudowie_(n ( \l x ( => ( > 1. ( ile x ) ) ( \A ( \l y ( = ( zloz ( juz x ) ( (1 y ) ) ( juz ( x y ) ) ) ) ) ) ) ) | + | ( \A_ wBudowie_(n ( \l x ( => ( > 1. ( ile x ) ) ( \A ( \l y ( & ( = ( 'N ( ile ( x y ) ) ) ( ile x ) ) ( = ( zloz ( juz x ) ( (1 y ) ) ( juz ( x y ) ) ) ) ) ) ) ) ) |
( \A_ wBudowie_(n ( \l x ( => ( = 1. ( ile x ) ) ( \A ( \l y ( = ( zloz ( juz x ) ( (1 y ) ) ( x y ) ) ) ) ) ) ) | ( \A_ wBudowie_(n ( \l x ( => ( = 1. ( ile x ) ) ( \A ( \l y ( = ( zloz ( juz x ) ( (1 y ) ) ( x y ) ) ) ) ) ) ) | ||
| Linia 591: | Linia 593: | ||
A następnie grupy, ciała, przestrzenie wektorowe i algebry. | A następnie grupy, ciała, przestrzenie wektorowe i algebry. | ||
| + | ( formula grupoid ) | ||
| + | ( \A_ grupoid ( \l x ( zbior ( {ff ( \w x ) ) ) ) ) | ||
| + | ( \A_ grupoid ( \l x ( \A_ grupoid ( \l y ( = ( = x y ) ( & ( = ( {ff ( \w x ) ) ( {ff ( \w y ) ) ) ( \A_ ( \w x ) ( \l z ( \A_ ( \w x ) ( \l t ( = ( oG x z t ) ( oG y z t ) ) ) ) ) ) ) ) ) ) ) ) | ||
| + | |||
| + | Według schematu ( laczny zbiór działanie ) | ||
| + | ( = laczny ( \l x ( \l y ( \A_ ( \w x ) ( \l a ( \A_ ( \w x ) ( \l b ( \A_ ( \w x ) ( \l c ( = ( y ( y c b ) a ) ( y c ( y b a ) ) ) ) ) ) ) ) ) ) | ||
| + | Według schematu ( e_neutralny zbiór działanie element ) | ||
| + | ( = e_neutralny ( \l x ( \l y ( \l z ( \A_ ( \w x ) ( \l a ( & ( = ( y z a ) a ) ( = ( y a z ) a ) ) ) ) ) ) ) ) | ||
| + | Według schematu ( e_przeciwny zbiór działanie element_a element_b ) | ||
| + | ( = e_przeciwny ( \l x ( \l y ( \l a ( \l b ( & ( e_neutralny x y ( y a b ) ) ( e_neutralny x y ( y b a ) ) ) ) ) ) ) ) | ||
| + | Według schematu ( przemienny zbiór działanie ) | ||
| + | ( = przemienny ( \l x ( \l y ( \A_ ( \w x ) ( \l z ( \A_ ( \w x ) ( \l t ( = ( y z t ) ( y t z ) ) ) ) ) ) ) ) ) | ||
| + | |||
| + | ( = polgrupa ( \l x ( & ( grupoid x ) ( laczny x ( oG x ) ) ) ) ) | ||
| + | ( = grupoid_z1 ( \l x ( & ( grupoid x ) ( \V_ ( \w x ) ( e_neutralny x ( oG x ) ) ) ) ) ) | ||
| + | ( = lupa ( \l x ( & ( grupoid_z1 x ) ( \A_ ( \w x ) ( \l a ( \V_ ( \w x ) ( e_przeciwny x ( oG x ) a ) ) ) ) ) ) ) | ||
| + | ( = grupa ( \l x ( & ( lupa x ) ( polgrupa x ) ) ) ) | ||
| + | ( = grupaPrzemienna ( \l x ( & ( grupa x ) ( przemienny ( oG x ) ) ) ) ) | ||
| + | |||
| + | Złóż grupę | ||
| + | ... ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( zbior ( {ff x ) ) ) ) ) | ||
| + | ... ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( \A ( \l z ( = ( \w ( {ff x ) z ) ( x z ) ) ) ) ) ) ) | ||
| + | |||
| + | ( formula pierscienioid ) | ||
| + | ( \A_ pierscienioid ( \l x ( zbior ( {ff ( \w x ) ) ) ) ) | ||
| + | ( \A_ pierscienioid ( \l x ( \A_ pierscienioid ( \l y | ||
| + | ( = ( = x y ) ( & ( = ( {ff ( \w x ) ) ( {ff ( \w y ) ) ) ( \A_ ( \w x ) ( \l z ( \A_ ( \w x ) ( \l t ( & ( = ( +P x z t ) ( +P y z t ) ) ( = ( *P x z t ) ( *P y z t ) ) ) ) ) ) ) ) ) | ||
| + | ) ) ) ) | ||
| + | |||
| + | Według schematu ( rozdzielny zbiór mnożenie dodawanie ) | ||
| + | ( = rozdzielny ( \l x ( \l y ( \l z | ||
| + | ( \A_ ( \w x ) ( \l a ( \A_ ( \w x ) ( \l b ( \A_ ( \w x ) ( \l c | ||
| + | ( & ( = ( z c ( y a b ) ) ( y ( z c a ) ( z c b ) ) ) ( = ( z ( y a b ) c ) ( y ( z a c ) ( z b c ) ) ) ) | ||
| + | ) ) ) ) ) ) | ||
| + | ) ) ) ) | ||
| + | |||
| + | ( = subpierscien ( \l x ( & ( pierscienioid x ) ( grupaPrzemienna ( zlozGrupe x ( +P x ) ) ) ) ) ) | ||
| + | ( = pierscien_sl ( \l x ( & ( subpierscien x ) ( rozdzielny x ( +Px ) ( *P x ) ) ) ) ) | ||
| + | ( = pierscien ( \l x ( & ( pierscien_sl x ) ( laczny x ( *P x ) ) ) ) ) | ||
| + | ... pierścień przemienny itd. | ||
Oraz liczby rzeczywiste i zespolone. | Oraz liczby rzeczywiste i zespolone. | ||
| + | |||
| + | == Paradoks == | ||
| + | <code>( \l x ( = nie ( x x ) ) )</code> zastosowany na siebie | ||
| + | ( \l x ( = ( = ani = ) ( x x ) ) ( \l x ( = ( = ani = ) ( x x ) ) ) ) | ||
[[Kategoria:Logiczny język]] | [[Kategoria:Logiczny język]] | ||
Wersja z 23:46, 25 paź 2009
Częścią logicznego języka jest zapis matematyczny. W jednej z wersji:
Używa się 84 znaków (dostępnych bezpośrednio z klawiatury):
a b c d e f g h i j k l m n o p q r s t u v w x y z
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
1 2 3 4 5 6 7 8 9 0
` ~ ! @ # $ % ^ & * ( ) - _ = + [ { ] } ; : ' " \ | , < . > / ?
Symbole dzieli się dowolnymi białymi znakami (spacja, znak tabulacji, enter).
Jest sześć pojęć pierwotnych, których nie precyzuje się nawet aksjomatami.
(,)- nawiasy używane jak w Lispie\l- operator lambda przyjmujący dwa argumenty (zmienną związaną i wyrażenie; tworzy raczej funkcjonały niż funkcje)\V- operator jednoargumentowy, przyjmuje funkcjonał i zwraca prawdę, jeśli coś może dać jedenani- operator logiczny dwuargumentowy=- operator dwuargumentowy
Ani zastępuje wszystkie funkcje logiczne (z innymi znakami można łatwiej):
| a\b | 0 | 1 |
| 0 | ||
| 1 |
00 0 00 ( ani a ( ani a a ) ) 00 a i b 01 ( ani ( ani a a ) ( ani b b ) ) 00 a i ~b 10 ( ani b ( ani a b ) ) 00 a 11 a 01 ~a i b 00 ( ani a ( ani a b ) ) 01 b 01 b 01 a albo b 10 ( ani ( ani a b ) ( ani ( ani a a ) ( ani b b ) ) 01 a lub b 11 ( ani ( ani a b ) ( ani a b ) ) 10 a ani b 00 ( ani a b ) 10 a <=> b 01 (ani ( ani a ( ani a b ) ) ( ani b ( ani a b ) ) ) 10 ~b 10 ( ani b b ) 10 b => a 11 (ani ( ani a ( ani a b ) ) ( ani a ( ani a b ) ) ) 11 ~a 00 ( ani a a ) 11 a => b 01 (ani ( ani b ( ani a b ) ) ( ani b ( ani a b ) ) ) 11 ~a lub ~b 10 ( ani ( ani ( ani a a ) ( ani b b ) ) ( ani ( ani a a ) ( ani b b ) ) ) 11 1 11 ( ani ( ani a ( ani a a ) ) ( ani a ( ani a a ) ) )
Implikację a=>b można też zapisać
( ani ( ani ( ani a a ) b ) ( ani ( ani a a ) b ) )
Co odpowiada definicji
( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) )
Z powyższych tworzymy zdanie, w którym mamy zdanie b przy założeniu zdefiniowania implikacji
( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ) b ) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ) b ) )
Definiujemy też tradycyjne operatory logiczne (równoważność to równość):
- negację
( = ~ ( \l x ( ani x x ) ) )
- koniunkcję
( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
- alternatywę
( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
- kwantyfikator wielki - działa na funkcje
( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
- istnienie
( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
Łączymy je i dostajemy zdanie, które mówi, że jeśli zastosujemy te symbole, to b
( => ( = ~ ( \l x ( ani x x ) ) )
( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( => ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
b
)
)
)
)
)
Wstawiamy je do poprzedniego wielkiego zdania
( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
( => ( = ~ ( \l x ( ani x x ) ) )
( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( => ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
b
)
)
)
)
)
) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
( => ( = ~ ( \l x ( ani x x ) ) )
( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( => ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
b
)
)
)
)
)
) )
Teraz w zdaniu b można korzystać z operatorów logicznych i kwantyfikatorów, a całość może działać bez wykorzystywania zewnętrznych twierdzeń.
Warto dorobić kilka definicji (nieopisanych na razie w zbiorczych wzorach)
( = tak ( \V ( \l x ( = x x ) ) ) ( = nie ( ~ tak ) ) ( = albo ( \l x ( \l y ( ani ( ani x y ) ( & x y ) ) ) ) ) ( = \V_ ( \l x ( \l y ( \V ( \l z ( & ( x z ) ( y z ) ) ) ) ) ) ) ( = \A_ ( \l x ( \l y ( \V ( \l z ( => ( x z ) ( y z ) ) ) ) ) ) ) ( = formula ( \l x ( \A y ( lub ( = ( x y ) tak ) ( = ( x y ) nie ) ) ) ) ) ( = != ( \l x ( \l y ( ~ ( = x y ) ) ) ) ) ( = \E! ( \l x ( ( \V y ( \A ( \l z ( = ( = y z ) ( x z ) ) ) ) ) ) ) ) ( = \E!_ ( \l x ( \l y ( \E! ( \l z ( & ( x z ) ( y z ) ) ) ) ) ) ) ( = <= ( \l x ( \l y ( => y x ) ) ) )
Można też opisać liczby naturalne. . oznacza liczbę zero, a 0 będzie raczej cyfrą (funkcją). Definicje się kończą, a aksjomaty wymagają chyba założenia istnienia. Aksjomaty przybierają postać:
( \E . )
( \E naturalna )
( \E 'N )
( naturalna . )
( \A ( \l x ( naturalna ( 'N x ) ) ) )
( ~ ( \V ( \l x ( & ( naturalna x ) ( = ( 'N x ) . ) ) ) ) )
( \A ( \l x ( \A ( \l y ( =>
( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
( ~ ( = ( 'N x ) ( 'N y ) ) )
) ) ) ) )
( \A ( \l x ( =>
( & ( x . ) ( \A ( \l y ( =>
( & ( naturalna y ) ( x y ) )
( x ( 'N y ) )
) ) ) )
( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
) ) )
Definicja dodawania:
( \E + ) ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) ) ( \A ( \l x ( \A ( \l y ( => ( & ( naturalna x ) ( naturalna y ) ) ( = ( + ( 'N y ) x ) ( 'N ( + y x ) ) ) ) ) ) ) )
I mnożenia:
( \E * ) ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) ) ( \A ( \l x ( \A ( \l y ( => ( & ( naturalna x ) ( naturalna y ) ) ( = ( * ( 'N y ) x ) ( + x ( * y x ) ) ) ) ) ) ) )
To znowu zbieramy
( => ( \E . )
( => ( \E naturalna )
( => ( \E 'N )
( => ( naturalna . )
( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( = ( 'N x ) . ) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
( ~ ( = ( 'N x ) ( 'N y ) ) )
) ) ) ) )
( => ( \A ( \l x ( =>
( & ( x . ) ( \A ( \l y ( =>
( & ( naturalna y ) ( x y ) )
( x ( 'N y ) )
) ) ) )
( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
) ) )
( => ( \E + )
( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( + ( 'N y ) x ) ( 'N ( + y x ) ) )
) ) ) ) )
( => ( \E * )
( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( * ( 'N y ) x ) ( + x ( * y x ) ) )
) ) ) ) )
b
)
)
)
)
)
)
)
)
)
)
)
)
)
)
i wstawiamy do z poprzednimi załorzeniami:
( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
( => ( = ~ ( \l x ( ani x x ) ) )
( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( => ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
( => ( \E . )
( => ( \E naturalna )
( => ( \E 'N )
( => ( naturalna . )
( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( = ( 'N x ) . ) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
( ~ ( = ( 'N x ) ( 'N y ) ) )
) ) ) ) )
( => ( \A ( \l x ( =>
( & ( x . ) ( \A ( \l y ( =>
( & ( naturalna y ) ( x y ) )
( x ( 'N y ) )
) ) ) )
( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
) ) )
( => ( \E + )
( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( + ( 'N y ) x ) ( 'N ( + y x ) ) )
) ) ) ) )
( => ( \E * )
( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( * ( 'N y ) x ) ( + x ( * y x ) ) )
) ) ) ) )
b
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
( => ( = ~ ( \l x ( ani x x ) ) )
( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( => ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
( => ( \E . )
( => ( \E naturalna )
( => ( \E 'N )
( => ( naturalna . )
( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( = ( 'N x ) . ) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
( ~ ( = ( 'N x ) ( 'N y ) ) )
) ) ) ) )
( => ( \A ( \l x ( =>
( & ( x . ) ( \A ( \l y ( =>
( & ( naturalna y ) ( x y ) )
( x ( 'N y ) )
) ) ) )
( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
) ) )
( => ( \E + )
( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( + ( 'N y ) x ) ( 'N ( + y x ) ) )
) ) ) ) )
( => ( \E * )
( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( * ( 'N y ) x ) ( + x ( * y x ) ) )
) ) ) ) )
b
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
) )
Wreszcie możemy zapisać 2+2=4, czyli 0''+0''=0''''
( = ( 'N ( 'N ( 'N ( 'N . ) ) ) ) ( + ( 'N ( 'N . ) ) ( 'N ( 'N . ) ) ) )
A więc po wstawieniu
( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
( => ( = ~ ( \l x ( ani x x ) ) )
( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( => ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
( => ( \E . )
( => ( \E naturalna )
( => ( \E 'N )
( => ( naturalna . )
( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( = ( 'N x ) . ) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
( ~ ( = ( 'N x ) ( 'N y ) ) )
) ) ) ) )
( => ( \A ( \l x ( =>
( & ( x . ) ( \A ( \l y ( =>
( & ( naturalna y ) ( x y ) )
( x ( 'N y ) )
) ) ) )
( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
) ) )
( => ( \E + )
( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( + ( 'N y ) x ) ( 'N ( + y x ) ) )
) ) ) ) )
( => ( \E * )
( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( * ( 'N y ) x ) ( + x ( * y x ) ) )
) ) ) ) )
( = ( 'N ( 'N ( 'N ( 'N . ) ) ) ) ( + ( 'N ( 'N . ) ) ( 'N ( 'N . ) ) ) )
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
( => ( = ~ ( \l x ( ani x x ) ) )
( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( => ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) )
( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
( => ( \E . )
( => ( \E naturalna )
( => ( \E 'N )
( => ( naturalna . )
( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( = ( 'N x ) . ) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
( ~ ( = ( 'N x ) ( 'N y ) ) )
) ) ) ) )
( => ( \A ( \l x ( =>
( & ( x . ) ( \A ( \l y ( =>
( & ( naturalna y ) ( x y ) )
( x ( 'N y ) )
) ) ) )
( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
) ) )
( => ( \E + )
( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( + ( 'N y ) x ) ( 'N ( + y x ) ) )
) ) ) ) )
( => ( \E * )
( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
( => ( \A ( \l x ( \A ( \l y ( =>
( & ( naturalna x ) ( naturalna y ) )
( = ( * ( 'N y ) x ) ( + x ( * y x ) ) )
) ) ) ) )
( = ( 'N ( 'N ( 'N ( 'N . ) ) ) ) ( + ( 'N ( 'N . ) ) ( 'N ( 'N . ) ) ) )
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
) )
Można by oczywiscie trochę krócej.
Przydadzą się nierówności i krótki zapis liczb (system dziesiętny później).
( = ( 'N . ) 1. ) ( = ( 'N 1. ) 2. ) ( = ( 'N 2. ) 3. ) ( = ( 'N 3. ) 4. ) ( = ( 'N 4. ) 5. ) ( = ( 'N 5. ) 6. ) ( = ( 'N 6. ) 7. ) ( = ( 'N 7. ) 8. ) ( = ( 'N 8. ) 9. ) ( = ( 'N 9. ) 10. )
- y jest większe lub równe
( \A_ naturalna ( \l x ( \A_ naturalna ( \l y ( lub ( = ( >= x y ) tak ) ( = ( >= x y ) nie ) ) ) ) ) ) ( \A_ naturalna ( \l x ( >= x x ) ) ) ( \A_ naturalna ( \l x ( \A_ naturalna ( \l y ( => ( >= x y ) ( >= x ( 'N y ) ) ) ) ) ) ) ( \A_ naturalna ( \l x ( \A_ naturalna ( \l y ( => ( != x y ) ( albo ( >= x y ) ( >= y x ) ) ) ) ) ) )
- nierówność ostra
( \A_ naturalna ( \l x ( \A_ naturalna ( \l y ( = ( > x y ) ( & ( != x y ) ( >= x y ) ) ) ) ) ) )
( = < ( \l x ( \l y ( > y x ) ) ) ) ( = =< ( \l x ( \l y ( >= y x ) ) ) )
Następny etap to zbiory.
Oryginalnie założę, że nie wszystko jest zbiorem.
( formula zbior )
( \A_ zbior ( \l x ( formula ( \w x ) ) ) )
( = zbiorZbiorow ( \l x ( & ( zbior x ) ( ( \A ( \w x ) ( zbior) ) ) ) ) )
( zbior {} )
( ~ ( \V ( \w {} ) ) )
( \A_ zbior ( \l x ( \A_ zbior ( \l y ( = ( \u x y ) ( \U ( {2 x y ) ) ) ) ) ) )
( \A_ zbiorZbiorow ( \l x ( = ( \nn x ) ( {f ( \l y ( \A_ ( \w x ) ( \l z ( ( \w z y ) ) ) ) ) ( ( \U x ) ) ) ) ) )
( \A_ zbior ( \l x ( \A_ zbior ( \l y ( = ( \n x y ) ( \nn ( {2 x y ) ) ) ) ) ) )
- Aksjomat ekstensjonalności
( \A_ zbior ( \l x ( \A_ zbior ( \l y ( => ( \A ( \l z ( = ( \w x z ) ( \w y z ) ) ) ) ( = x y ) ) ) ) ) )
- Aksjomat podzbioru
( \A_ zbior ( \l x ( \A_ formula ( \l y ( \A ( \l z ( = ( \w ( {f y x ) z ) ( & ( \w x z ) ( y z ) ) ) ) ) ) ) ) ) )
( \A_ zbior ( \l x ( \A_ formula ( \l y ( ( zbior ( {f y x ) ) ) ) ) ) )
- aksjomat pary
( \A_ zbior ( \l x ( \A_ zbior ( \l y ( \A ( \l z ( = ( \w ( {2 x y ) z ) ( lub ( = x z ) ( = y z ) ) ) ) ) ) ) ) )
( \A_ zbior ( \l x ( \A_ zbior ( \l y ( zbior ( {2 x y ) ) ) ) ) )
- aksjomat sumy
( \A_ zbiorZbiorow ( \l x ( \A ( \l y ( = ( \w ( \U x ) y ) ( \V_ ( \w x ) ( \l z ( \w z y ) ) ) ) ) ) ) ) ( \A_ zbiorZbiorow ( \l x ( zbior ( \U x ) ) ) )
- aksjomat zbioru potęgowego
( = \c ( \l x ( \l y ( \A_ ( \w y ) ( \w x ) ) ) ) ) ( \A_ zbior ( \l x ( = ( \w ( \P x ) ) ( \c x ) ) ) ) ( \A_ zbior ( \l x ( zbior ( \P x ) ) ) )
- aksjomat nieskończoności
( = ( \w \N ) naturalna ) ( zbior \N )
- aksjomat zastępowania
( \A_ zbior ( \l x ( \A_ ( \l y ( \A ( \l z ( zbior ( y z ) ) ) ) ) ( \l y ( = ( \w ( {z y x ) ) ( \l z ( \V_ ( \w x ) ( \l t ( = ( y t ) z ) ) ) ) ) ) ) ) )
( \A_ zbior ( \l x ( \A_ ( \l y ( \A ( \l z ( zbior ( y z ) ) ) ) ) ( \l y ( zbior ( {z y x ) ) ) ) ) )
- aksjomat regularności
( \A_ zbior ( \l x ( \V_ ( \w x ) ( \l y ( = {} ( \n x y ) ) ) ) ) )
- aksjomat wyboru
( \A_ zbiorZbiorow ( \l x ( =>
( &
( \A_ ( \w x ) ( \l y ( \A_ ( \w x ) ( \l z
( => ( != y z ) ( = {} ( \n y z ) ) )
) ) ) )
( \A_ ( \w x ) ( != {} ) )
)
( \V_ zbior ( \l y ( \A_ ( \w x ) ( \l z
( \E!_ ( \w y ) ( \w z ) )
) ) ) )
) ) )
Poprawa definiowania podzbiorów
( \A_ zbior ( \l x ( \A_ ( \l y ( formula ( \l z ( lub ( \w x z ) ( y z ) ) ) ) ) ( \l y ( = ( {f y x ) ( {f ( \l z ( & ( \w x z ) ( y z ) ) ) x ) ) ) ) ) )
( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( zbior ( {ff x ) ) ) ) )
( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( \A ( \l z ( = ( \w ( {ff x ) z ) ( x z ) ) ) ) ) ) )
Od razu przedziały liczb naturalnych:
( \A_ naturalna ( \l x ( \A_ naturalna ( \l y ( = ( [N x y ) ( {f ( \l z ( & ( >= x z ) ( >= z y ) ) ) \N ) ) ) ) ) )
( = \N+ ( {f ( > . ) \N ) )
Zbiory definiowane przez wymienienie argumentów
( \A ( \l x ( => ( \V_ zbior ( \l y ( = ( \w y ) ( = x ) ) ) ) ( & ( = ( \w ( { x ) ) ( = x ) ) ( zbior ( { x ) ) ) ) ) )
( \A ( \l x ( = ( \V_ zbior ( \l y ( = ( \w y ) ( = x ) ) ) ) ( zbior ( { x ) ) ) ) )
( formula wBudowie_{. )
( wBudowie_{. {. )
( = ( .. {. ) {} )
( \A_ wBudowie_{. ( \l x ( \A ( \l y ( = ( .. ( x y ) ) ( \u ( .. x ) ( { y ) ) ) ) ) ) )
( formula wBudowie_{n )
( \A_ ( \w \N+ ) ( \l x ( & ( & ( wBudowie_{n ( {n x ) ) ( = {} ( juz ( {n x ) ) ) ) ( = x ( ile ( {n x ) ) ) ) ) )
( \A_ wBudowie_{n ( \l x ( => ( > 1. ( ile x ) ) ( \A ( \l y ( & ( = ( 'N ( ile ( x y ) ) ) ( ile x ) ) ( = ( \u ( juz x ) ( { y ) ) ( juz ( x y ) ) ) ) ) ) ) )
( \A_ wBudowie_{n ( \l x ( => ( = 1. ( ile x ) ) ( \A ( \l y ( = ( \u ( juz x ) ( { y ) ) ( x y ) ) ) ) ) ) )
( = {} ( {n . ) )
( = {2 ( {n 2. ) )
Teraz przychodzi kolej na funkcje o określonej dziedzinie i pary.
( formula ( funkcjaZ x ) )
( \A_ funkcjaZ ( \l x ( zbior ( dziedzina x ) ) ) )
( \A_ funkcjaZ ( \l x ( \A_ funkcjaZ ( \l y
( = ( = x y ) ( & ( = ( dziedzina x ) ( dziedzina y ) ) ( \A_ ( \w ( dziedzina x ) ) ( \l z ( = ( x z ) ( y z ) ) ) ) ) )
) ) ) )
( = para ( \l x ( & ( funkcjaZ x ) ( = ( dziedzina x ) ( [N 1. 2. ) ) ) )
( \A_ ( \w \N+ ) ( \l x ( = ( n-ka x ) ( \l y ( & ( funkcjaZ y ) ( = ( dziedzina y ) ( [N 1. x ) ) ) ) ) )
( = ( n-ka . ) ( \l y ( & ( funkcjaZ x ) ( = ( dziedzina x ) {} ) ) )
( = krotka ( \l x ( \V_ naturalna ( \l y ( n-ka y x ) ) ) ) )
( \A_ krotka ( \l x ( n-ka ( dlugosc x ) x ) ) )
( \A ( \l x ( & ( n-ka 1. ( (1 x ) ) ( = x ( (1 x 1. ) ) ) ) )
( \A_ krotka ( \l x ( \A_ krotka ( \l y
( &
( n-ka ( + ( dlugosc x ) ( dlugosc y ) ) ( zloz x y ) )
( &
( \A_ ( \w ( [N 1. ( dlugosc x ) ) ) ( \l z ( = ( zloz x y z ) ( x z ) ) ) )
( \A_ ( \w ( [N 1. ( dlugosc y ) ) ) ( \l z ( = ( zloz x y ( + z ( dlugosc x ) ) ) ( y z ) ) ) )
)
)
) ) ) )
( formula wBudowie_(. ) ( wBudowie_(. (. ) ( n-ka . ( .. (. ) ) ( \A_ wBudowie_(. ( \l x ( \A ( \l y ( = ( .. ( x y ) ) ( zloz ( .. x ) ( (1 y ) ) ) ) ) ) ) ( formula wBudowie_(n ) ( \A_ ( \w \N+ ) ( \l x ( & ( & ( wBudowie_(n ( (n x ) ) ( n-ka . ( juz ( (n x ) ) ) ) ( = x ( ile ( (n x ) ) ) ) ) ) ( \A_ wBudowie_(n ( \l x ( => ( > 1. ( ile x ) ) ( \A ( \l y ( & ( = ( 'N ( ile ( x y ) ) ) ( ile x ) ) ( = ( zloz ( juz x ) ( (1 y ) ) ( juz ( x y ) ) ) ) ) ) ) ) ) ( \A_ wBudowie_(n ( \l x ( => ( = 1. ( ile x ) ) ( \A ( \l y ( = ( zloz ( juz x ) ( (1 y ) ) ( x y ) ) ) ) ) ) ) ( n-ka . ( (n . ) ) ( = (2 ( (n 2. ) )
A następnie grupy, ciała, przestrzenie wektorowe i algebry.
( formula grupoid )
( \A_ grupoid ( \l x ( zbior ( {ff ( \w x ) ) ) ) )
( \A_ grupoid ( \l x ( \A_ grupoid ( \l y ( = ( = x y ) ( & ( = ( {ff ( \w x ) ) ( {ff ( \w y ) ) ) ( \A_ ( \w x ) ( \l z ( \A_ ( \w x ) ( \l t ( = ( oG x z t ) ( oG y z t ) ) ) ) ) ) ) ) ) ) ) )
Według schematu ( laczny zbiór działanie )
( = laczny ( \l x ( \l y ( \A_ ( \w x ) ( \l a ( \A_ ( \w x ) ( \l b ( \A_ ( \w x ) ( \l c ( = ( y ( y c b ) a ) ( y c ( y b a ) ) ) ) ) ) ) ) ) )
Według schematu ( e_neutralny zbiór działanie element )
( = e_neutralny ( \l x ( \l y ( \l z ( \A_ ( \w x ) ( \l a ( & ( = ( y z a ) a ) ( = ( y a z ) a ) ) ) ) ) ) ) )
Według schematu ( e_przeciwny zbiór działanie element_a element_b )
( = e_przeciwny ( \l x ( \l y ( \l a ( \l b ( & ( e_neutralny x y ( y a b ) ) ( e_neutralny x y ( y b a ) ) ) ) ) ) ) )
Według schematu ( przemienny zbiór działanie )
( = przemienny ( \l x ( \l y ( \A_ ( \w x ) ( \l z ( \A_ ( \w x ) ( \l t ( = ( y z t ) ( y t z ) ) ) ) ) ) ) ) )
( = polgrupa ( \l x ( & ( grupoid x ) ( laczny x ( oG x ) ) ) ) ) ( = grupoid_z1 ( \l x ( & ( grupoid x ) ( \V_ ( \w x ) ( e_neutralny x ( oG x ) ) ) ) ) ) ( = lupa ( \l x ( & ( grupoid_z1 x ) ( \A_ ( \w x ) ( \l a ( \V_ ( \w x ) ( e_przeciwny x ( oG x ) a ) ) ) ) ) ) ) ( = grupa ( \l x ( & ( lupa x ) ( polgrupa x ) ) ) ) ( = grupaPrzemienna ( \l x ( & ( grupa x ) ( przemienny ( oG x ) ) ) ) )
Złóż grupę ... ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( zbior ( {ff x ) ) ) ) ) ... ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( \A ( \l z ( = ( \w ( {ff x ) z ) ( x z ) ) ) ) ) ) )
( formula pierscienioid )
( \A_ pierscienioid ( \l x ( zbior ( {ff ( \w x ) ) ) ) )
( \A_ pierscienioid ( \l x ( \A_ pierscienioid ( \l y
( = ( = x y ) ( & ( = ( {ff ( \w x ) ) ( {ff ( \w y ) ) ) ( \A_ ( \w x ) ( \l z ( \A_ ( \w x ) ( \l t ( & ( = ( +P x z t ) ( +P y z t ) ) ( = ( *P x z t ) ( *P y z t ) ) ) ) ) ) ) ) )
) ) ) )
Według schematu ( rozdzielny zbiór mnożenie dodawanie )
( = rozdzielny ( \l x ( \l y ( \l z
( \A_ ( \w x ) ( \l a ( \A_ ( \w x ) ( \l b ( \A_ ( \w x ) ( \l c
( & ( = ( z c ( y a b ) ) ( y ( z c a ) ( z c b ) ) ) ( = ( z ( y a b ) c ) ( y ( z a c ) ( z b c ) ) ) )
) ) ) ) ) )
) ) ) )
( = subpierscien ( \l x ( & ( pierscienioid x ) ( grupaPrzemienna ( zlozGrupe x ( +P x ) ) ) ) ) ) ( = pierscien_sl ( \l x ( & ( subpierscien x ) ( rozdzielny x ( +Px ) ( *P x ) ) ) ) ) ( = pierscien ( \l x ( & ( pierscien_sl x ) ( laczny x ( *P x ) ) ) ) )
... pierścień przemienny itd.
Oraz liczby rzeczywiste i zespolone.
Paradoks
( \l x ( = nie ( x x ) ) ) zastosowany na siebie
( \l x ( = ( = ani = ) ( x x ) ) ( \l x ( = ( = ani = ) ( x x ) ) ) )
