Tekst źródłowy strony Logiczny zapis matematyki

Częścią [[logiczny język|logicznego języka]] jest zapis matematyczny. W jednej z wersji:

== Podstawy ==
Używa się 84 znaków (dostępnych bezpośrednio z klawiatury):
<pre>
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
` ~ ! @ # $ % ^ & * ( ) - _ = + [ { ] } ; : ' " \ | , < . > / ?
</pre>
Symbole dzieli się dowolnymi białymi znakami (spacja, znak tabulacji, enter).

Jest pięć pojęć pierwotnych, których nie precyzuje się nawet aksjomatami.
* <code>(</code> - prafunkcja dwuargumentowa "pierwszy od drugiego", szczególny element składni
* <code>\l</code> - operator lambda przyjmujący dwa argumenty (zmienną związaną i wyrażenie); tworzy raczej funkcjonały niż funkcje, otrzymany funkcjonał działa zgodnie z wyrażeniem dla zwykłych rzeczy, ale dla innych takich funkcjonałów zwraca błąd (zawsze ten sam); nie może być argumentem
* <code>_A\V</code> - operator "istnieje" przyjmujący dwa argumenty (zmienną związaną i wyrażenie); traktuje wszystko, co nie jest prawdą, jak fałsz; nie może być argumentem
* <code>_Aani</code> - zwykły operator logiczny dwuargumentowy; traktuje wszystko, co nie jest prawdą, jak fałsz; po zastosowaniu do jednego argumentu dla każdej nieprawdy daje to samo
* <code>lambda</code> - zwykły operator jednoargumentowy, informuje, czy coś jest wynikiem działania lambdy

== Logika ==
Ani zastępuje wszystkie funkcje logiczne (z innymi znakami można łatwiej):

{| border
| a\b || 0 || 1
|-
| 0 || ||
|-
| 1 || ||
|}
<pre>
 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 a <= b
 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
</pre>

Równoważność zapisujemy
<pre>
 ( ( _Aani ( ( _Aani a ( ( _Aani a b ( ( _Aani b ( ( _Aani a b
</pre>

Równe jest to, co ma równe wartości dla wszystkich argumentów i jako argument dla wszystkich funkcji
<pre>
 ( ( _A<=>
  ( ( = x y
  ( ( ani
   ( ( _A\V z ( ~ ( ( = ( x z ( y z
   ( ( _A\V z ( ~ ( ( = ( z x ( z x
</pre>
Coś jest równe
<pre>
 ( ( = ani ani
</pre>
A coś jest nierówne
<pre>
 ( ( ani ( ( = ( ( = ani lambda ( ( = ani lambda
</pre>

Implikację a=>b można też zapisać
<pre>
 ( ( _Aani ( ( _Aani ( ( _Aani a a b ( ( _Aani ( ( _Aani a a b
</pre>
Co odpowiada definicji
 ( ~ ( ( _A\V x ( ( _A\V y ( ~ ( ( = ( ( _Aani ( ( _Aani ( ( _Aani x x y ( ( _Aani ( ( _Aani x x y ( ( _A=> x 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

Łą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
             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
                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
                   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 ) ) ) ) ) ) )
 ( \A ( ( \l x ( ( = ( logiczny x ( ( lub ( ( = tak x ( ( = nie x
 ( \A ( ( \l x ( ( = ( formula x ( \A ( ( \l y ( logiczny ( x y
 ( = != ( \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 ) ) ) )

== Liczby naturalne ==
Można też opisać liczby naturalne. <code>.</code> oznacza liczbę zero, a <code>0</code> będzie raczej cyfrą (funkcją). Definicje się kończą, a aksjomaty wymagają chyba założenia istnienia. Aksjomaty przybierają postać:
 ( naturalna .
 ( \A ( ( \l x ( ( => ( naturalna ( 'N x ( naturalna 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łożeniami:
 ( 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 <nowiki>0''+0''=0''''</nowiki>
 ( = ( '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. )

* x 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 ) ) ) ) ) ) )
.. sprawdzić

Zamiana kolejności argumentów
 ( ( \A ( ( \l x  ( ( \A ( ( \l y ( ( \A ( ( \l z
    ( ( = ( ( ( \kappa_1<->2 x y z ( ( x z y

 ( ( = < ( \kappa_1<->2 >
 ( ( = =< ( \kappa_1<->2 >=

Definiuje
<pre>
 ( \A ( ( \l x ( \A ( ( \l y ( ( = ( ( definiuje x y ( ( => ( \V ( ( \l z ( x z ( x y
</pre>
Działania na funkcjach zamiast na argumentach
<pre>
 ( \A ( ( \l x ( \A ( ( \l y ( ( definiuje
    ( ( \l z ( ( \A ( ( \l t ( ( = ( z t ( x ( y t
    ( ( f\l x y
 ( ( = ~\l ( f\l ~
 ( \A ( ( \l x ( \A ( ( \l y ( \A ( ( \l z ( ( definiuje
    ( ( \l t ( ( \A ( ( \l u ( ( = ( t u ( ( x ( y u ( z u
    ( ( ( o\l x y z
 ( ( = &\l ( o\l &
 ( ( = lub\l ( o\l lub
 ( ( = +\l ( o\l +
 ( ( = *\l ( o\l *
</pre>

Jedyne
<pre>
 ( ( \A_ ( ( \l a ( \V ( ~\l a
    ( ( \l a ( ( = ( a ( jedyne a ( \E! a
</pre>

== Zbiory ==
Następny etap to zbiory.

Oryginalnie założę, że nie wszystko jest zbiorem.

 ( \A ( ( \l x ( ( = ( klasa x ( formula ( \w x
 ( formula zbior
 ( ( \A_ zbior klasa
 ( ( = 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 - istnieje zbiór liczba naturalnych
 ( ( \V_ zbior ( ( \l x ( \A ( ( \l y ( ( = ( naturalna y ( ( \w x y
* 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

<pre>
 ( ( = \wen ( \kappa_1<->2 \w
</pre>

<code>\N</code> - prawdziwy "zbiór" liczb naturalnych to nie zbiór
 ( ( = ( \w \N naturalna
 ( ~ ( zbior \N

Poprawa definiowania podzbiorów
 ( ( \A_ zbior ( ( \l x ( ( \A_
    ( ( \l y ( formula ( ( \l z ( ( & ( ( \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 ) ) ) ) ) ) )

 ( ( = podzbior ( ( \l x ( ( \l y ( ( \A_ ( \w y ( \w x

 ( ( = nadzbior ( \kappa_1<->2 podzbior

Różnica zbiorów
 ( ( = -{ ( ( \l x ( ( \l y ( ( {f y ( ( \l z ( ~ ( ( \w x z

Od razu przedziały liczb naturalnych:
 ( \A ( \l x ( \A ( \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. ) )

== Funkcje ==

Teraz przychodzi kolej na funkcje o określonej dziedzinie i pary.
 ( formula funkcjaZ
 ( ( \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 ) ) ) ) ) )
 ) ) ) )
 
 ( \A ( ( \l x ( \A y ( ( =
    ( ( \V_ funkcjaZ ( ( \l z ( ( &
       ( ( = ( dziedzina z ( {ff ( \w x
       ( ( \A_ ( \w x ( ( \l t ( ( = ( y t ( z t
    ( ( & ( ( &
       ( funkcjaZ ( ( obetnij x y
       ( ( = ( dziedzina ( ( obetnij x y ( {ff ( \w x
       ( ( \A_ ( \w x ( ( \l t ( ( = ( y t ( ( ( obetnij x y t
 
 ( = 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 ) ) ) ) ) ) )
 
 ( ( \A_ krotka ( ( \l x ( \A ( ( \l y ( ( = ( ( doloz y x ( ( zloz x ( (1 y
 
 ( ( n-ka . ( (n .
 ( ( = (2 ( (n 2.

Funkcje definiujące
 ( ( = okresla ( ( \l x ( ( \l y ( ( \A_ x ( ( \l z ( ( \A_ x ( ( \l t ( ( = ( ( = z t ( ( = ( y z ( y t
 ( ( \A_ formula ( ( \l x ( \A ( ( \l y ( \A ( ( \l z ( ( &
    ( ( = ( ( \V_ x ( ( \l t ( ( = ( y t z ( x ( ( ( zloz x y z
    ( ( => ( x ( ( ( zloz x y z ( ( = ( y ( ( ( zloz x y z z

Identyczność
 ( ( = id ( ( \l x x

 ( ( = odwracalna ( ( \l x ( \V ( ( \l y ( ( = id ( ( \l z ( y ( x z
 ( ( \A_ odwracalna ( ( \l x ( \A ( ( \l y ( ( = ( ( odwrotna x ( x y y

Przerabianie funkcji działajacej na n-kach na funkcję tworzącą funkcje <code>( ( \kappa_n-ka->wieloargumentowa n f</code>
 ( ( = ( \kappa_wieloargumentowa->n-ka . id
 ( ( \A_ ( \w \N ( ( \l x ( ( \A_ ( n-ka x ( ( \l y ( \A ( ( \l z ( \A ( ( \l t ( ( =
    ( ( ( ( \kappa_wieloargumentowa->n-ka x z y t
    ( ( ( \kappa_wieloargumentowa->n-ka ( 'N x z ( doloz t y
 ( \A_ naturalna ( ( \l x ( ( & ( odwracalna ( \kappa_wieloargumentowa->n-ka x ( ( = ( \kappa_n-ka->wieloargumentowa x ( odwrotna ( \kappa_wieloargumentowa->n-ka x

== Grupy itd. ==
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 y ( \V_ ( \w x ) ( e_przeciwny x ( oG x ) y ) ) ) ) ) ) )
 ( = grupa ( \l x ( & ( lupa x ) ( polgrupa x ) ) ) )
 ( = grupaPrzemienna ( \l x ( & ( grupa x ) ( przemienny x ( oG x ) ) ) ) )

Złóż grupę
 ( \A ( ( \l x ( \A ( ( y ( ( =
    ( ( V_ grupoid ( ( \l z ( ( &
       ( ( = ( \w x ( \w z
       ( ( \A_ ( \w x ( ( \l t ( ( \A_ ( \w x ( ( \l u
          ( ( = ( ( y t u ( ( ( oG z t u
    ( ( & ( ( &
       ( grupoid ( ( zlozGrupe x y
       ( ( = ( \w x ( \w ( ( zlozGrupe x y
       ( ( \A_ ( \w x ( ( \l t ( ( \A_ ( \w x ( ( \l u
          ( ( = ( ( y t u ( ( ( oG ( ( zlozGrupe x y t u

Grupa addytywna i multiplikatywna
<pre>
 ( formula grupowosc
 ( grupowosc grupoid
 ( grupowosc polgrupa
 ( grupowosc grupoid_z1
 ( grupowosc lupa
 ( grupowosc grupa
 ( grupowosc grupaPrzemienna
</pre>
<pre>
 ( ( \A_ grupowosc ( ( \l x ( \A ( ( \l y ( ( = ( ( addytywna x y ( x ( ( zlozGrupe y ( +P x
 ( ( \A_ grupowosc ( ( \l x ( \A ( ( \l y ( ( = ( ( multiplikatywna x y ( x ( ( zlozGrupe y ( *P x
</pre>

Pierścienie
 ( 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

 ( ( \A_ subpierscien ( ( \l x ( ( ( e_neutralny x ( +P x ( 0P x

 ( ( = pierscien_sl ( ( \l x ( ( & ( subpierscien x ( ( ( rozdzielny x ( +P x ( *P x
 ( ( = pierscien ( ( \l x ( ( & ( pierscien_sl x ( ( laczny x ( *P x
 ( ( = pierscienPrzemienny ( ( \l x ( ( & ( pierscien x ( ( przemienny x ( *P x
 ( ( = pierscien_z1 ( ( \l x ( ( & ( pierscien x ( ( \V_ ( \w x ( ( e_neutralny x ( *P x

 ( ( \A_ pierscien_z1 ( ( \l x ( ( ( e_neutralny x ( *P x ( 1P x

 ( ( = pierscienBezDzielnikow0 ( ( \l x ( ( & ( pierscien x
    ( ~ ( ( \V_ ( \w ( ( -{ ( { ( 0P x x ( ( \l y ( ( \V_ ( \w ( ( -{ ( { ( 0P x x ( ( \l z
       ( ( = ( ( ( *P y z ( 0P x
 ( ( = cialo ( ( \l x ( ( & ( pierscien_z1 x ( ( \A_ ( \w ( ( -{ ( { ( 0P x x ( ( \l y ( ( \V_ ( \w x ( ( ( e_przeciwny x ( *P x y
 ( ( = cialoPrzemienne ( ( \l x ( ( & ( cialo x ( pierscienPrzemienny x
zlozPierscien
 ( \A ( ( \l x ( \A ( ( \l y ( \A ( ( \l z 
    ( ( =>
       ( ( \V_ pierscienoid ( ( \l t ( ( &
          ( \A ( ( \l a ( ( = ( ( \w t a ( ( \w x a
          ( \A_ ( \w t ( ( \l a ( \A_ ( \w t ( ( \l b ( ( &
             ( ( = ( ( ( +P t a b ( ( y a b
             ( ( = ( ( ( *P t a b ( ( z a b
    ( ( = t ( ( ( zlozPierscien x y z
Odejmowanie i dzielenie
 ( \A ( ( \l x ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( =>
    ( ( \E!_ ( \w x ( ( \l t
       ( ( & ( ( = ( ( ( +P x y t z ( ( = ( ( ( +P x t y z
    ( ( & ( ( \w x ( ( ( -P x y z ( ( & ( ( = ( ( ( +P x y ( ( ( -P x y z z ( ( = ( ( ( +P x ( ( ( -P x y z y z
 ( \A ( ( \l x ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( =>
    ( ( \E!_ ( \w x ( ( \l t
       ( ( & ( ( = ( ( ( *P x y t z ( ( = ( ( ( *P x t y z
    ( ( & ( ( \w x ( ( ( /P x y z ( ( & ( ( = ( ( ( *P x y ( ( ( /P x y z z ( ( = ( ( ( *P x ( ( ( /P x y z y z

Relacje i porządki
 ( ( = ( formula_n 1. formula
 ( ( \A_ ( \w \N+ ( ( \l x ( ( = ( formula_n ( 'N x  ( ( \l y ( \A ( ( \l z ( ( formula_n x ( y z
 ( ( = relacja ( formula_n 2.

<pre>
 ( ( \A_ klasa ( ( \l x ( ( = ( porzadkoid x ( ( & ( ( &
    ( relacja ( >P x
    ( relacja ( >=P x
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( & ( ( & ( ( &
       ( ( = ( ( ( >=P x y z ( ( lub ( ( ( >P x y z ( ( = y z
       ( ( = ( ( ( >P x y z ( ( & ( ( ( >=P x y z ( ~ ( ( = y z
       ( ( = ( ( ( >P x y z ( ( ( <P x z y
       ( ( = ( ( ( >=P x y z ( ( ( =<P x z y
</pre>
... praporządek niedopracowany
<pre>
 ( ( \A_ klasa ( ( \l x ( ( = ( prauporzadkowany x ( ( &
    ( porzadkoid  x
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( \A_ ( \w x ( ( \l t
       ( ( => ( ( & ( ( ( >=P x y z ( ( ( >=P x z t ( ( ( >=P x y t
 ( ( \A_ klasa ( ( \l x ( ( = ( uporzadkowanyCzesciowo x ( ( &
    ( prauporzadkowany x
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z
       ( ( => ( ( & ( ( ( >=P x y z ( ( ( >=P x z y ( ( = y z
 ( ( \A_ klasa ( ( \l x ( ( = ( uporzadkowany x ( ( &
    ( uporzadkowanyCzesciowo x
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z
       ( ( lub ( ( ( >=P x y z ( ( ( >=P x z y
</pre>
<pre>
 ( ( \A_ uporzadkowany ( ( \l x ( ( =>
    ( ( \V_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( ( >=P x y z
    ( ( & ( ( \w x ( najwiekszy x ( ( \A_ ( \w x ( ( \l z ( ( ( >=P x ( najwiekszy x z
 ( ( \A_ uporzadkowany ( ( \l x ( ( =>
    ( ~ ( ( \V_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( ( >=P x y z
    ( ~ ( ( \w x ( najwiekszy x
 ( ( \A_ uporzadkowany ( ( \l x ( ( =>
    ( ( \V_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( ( =<P x y z
    ( ( & ( ( \w x ( najmniejszy x ( ( \A_ ( \w x ( ( \l z ( ( ( =<P x ( najwiekszy x z
 ( ( \A_ uporzadkowany ( ( \l x ( ( =>
    ( ~ ( ( \V_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( ( =<P x y z
    ( ~ ( ( \w x ( najmniejszy x
 ( ( \A_ uporzadkowany ( ( \l x ( ( \A_ ( podstruktura x ( ( \l y ( ( = ( ( ograniczonyZGory x y
    ( ( \V_ ( \w x ( ( \l z ( ( \A_ ( \w y ( ( >=P x z
 ( ( \A_ uporzadkowany ( ( \l x ( ( \A_ ( podstruktura x ( ( \l y ( ( = ( ( ograniczonyZDolu x y
    ( ( \V_ ( \w x ( ( \l z ( ( \A_ ( \w y ( ( =<P x z
</pre>
<pre>
 ( ( \A_ klasa ( ( \l x ( ( = ( cialoPrzemienneUporzadkowane x ( ( & ( ( &
    ( cialoPrzemienne x
    ( uporzadkowany x
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( \A_ ( \w x ( ( \l t ( ( &
       ( ( => ( ( ( >=P x y z ( ( ( >=P x ( ( ( +P x t y ( ( ( +P x t z
       ( ( => ( ( & ( ( ( >=P x t ( 0P x ( ( ( >=P x ( ( ( *P x t y ( ( ( *P x t z
</pre>

gęstość, ciągłość itp.
<pre>
 ( ( \A_ uporzadkowany ( ( \l x ( ( = ( gesty x
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z
       ( ( => ( ( ( >P x y z ( ( \V_ ( \w x ( ( \l t ( ( & ( ( ( >P x y t ( ( ( >P x t z
 ( \A ( ( \l x ( ( = ( ciagleUporzadkowany x ( ( & ( ( & ( ( &
    ( uporzadkowany x
    ( gesty x
    ( ( \A_ ( podstruktura x ( ( \l y ( ( => ( ( ograniczonyZGory x y ( ( \w y ( najwiekszy y
    ( ( \A_ ( podstruktura x ( ( \l y ( ( => ( ( ograniczonyZDolu x y ( ( \w y ( najmniejszy y
</pre>

Podstruktura - coś jak podzbiór, ale z zachowaniem struktury
<pre>
 ( \A ( ( \l x ( \A ( ( l y ( ( => ( ( podstruktura x y
    ( ( &( ( podzbior x y
    ( ( & ( ( = ( +P x ( +P y
    ( ( & ( ( = ( *P x ( *P y
    ( ( & ( ( = ( >P x ( >P y
    ( ( & ( ( = ( <P x ( <P y
    ( ( & ( ( = ( >=P x ( >=P y
    ( ( & ( ( = ( =<P x ( =<P y
 ( ( \A_ klasa ( ( \l x ( \A ( ( \l y ( ( =>
    ( formula ( ( &\l ( \w x y
    ( ( definiuje
       ( ( &\l
          ( ( \l z ( ( = ( ( &\l ( \w x y ( \w z
          ( podstruktura x
       ( ( {f y x
 
 ( ( = nadstruktura ( \kappa_1<->2 podstruktura
</pre>
=== Liczby rzeczywiste i zespolone ===
... zaznaczyć, że nie definiuje
<pre>
 ( cialoPrzemienneUporzadkowane \R
 ( ciagleUporzadkowany \R
 ( ( = ( >=P \R >=
 ( ( podstruktura \R \N
 ( ( = -1. ( -. 1
 ( ( = \R+ ( ( {f ( < . \R
 ( ( = \R- ( ( {f ( > . \R
 ( ( podstruktura \C \R
 ( cialoPrzemienne \C
 ( ( = ( +P \C +
 ( ( = ( *P \C *
 ( ( = ( -P \C -
 ( ( \A_ ( \w \C ( ( \l x ( ( = ( -. x ( ( - x .
 ( ( = ( /P \C /
 ( ( = ( * \i \i -1.
 ( ( \w \C \i
</pre>
Przedziały
<pre>
 ( ( \A_ ( \w \R ( ( \l x ( ( \A_ ( \w \R ( ( \l y ( ( = ( ( ][ x y ( ( {f ( ( &\l ( > x ( ( < y \R
 ( ( \A_ ( \w \R ( ( \l x ( ( \A_ ( \w \R ( ( \l y ( ( = ( ( [] x y ( ( {f ( ( &\l ( >= x ( ( =< y \R
 ( ( \A_ ( \w \R ( ( \l x ( ( \A_ ( \w \R ( ( \l y ( ( = ( ( [[ x y ( ( {f ( ( &\l ( >= x ( ( < y \R
 ( ( \A_ ( \w \R ( ( \l x ( ( \A_ ( \w \R ( ( \l y ( ( = ( ( ]] x y ( ( {f ( ( &\l ( > x ( ( =< y \R
</pre>
Wartość bezwzględna
<pre>
 ( ( \A_ ( \w \R+ ( ( \l x ( ( = x ( | x
 ( ( = . | .
 ( ( \A_ ( \w \R- ( ( \l x ( ( = ( -. x ( | x
</pre>
Nieskończoność
<pre>
 ( ( \A_ ( \w R ( > niesk
</pre>

=== Przestrzeń topologiczna ===
<pre>
 ( ( \A_ klasa ( ( \l x ( ( = ( topologiczna x
    ( ( & ( ( & ( ( & ( ( &
       ( ( \A_ ( podzbior x ( ( \l y ( logiczny ( ( otwarty x y
       ( \A ( ( \l y ( \A ( ( \l z ( ( => ( \A ( ( \l t ( ( = ( ( \w y t ( ( \w z t ( ( = ( ( otwarty x y ( ( otwarty x z
       ( ( & ( ( otwarty x {} ( ( otwarty x x
       ( ( \A_ ( otwarty x ( ( \l y ( ( \A_ ( otwarty x ( ( \l z ( ( otwarty x ( ( \n y z
       ( ( \A_ ( podzbior ( {f ( otwarty x ( ( \l y ( ( otwarty x ( \U y
</pre>

Otoczenie
<pre>
 ( ( \A_ topologiczna ( ( \l x ( ( \A_ ( \w x ( ( \l y
    ( ( = ( ( otoczenieOtwarte x y ( ( &\l ( otwarty x ( ( \wen y
 ( ( \A_ topologiczna ( ( \l x ( ( \A_ ( \w x ( ( \l y ( \A ( ( \l z
    ( ( = ( ( otoczenie x y z ( ( & ( podzbior x z ( ( \V_ ( podzbior z ( ( otoczenieOtwarte x y
 ( ( \A_ topologiczna ( ( \l a ( ( \A_ ( \w a ( ( \l b
    ( ( = ( ( otoczenia a b ( ( {f ( ( otoczenie a b ( \P a
</pre>

Brzeg
<pre>
 ( ( \A_ topologiczna ( ( \l x( ( \A_ ( podzbior x ( ( \l y ( ( \A_ ( \w x ( ( \l z
    ( ( = ( ( ( brzegowy x y z ( ( \A_ ( ( otoczenie x z ( ( \l t ( ( & ( ( \A_ ( \w t ( \w y ( ( \A_ ( \w t ( ( ~\l ( \w y
 ( ( \A_ topologiczna ( ( \l x( ( \A_ ( podzbior x ( ( \l y ( ( = ( ( brzeg x y ( ( {f ( ( brzegowy x y x
</pre>

równoważne cechy
<pre>
 ( ( \A_ topologiczna ( ( \l x ( ( \A_ ( podzbior x ( ( \l y ( ( = ( ( otwarty x ( ( -{ y x ( ( zamkniety x y
 ( ( \A_ topologiczny ( ( \l x ( ( \A_ ( podzbior x ( ( \l y ( ( = ( ( wnetrze x y
    ( ( {f ( ( \l z ( ( \V_ ( ( &\l ( otwarty x ( podzbior y ( ( \wen z y
 ( ( \A_ topologiczny ( ( \l x ( ( \A_ ( podzbior x ( ( \l y ( ( = ( ( domkniecie x y ( ( \u ( ( brzeg x y y
</pre>

== Granice ==
Formalnie zdefiniowane dążenie działające do wszystkiego (wyrażenia y po filtrze x dąży do filtra z) (albo i nie filtrze)
<pre>
 ( \A ( ( \l x ( \A ( ( \l y ( \A ( ( \l z
    ( ( = ( ( ( _-> x y z
       ( ( \A_ ( \w z ( ( \l t ( ( \V_ ( \w x ( ( \l u
          ( ( \A_ ( \w u ( ( \l v ( ( \w t ( y v
</pre>
I formalnie zdefiniowana granica - granica po a ze zbioru filtrów b funkcji c - jedyne d z b takie, że ( ( ( _-> a c d
<pre>
 ( \A ( ( \l a ( \A ( ( \l b ( \A ( ( \l c ( ( &
    ( ( = ( ( \w b ( ( ( _lim a b c
       ( ( \E!_ ( \w b ( ( _-> a c
    ( ( => ( ( \w b ( ( ( _lim a b c
       ( ( ( _-> a c ( ( ( _lim a b c
</pre>

Granica ciągu w p-ni topologicznej
<pre>
 ( ( \A_ topologiczna ( ( \l a ( ( \A_ ( ( \l b ( ( podzbior a ( ( {z b \N ( ( \l b
    ( ( = ( ( limN a b ( jedyne ( \w ( \U ( ( ( _lim
       ( ( {z ( ( \l c ( ( [N c niesk \N
       ( ( {z ( otoczenia a a
       b
</pre>

Zwykła granica funkcji dla liczb rzeczywistych
<pre>
 ( \A ( ( \l x ( ( \A_ ( \w \R ( ( \l y ( ( => 
    ( ( \V_ ( \w \R+ ( ( \l z
       ( ( \A_ ( \w ( ( -{ ( ( ][ ( ( - z y ( ( + z y { y
          ( f\l ( \w R x
    ( ( definiuje
       ( ( \l z ( ( \A_ ( \w R+ ( ( \l t ( ( \V_ ( \w \R+ ( ( \l u
          ( ( \A_ ( \w ( ( -{ ( ( ][ ( ( - u y ( ( + u y { y
             ( f\l ( \w ( ( ][ ( ( - u y ( ( + u y x
       ( ( lim x y
</pre>

Pochodna<br />
...przynajmniej jeśli granica istnieje
<pre>
 ( \A ( ( \l x ( ( \A_ ( \w \R ( ( \l y ( ( =
    ( ( lim ( ( \l z ( ( / z ( ( - ( x y ( x ( ( + z y 
    ( ( ' x y
</pre>

== Przestrzeń wektorowa ==
<pre>
 ( ( \A_ klasa ( ( \l x ( ( = ( wektorowa x ( ( & ( ( & ( ( & ( ( &
    ( ( addytywna grupaPrzemienna x
    ( cialo ( nad x
    ( ( \A_ ( \w ( nad x ( ( \l y ( ( \A_ ( \w ( nad x ( ( \l z ( ( \A_ ( \w x ( ( \l t
       ( ( = ( ( ( *V x y ( ( ( *V x z t ( ( ( *V x ( ( ( *P ( nad x z y t
    ( ( \A_ ( \w ( nad x ( ( \l y ( ( \A_ ( \w ( nad x ( ( \l z ( ( \A_ ( \w x ( ( \l t
       ( ( = ( ( ( *V x ( ( ( +P ( nad x z y t ( ( ( +P x ( ( ( *V x z t ( ( ( *V x y t
    ( ( \A_ ( \w ( nad x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( \A_ ( \w x ( ( \l t
       ( ( = ( ( ( *V x y ( ( ( +P x t z ( ( ( +P x ( ( ( *V x y t ( ( ( *V x y z
</pre>

== Przestrzeń metryczna ==
<pre>
 ( ( \A_ klasa ( ( \l x ( ( = ( metryczna x
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z ( ( & ( ( & ( ( &
       ( ( \w \R+ ( ( ( \d x y z
       ( ( = ( ( = ( ( ( \d x y z . ( ( = y z
       ( ( = ( ( ( \d x y z ( ( ( \d x z y
       ( ( \A_ ( \w x ( ( \l t
          ( ( =< ( ( ( \d x y z ( ( + ( ( ( \d x y t ( ( ( \d x t z
</pre>
Kula
<pre>
 ( ( \A_ metryczna ( ( \l x ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w \R+ ( ( \l z
    ( ( = ( ( ( \K x y z ( ( {f ( ( \l t ( ( > z ( ( ( \d x y t x
</pre>
jest topologiczna
<pre>
 ( ( \A_ metryczna topologiczna
 ( ( \A_ metryczna ( ( \l x ( ( \A_ ( podzbior x ( ( \l y
    ( ( = ( \w ( wnetrze x y ( ( \l z ( ( \V
</pre>
Ciągi Cauchy'ego, przestrzeń zupełna
<pre>
 ( ( \A_ metryczna ( ( \l x ( ( \A_ ( ( \l y ( ( podzbior x ( ( {z y \N ( ( \l y ( ( = ( ( Cauchyego x y
    ( ( \A_ ( \w \R+ ( ( \l z ( ( \V_ ( \w \N ( ( \l t
       ( ( \A_ ( \w ( ( [N t niesk ( ( \l u ( ( \A_ ( \w ( ( [N t niesk ( ( \l v
          ( ( < ( ( ( \d x ( y u ( y v z
 ( ( \A_ metryczna ( ( \l x ( ( = ( zupelna x ( ( \A_ ( ( \l y ( ( podzbior x ( ( {z y \N ( ( \l y ( ( => ( ( Cauchyego x y ( ( \w y ( ( lim_ x y
</pre>

== Przestrzeń unormowana ==
Przestrzeń unormowana (na razie nad \R)
<pre>
 ( ( \A_ wektorowa ( ( \l x ( ( => ( ( = \R ( nad x ( ( = unormowana x ( ( & ( ( & ( ( &
    ( ( \A_ ( \w x ( ( \l y ( ( \w \R+ ( ( || x y
    ( ( \A_ ( \w x ( ( \l y ( ( = ( ( = ( ( || x y . ( ( = ( 0P x y
    ( ( \A_ ( \w x ( ( \l y ( ( ( ( \A_ ( \w ( nad x ( ( \l z
       ( ( = ( ( * ( | z ( ( || x y ( ( || x ( ( ( *V x z y
    ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z
       ( ( =< ( ( || x ( ( ( +P x y z ( ( + ( ( || x y (( || x z
</pre>
jest metryczna
<pre>
 ( ( \A_ unormowana metryczna
 ( ( \A_ unormowana ( ( \l x ( ( \A_ ( \w x ( ( \l y ( ( \A_ ( \w x ( ( \l z
    ( ( = ( ( || x ( ( ( -P x y z ( ( ( \d x y z 
</pre>

Przestrzenie Banacha
<pre>
 ( ( = ( ( &\l zupelna unormowana Banacha
</pre>

Pochodna '__ funkcji d z a do b w c
<pre>
 ( ( \A_ unormowana ( ( \l a  ( ( \A_ unormowana ( ( \l b  ( ( \A_ ( \w a ( ( \l c
    ( ( \A_ ( ( \l d ( ( \V_ ( ( otoczenie a c ( ( \l e ( ( podzbior b ( ( {f d e ( ( \l d
       ( ( jedyne
          ( ( \l e ( ( = . ( ( ( lim_ a ( ( \l f ( ( / ( ( || a f ( ( || b ( ( ( -P b e ( ( ( -P b ( d c ( d ( ( ( +P a e c ( 0P a
          ( ( ( ( '__ a b d c
</pre>

... ciagła
...liniowa
...odwracalna
... lim_
... różniczkowalne__
... osobliwa

== Twierdzenie o funkcji uwikłanej ==
Dla każdego d z a do b określonego na otoczeniu c 
<pre>
 ( ( \A_ Banacha ( ( \l a ( ( \A_ Banacha ( ( \l b  ( ( \A_ ( \w a ( ( \l c
    ( ( \A_ ( ( \l d ( ( \V_ ( ( otoczenie a c ( ( \l e ( ( podzbior b ( ( {f d e ( ( \l d
       ( ( => ( ( & ( ( ( ( różniczkowalne__ a b d c ( ~ ( osobliwa ( ( ( ( '__ a b d c
          ( odwracalna d
</pre>
... ( odwracalna d ???

== Paradoks ==
<code>( ( \l x ( ( = nie ( x x</code> zastosowany na siebie
<pre>( ( ( \l x ( ( = ( ( ani = ( x x ( ( \l x ( ( = ( ( ani = ( x x</pre>

(o ile lambda może działać na lambdę)

[[Kategoria:Logiczny język]]