Logiczny zapis matematyki: Różnice pomiędzy wersjami

Z Conlanger
Przejdź do nawigacji Przejdź do wyszukiwania
(grupy, paradoks)
(PRZERÓBKA w toku)
Linia 10: Linia 10:
 
Symbole dzieli się dowolnymi białymi znakami (spacja, znak tabulacji, enter).
 
Symbole dzieli się dowolnymi białymi znakami (spacja, znak tabulacji, enter).
  
Jest sześć pojęć pierwotnych, których nie precyzuje się nawet aksjomatami.
+
Jest pięć pojęć pierwotnych, których nie precyzuje się nawet aksjomatami.
* <code>(</code>, <code>)</code> - nawiasy używane jak w Lispie
+
* <code>(</code> - prafunkcja dwuargumentowa "pierwszy od drugiego"
 
* <code>\l</code> - operator lambda przyjmujący dwa argumenty (zmienną związaną i wyrażenie; tworzy raczej funkcjonały niż funkcje)
 
* <code>\l</code> - operator lambda przyjmujący dwa argumenty (zmienną związaną i wyrażenie; tworzy raczej funkcjonały niż funkcje)
 
* <code>\V</code> - operator jednoargumentowy, przyjmuje funkcjonał i zwraca prawdę, jeśli coś może dać jeden
 
* <code>\V</code> - operator jednoargumentowy, przyjmuje funkcjonał i zwraca prawdę, jeśli coś może dać jeden
Linia 28: Linia 28:
  
 
  00 0
 
  00 0
  00 ( ani a ( ani a a ) )
+
  00 ( ( ani a ( ( ani a a
 
   
 
   
 
  00 a i b
 
  00 a i b
  01 ( ani ( ani a a ) ( ani b b ) )
+
  01 ( ( ani ( ( ani a a ( ( ani b b
 
   
 
   
 
  00 a i ~b
 
  00 a i ~b
  10 ( ani b ( ani a b ) )
+
  10 ( ( ani b ( ( ani a b
 
   
 
   
 
  00 a
 
  00 a
Linia 40: Linia 40:
 
   
 
   
 
  01 ~a i b
 
  01 ~a i b
  00 ( ani a ( ani a b ) )
+
  00 ( ( ani a ( ( ani a b
 
   
 
   
 
  01 b
 
  01 b
Linia 46: Linia 46:
 
   
 
   
 
  01 a albo b
 
  01 a albo b
  10 ( ani ( ani a b ) ( ani ( ani a a ) ( ani b b ) )
+
  10 ( ( ani ( ( ani a b ( ( ani ( ( ani a a ( ( ani b b
 
   
 
   
 
  01 a lub b
 
  01 a lub b
  11 ( ani ( ani a b ) ( ani a b ) )
+
  11 ( ( ani ( ( ani a b ( ani a b
 
   
 
   
 
  10 a ani b
 
  10 a ani b
  00 ( ani a b )
+
  00 ( ( ani a b
 
   
 
   
 
  10 a <=> b
 
  10 a <=> b
  01 (ani ( ani a ( ani a b ) ) ( ani b ( ani a b ) ) )
+
  01 ( ( ani ( ( ani a ( ( ani a b ( ( ani b ( ( ani a b
 
   
 
   
 
  10 ~b
 
  10 ~b
  10 ( ani b b )
+
  10 ( ( ani b b
 
   
 
   
  10 b => a
+
  10 a <= b
  11 (ani ( ani a ( ani a b ) ) ( ani a ( ani a b ) ) )
+
  11 ( ( ani ( ( ani a ( ( ani a b ( ( ani a ( ( ani a b
 
   
 
   
 
  11 ~a
 
  11 ~a
  00 ( ani a a )
+
  00 ( ( ani a a
 
   
 
   
 
  11 a => b
 
  11 a => b
  01 (ani ( ani b ( ani a b ) ) ( ani b ( ani a b ) ) )
+
  01 ( ( ani ( ( ani b ( ( ani a b ( ( ani b ( ( ani a b
 
   
 
   
 
  11 ~a lub ~b
 
  11 ~a lub ~b
  10 ( ani ( ani ( ani a a ) ( ani b b ) ) ( ani ( ani a a ) ( ani b b ) ) )
+
  10 ( ( ani ( ( ani ( ( ani a a ( ( ani b b ( ( ani ( ( ani a a ( ( ani b b
 
   
 
   
 
  11 1
 
  11 1
  11 ( ani ( ani a ( ani a a ) ) ( ani a ( ani a a ) ) )
+
  11 ( ( ani ( ( ani a ( ( ani a a ( ( ani a ( ( ani a a
  
 
Implikację a=>b można też zapisać
 
Implikację a=>b można też zapisać
  ( ani ( ani ( ani a a ) b ) ( ani ( ani a a ) b ) )
+
  ( ( ani ( ( ani ( ( ani a a b ( ( ani ( ( ani a a b
 
Co odpowiada definicji
 
Co odpowiada definicji
  ( = => ( \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
 
Z powyższych tworzymy zdanie, w którym mamy zdanie b przy założeniu zdefiniowania implikacji
 
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 ( ( 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 ) )
+
     ( ( 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ść):
 
Definiujemy też tradycyjne operatory logiczne (równoważność to równość):
 
* negację
 
* negację
  ( = ~ ( \l x ( ani x x ) ) )
+
  ( ( = ~ ( ( \l x ( ( ani x x
 
* koniunkcję
 
* koniunkcję
  ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
+
  ( ( = & ( ( \l x ( ( \l y ( ( ani ( ~ x ( ~ y
 
* alternatywę
 
* 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
  ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
+
  ( ( = \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
 
Łączymy je i dostajemy zdanie, które mówi, że jeśli zastosujemy te symbole, to b
  ( => ( = ~ ( \l x ( ani x x ) ) )
+
  ( ( => ( ( = ~ ( ( \l x ( ( ani x x
     ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
+
     ( ( => ( ( = & ( ( \l x ( ( \l y ( ( ani ( ~ x ( ~ y
       ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
+
       ( ( => ( ( = lub ( ( \l x ( ( \l y ( ~ ( ( ani  x y
           ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
+
           ( ( => ( ( = \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
 
                 b
 
                 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
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
 
                   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ń.
 
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ń.
  
Linia 146: Linia 127:
  
 
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ć:
 
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ć:
( \E . )
+
  ( naturalna .
( \E naturalna )
+
  ( \A ( ( \l x ( ( => ( naturalna ( 'N x ( naturalna x
( \E 'N )
 
  ( naturalna . )
 
  ( \A ( \l x ( naturalna ( 'N x ) ) ) )
 
 
  ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
 
  ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
 
  ( \A ( \l x ( \A ( \l y ( =>
 
  ( \A ( \l x ( \A ( \l y ( =>
Linia 485: Linia 463:
 
   
 
   
 
  ( zbior {} )
 
  ( zbior {} )
  ( ~ ( \V ( \w {} ) ) )
+
  ( ~ ( \V ( \w {}
 
  ( \A_ zbior ( \l x ( \A_ zbior ( \l y ( = ( \u x y ) ( \U ( {2 x y ) ) ) ) ) ) )
 
  ( \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_ zbiorZbiorow ( \l x ( = ( \nn x ) ( {f ( \l y ( \A_ ( \w x ) ( \l z ( ( \w z y ) ) ) ) ) ( ( \U x ) ) ) ) ) )  
Linia 530: Linia 508:
 
  ( \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 ) ) ) ) ) ) ( 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 ) ) ) ) ) ) )
 
  ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( \A ( \l z ( = ( \w ( {ff x ) z ) ( x z ) ) ) ) ) ) )
 +
 +
Różnica zbiorów
 +
( ( = -{ ( ( \l x ( ( \l y ( ( {f y ( ( \l z ( ~ ( ( \w x z
  
 
Od razu przedziały liczb naturalnych:
 
Od razu przedziały liczb naturalnych:
Linia 554: Linia 535:
  
 
Teraz przychodzi kolej na funkcje o określonej dziedzinie i pary.
 
Teraz przychodzi kolej na funkcje o określonej dziedzinie i pary.
  ( formula ( funkcjaZ x ) )
+
  ( formula funkcjaZ
  ( \A_ funkcjaZ ( \l x ( zbior ( dziedzina x ) ) ) )
+
  ( ( \A_ funkcjaZ ( ( \l x ( zbior ( dziedzina x
 
  ( \A_ funkcjaZ ( \l x ( \A_ funkcjaZ ( \l y
 
  ( \A_ funkcjaZ ( \l x ( \A_ funkcjaZ ( \l y
 
     ( = ( = x y ) ( & ( = ( dziedzina x ) ( dziedzina y ) ) ( \A_ ( \w ( dziedzina x ) ) ( \l z ( = ( x z ) ( y z ) ) ) ) ) )
 
     ( = ( = 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. ) ) ) )
 
  ( = para ( \l x ( & ( funkcjaZ x ) ( = ( dziedzina x ) ( [N 1. 2. ) ) ) )
Linia 565: Linia 555:
 
  ( = krotka ( \l x ( \V_ naturalna ( \l y ( n-ka y x ) ) ) ) )
 
  ( = krotka ( \l x ( \V_ naturalna ( \l y ( n-ka y x ) ) ) ) )
 
  ( \A_ krotka ( \l x ( n-ka ( dlugosc x ) x ) ) )
 
  ( \A_ krotka ( \l x ( n-ka ( dlugosc x ) x ) ) )
  ( \A ( \l x ( & ( n-ka 1. ( (1 x ) ) ( = x ( (1 x 1. ) ) ) ) )
+
  ( \A ( ( \l x ( ( & ( ( n-ka 1. ( (1 x ( ( = x ( ( (1 x 1.
 
   
 
   
  ( \A_ krotka ( \l x ( \A_ krotka ( \l y
+
  ( ( \A_ krotka ( ( \l x ( ( \A_ krotka ( ( \l y
     ( &
+
     ( ( &
       ( n-ka ( + ( dlugosc x ) ( dlugosc y ) ) ( zloz x 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 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 ) ) ) )
+
           ( ( \A_ ( \w ( ( [N 1. ( dlugosc y ( ( \l z ( ( = ( ( ( zloz x y ( ( + z ( dlugosc x ( y z
      )
 
    )
 
) ) ) )
 
  
  ( formula wBudowie_(. )
+
  ( formula wBudowie_(.
  ( wBudowie_(. (. )
+
  ( wBudowie_(. (.
  ( n-ka . ( .. (. ) )
+
  ( ( n-ka . ( .. (.
  ( \A_ wBudowie_(. ( \l x ( \A ( \l y ( = ( .. ( x y ) ) ( zloz ( .. x ) ( (1 y ) ) ) ) ) ) )
+
  ( ( \A_ wBudowie_(. ( ( \l x ( \A ( ( \l y ( ( = ( .. ( x y ( ( zloz ( .. x ( (1 y
 
   
 
   
 
  ( formula wBudowie_(n )
 
  ( formula wBudowie_(n )
Linia 590: Linia 577:
 
  ( = (2 ( (n 2. ) )
 
  ( = (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
 +
   
 +
... ( ( \kappa_n-ka->w-a n f
  
 
A następnie grupy, ciała, przestrzenie wektorowe i algebry.
 
A następnie grupy, ciała, przestrzenie wektorowe i algebry.
Linia 608: Linia 601:
 
  ( = polgrupa ( \l x ( & ( grupoid x ) ( laczny x ( oG x ) ) ) ) )
 
  ( = polgrupa ( \l x ( & ( grupoid x ) ( laczny x ( oG x ) ) ) ) )
 
  ( = grupoid_z1 ( \l x ( & ( grupoid x ) ( \V_ ( \w x ) ( e_neutralny 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 ) ) ) ) ) ) )
+
  ( = 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 ) ) ) )
 
  ( = grupa ( \l x ( & ( lupa x ) ( polgrupa x ) ) ) )
  ( = grupaPrzemienna ( \l x ( & ( grupa x ) ( przemienny ( oG x ) ) ) ) )
+
  ( = grupaPrzemienna ( \l x ( & ( grupa x ) ( przemienny x ( oG x ) ) ) ) )
  
 
Złóż grupę
 
Złóż grupę
... ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( zbior ( {ff x ) ) ) ) )
+
( \A ( ( \l x ( \A ( ( y ( ( =
... ( \A ( \l x ( = ( V_ zbior ( \l y ( \A ( \l z ( = ( \w y z ) ( x z ) ) ) ) ) ) ( \A ( \l z ( = ( \w ( {ff x ) z ) ( x z ) ) ) ) ) ) )
+
    ( ( 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
  
 
  ( formula pierscienioid )
 
  ( formula pierscienioid )
Linia 629: Linia 630:
 
  ) ) ) )
 
  ) ) ) )
  
  ( = subpierscien ( \l x ( & ( pierscienioid x ) ( grupaPrzemienna ( zlozGrupe x ( +P x ) ) ) ) ) )
+
  ( ( = 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 ) ) ) ) )
+
  ( ( \A_ subpierscien ( ( \l x ( ( ( e_neutralny x ( +P x ( 0P x
... pierścień przemienny itd.
+
 
 +
( ( = 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
 +
 
 +
Oraz liczby rzeczywiste i zespolone
 +
( zbior \R
 +
( cialoPrzemienne ( ( ( zlozPierscien \R + *
 +
( ( podzbior \R \N
 +
...
  
Oraz liczby rzeczywiste i zespolone.
+
Twierdzenie o funkcji uwikłanej
  
 
== Paradoks ==
 
== Paradoks ==
<code>( \l x ( = nie ( x x ) ) )</code> zastosowany na siebie
+
<code>( ( \l x ( ( = nie ( x x</code> zastosowany na siebie
  ( \l x ( = ( = ani = ) ( x x ) ) ( \l x ( = ( = ani = ) ( x x ) ) ) )
+
  ( ( ( \l x ( ( = ( ( ani = ( x x ( ( \l x ( ( = ( ( ani = ( x x
  
 
[[Kategoria:Logiczny język]]
 
[[Kategoria:Logiczny język]]

Wersja z 16:29, 26 gru 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 pięć pojęć pierwotnych, których nie precyzuje się nawet aksjomatami.

  • ( - prafunkcja dwuargumentowa "pierwszy od drugiego"
  • \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ć jeden
  • ani - 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 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

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

Łą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 ) ) ) ) ) ) )
( = 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ć:

( 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ł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 ) ) ) ) ) ) )

Różnica zbiorów

( ( = -{ ( ( \l x ( ( \l y ( ( {f y ( ( \l z ( ~ ( ( \w 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
( ( \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 ) ) ) ) ) ) )

( 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
   

... ( ( \kappa_n-ka->w-a n f

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
( 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

Oraz liczby rzeczywiste i zespolone

( zbior \R
( cialoPrzemienne ( ( ( zlozPierscien \R + *
( ( podzbior \R \N

...

Twierdzenie o funkcji uwikłanej

Paradoks

( ( \l x ( ( = nie ( x x zastosowany na siebie

( ( ( \l x ( ( = ( ( ani = ( x x ( ( \l x ( ( = ( ( ani = ( x x