Logiczny zapis matematyki: Różnice pomiędzy wersjami
Przejdź do nawigacji
Przejdź do wyszukiwania
BartekChom (dyskusja | edycje) (liczby naturalne) |
BartekChom (dyskusja | edycje) (zbiory) |
||
| Linia 87: | Linia 87: | ||
* koniunkcję | * koniunkcję | ||
( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) ) | ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) ) | ||
| − | * | + | * alternatywę |
( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) ) | ( = lub ( \l x ( \l y ( ~ ( ani x y ) ) ) ) ) | ||
* kwantyfikator wielki - działa na funkcje | * kwantyfikator wielki - działa na funkcje | ||
| Linia 440: | Linia 440: | ||
) ) | ) ) | ||
Można by oczywiscie trochę krócej. | Można by oczywiscie trochę krócej. | ||
| + | |||
| + | Następny etap to zbiory. | ||
| + | |||
| + | Warto dorobić kilka definicji | ||
| + | ( = nie ( \A ( \l x ( & x ( ~ x ) ) ) ) | ||
| + | ( = tak ( ~ nie ) ) | ||
| + | ( = 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 ) ) ) ) ) ) ) | ||
| + | |||
| + | Oryginalnie założę, że nie wszystko jest zbiorem (ale elementy wszystkiego tworzą zbiór zbiorem). | ||
| + | |||
| + | |||
| + | ( \E zbior ) | ||
| + | ( \E \w ) | ||
| + | * Aksjomat ekstensjonalności | ||
| + | ( \A_ zbior ( \l x ( \A_ zbior ( \l y ( => ( \A ( \l z ( = ( \w x z ) ( \w y z ) ) ) ) ( = x y ) ) ) ) ) ) | ||
| + | * Aksjomat podzbioru (dla <code>( = y ( \l z tak ) )</code> mamy tworzenie zbioru) | ||
| + | ( \A ( \l x ( \A ( \l y ( \A ( \l z ( = ( \w ( {f y x ) z ) ( & ( \w x z ) ( y z ) ) ) ) ) ) ) ) ) ) | ||
| + | ( \A_ zbior ( \l x ( \A ( \l y ( ( zbior ( {f y x ) ) ) ) ) ) ) | ||
| + | * aksjomat pary | ||
| + | ( \A ( \l x ( \A ( \l y ( \ A ( \l z ( = ( \w ( {2 x y ) z ) ( lub ( = x z ) ( = y z ) ) ) ) ) ) ) ) ) | ||
| + | ( \A ( \l x ( \A ( \l y ( zbior ( {2 x y ) ) ) ) ) ) | ||
| + | * aksjomat sumy | ||
| + | ( \A ( \l x ( \A ( \l y ( = ( \w ( \U x ) y ) ( \V_ ( \w x ) ( \l z ( \w z y ) ) ) ) ) ) ) ) | ||
| + | ( \A ( \l x ( zbior ( \U x ) ) ) ) | ||
| + | * aksjomat zbioru potęgowego | ||
| + | ( = \c ( \l x ( \l y ( \A_ ( \w y ) ( \w x ) ) ) ) ) | ||
| + | ( \A ( \l x ( = ( \w ( \P x ) ) ( \c x ) ) ) ) | ||
| + | ( \A_ zbior ( \l x ( zbior ( \P x ) ) ) ) | ||
| + | * aksjomat nieskończoności | ||
| + | ( = ( \w \N ) naturalna ) | ||
| + | * aksjomat zastępowania | ||
| + | ( \A ( \l x ( \A ( \l y ( = ( \w ( {z y x ) ) ( \l z ( \V_ ( \w x ) ( \l t ( = ( y t ) ( z ) ) ) ) ) ) ) ) ) ) | ||
| + | * aksjomat regularności | ||
| + | |||
| + | * aksjomat wyboru | ||
[[Kategoria:Logiczny język]] | [[Kategoria:Logiczny język]] | ||
Wersja z 16:05, 14 lip 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ń.
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.
Następny etap to zbiory.
Warto dorobić kilka definicji
( = nie ( \A ( \l x ( & x ( ~ x ) ) ) ) ( = tak ( ~ nie ) ) ( = 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 ) ) ) ) ) ) )
Oryginalnie założę, że nie wszystko jest zbiorem (ale elementy wszystkiego tworzą zbiór zbiorem).
( \E zbior ) ( \E \w )
- Aksjomat ekstensjonalności
( \A_ zbior ( \l x ( \A_ zbior ( \l y ( => ( \A ( \l z ( = ( \w x z ) ( \w y z ) ) ) ) ( = x y ) ) ) ) ) )
- Aksjomat podzbioru (dla
( = y ( \l z tak ) )mamy tworzenie zbioru)
( \A ( \l x ( \A ( \l y ( \A ( \l z ( = ( \w ( {f y x ) z ) ( & ( \w x z ) ( y z ) ) ) ) ) ) ) ) ) )
( \A_ zbior ( \l x ( \A ( \l y ( ( zbior ( {f y x ) ) ) ) ) ) )
- aksjomat pary
( \A ( \l x ( \A ( \l y ( \ A ( \l z ( = ( \w ( {2 x y ) z ) ( lub ( = x z ) ( = y z ) ) ) ) ) ) ) ) )
( \A ( \l x ( \A ( \l y ( zbior ( {2 x y ) ) ) ) ) )
- aksjomat sumy
( \A ( \l x ( \A ( \l y ( = ( \w ( \U x ) y ) ( \V_ ( \w x ) ( \l z ( \w z y ) ) ) ) ) ) ) ) ( \A ( \l x ( zbior ( \U x ) ) ) )
- aksjomat zbioru potęgowego
( = \c ( \l x ( \l y ( \A_ ( \w y ) ( \w x ) ) ) ) ) ( \A ( \l x ( = ( \w ( \P x ) ) ( \c x ) ) ) ) ( \A_ zbior ( \l x ( zbior ( \P x ) ) ) )
- aksjomat nieskończoności
( = ( \w \N ) naturalna )
- aksjomat zastępowania
( \A ( \l x ( \A ( \l y ( = ( \w ( {z y x ) ) ( \l z ( \V_ ( \w x ) ( \l t ( = ( y t ) ( z ) ) ) ) ) ) ) ) ) )
- aksjomat regularności
- aksjomat wyboru