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

Z Conlanger
Przejdź do nawigacji Przejdź do wyszukiwania
(poprawki, poszerzenie)
(liczby naturalne)
Linia 86: Linia 86:
 
  ( = ~ ( \l x ( ani x x ) ) )
 
  ( = ~ ( \l x ( ani x x ) ) )
 
* koniunkcję
 
* koniunkcję
  ( = i ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
+
  ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
 
* elternatywę
 
* elternatywę
 
  ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
 
  ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
Linia 95: Linia 95:
 
Łą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 ) ) )
     ( => ( = i ( \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 ) ) ) ) ) )
Linia 108: Linia 108:
 
  ( 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 ) ) ) ) ) )
 
  ( 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 ( ani x x ) ) )
       ( => ( = i ( \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 ) ) ) ) ) )
Linia 120: Linia 120:
 
  ) ( 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 ) ) ) ) ) )
 
  ) ( 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 ( ani x x ) ) )
       ( => ( = i ( \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 ) ) ) ) ) )
Linia 132: Linia 132:
 
  ) )
 
  ) )
 
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ń.
 +
 +
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 . )
 +
( \E naturalna )
 +
( \E 'N )
 +
( naturalna . )
 +
( \A ( \l x ( naturalna ( 'N x ) ) ) )
 +
( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
 +
( \A ( \l x ( \A ( \l y ( =>
 +
    ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
 +
    ( ~ ( = ( 'N x ) ( 'N y ) ) )
 +
) ) ) ) )
 +
( \A ( \l x ( =>
 +
    ( & ( x . ) ( \A ( \l y ( =>
 +
      ( & ( naturalna y ) ( x y ) )
 +
      ( x ( 'N y ) )
 +
    ) ) ) )
 +
    ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
 +
) ) )
 +
 +
Definicja dodawania:
 +
( \E + )
 +
( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
 +
( \A ( \l x ( \A ( \l y ( =>
 +
    ( & ( naturalna x ) ( naturalna y ) )
 +
    ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
 +
) ) ) ) )
 +
I mnożenia:
 +
( \E * )
 +
( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
 +
( \A ( \l x ( \A ( \l y ( =>
 +
    ( & ( naturalna x ) ( naturalna y ) )
 +
    ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
 +
) ) ) ) )
 +
 +
To znowu zbieramy
 +
( => ( \E . )
 +
    ( => ( \E naturalna )
 +
      ( => ( \E 'N )
 +
          ( => ( naturalna . )
 +
            ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
 +
                ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
 +
                  ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                      ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
 +
                      ( ~ ( = ( 'N x ) ( 'N y ) ) )
 +
                  ) ) ) ) )
 +
                      ( => ( \A ( \l x ( =>
 +
                        ( & ( x . ) ( \A ( \l y ( =>
 +
                            ( & ( naturalna y ) ( x y ) )
 +
                            ( x ( 'N y ) )
 +
                        ) ) ) )
 +
                        ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
 +
                      ) ) )
 +
                        ( =>  ( \E + )
 +
                            ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
 +
                              ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                  ( & ( naturalna x ) ( naturalna y ) )
 +
                                  ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
 +
                              ) ) ) ) )
 +
                                  ( => ( \E * )
 +
                                    ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
 +
                                        ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                          ( & ( naturalna x ) ( naturalna y ) )
 +
                                          ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
 +
                                        ) ) ) ) )
 +
                                          b
 +
                                        )
 +
                                    )
 +
                                  )
 +
                              )
 +
                            )
 +
                        )
 +
                      )
 +
                  )
 +
                )
 +
            )
 +
          )
 +
      )
 +
    )
 +
)
 +
i wstawiamy do z poprzednimi załorzeniami:
 +
( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
 +
    ( => ( = ~ ( \l x ( ani x x ) ) )
 +
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
 +
          ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
 +
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
 +
                ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
 +
                  ( => ( \E . )
 +
                      ( => ( \E naturalna )
 +
                        ( => ( \E 'N )
 +
                            ( => ( naturalna . )
 +
                              ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
 +
                                  ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
 +
                                    ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                        ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
 +
                                        ( ~ ( = ( 'N x ) ( 'N y ) ) )
 +
                                    ) ) ) ) )
 +
                                        ( => ( \A ( \l x ( =>
 +
                                          ( & ( x . ) ( \A ( \l y ( =>
 +
                                              ( & ( naturalna y ) ( x y ) )
 +
                                              ( x ( 'N y ) )
 +
                                          ) ) ) )
 +
                                          ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
 +
                                        ) ) )
 +
                                          ( =>  ( \E + )
 +
                                              ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
 +
                                                ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                                    ( & ( naturalna x ) ( naturalna y ) )
 +
                                                    ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
 +
                                                ) ) ) ) )
 +
                                                    ( => ( \E * )
 +
                                                      ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
 +
                                                          ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                                            ( & ( naturalna x ) ( naturalna y ) )
 +
                                                            ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
 +
                                                          ) ) ) ) )
 +
                                                            b
 +
                                                          )
 +
                                                      )
 +
                                                    )
 +
                                                )
 +
                                              )
 +
                                          )
 +
                                        )
 +
                                    )
 +
                                  )
 +
                              )
 +
                            )
 +
                        )
 +
                      )
 +
                  )
 +
                )
 +
            )
 +
          )
 +
      )
 +
    )
 +
) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
 +
    ( => ( = ~ ( \l x ( ani x x ) ) )
 +
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
 +
          ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
 +
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
 +
                ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
 +
                  ( => ( \E . )
 +
                      ( => ( \E naturalna )
 +
                        ( => ( \E 'N )
 +
                            ( => ( naturalna . )
 +
                              ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
 +
                                  ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
 +
                                    ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                        ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
 +
                                        ( ~ ( = ( 'N x ) ( 'N y ) ) )
 +
                                    ) ) ) ) )
 +
                                        ( => ( \A ( \l x ( =>
 +
                                          ( & ( x . ) ( \A ( \l y ( =>
 +
                                              ( & ( naturalna y ) ( x y ) )
 +
                                              ( x ( 'N y ) )
 +
                                          ) ) ) )
 +
                                          ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
 +
                                        ) ) )
 +
                                          ( =>  ( \E + )
 +
                                              ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
 +
                                                ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                                    ( & ( naturalna x ) ( naturalna y ) )
 +
                                                    ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
 +
                                                ) ) ) ) )
 +
                                                    ( => ( \E * )
 +
                                                      ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
 +
                                                          ( => ( \A ( \l x ( \A ( \l y ( =>
 +
                                                            ( & ( naturalna x ) ( naturalna y ) )
 +
                                                            ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
 +
                                                          ) ) ) ) )
 +
                                                            b
 +
                                                          )
 +
                                                      )
 +
                                                    )
 +
                                                )
 +
                                              )
 +
                                          )
 +
                                        )
 +
                                    )
 +
                                  )
 +
                              )
 +
                            )
 +
                        )
 +
                      )
 +
                  )
 +
                )
 +
            )
 +
          )
 +
      )
 +
    )
 +
) )
 +
 +
Wreszcie możemy zapisać 2+2=4, czyli <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.
  
 
[[Kategoria:Logiczny język]]
 
[[Kategoria:Logiczny język]]

Wersja z 17:47, 1 lip 2009

Częścią logicznego języka jest zapis matematyczny. W jednej z wersji:

Używa się 84 znaków (dostępnych bezpośrednio z klawiatury):

a b c d e f g h i j k l m n o p q r s t u v w x y z
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
1 2 3 4 5 6 7 8 9 0
` ~ ! @ # $ % ^ & * ( ) - _ = + [ { ] } ; : ' " \ | , < . > / ?

Symbole dzieli się dowolnymi białymi znakami (spacja, znak tabulacji, enter).

Jest sześć pojęć pierwotnych, których nie precyzuje się nawet aksjomatami.

  • (, ) - nawiasy używane jak w Lispie
  • \l - operator lambda przyjmujący dwa argumenty (zmienną związaną i wyrażenie; tworzy raczej funkcjonały niż funkcje)
  • \V - operator jednoargumentowy, przyjmuje funkcjonał i zwraca prawdę, jeśli coś może dać 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 b => a
11 (ani ( ani a ( ani a b ) ) ( ani a ( ani a b ) ) )

11 ~a
00 ( ani a a )

11 a => b
01 (ani ( ani b ( ani a b ) ) ( ani b ( ani a b ) ) )

11 ~a lub ~b
10 ( ani ( ani ( ani a a ) ( ani b b ) ) ( ani ( ani a a ) ( ani b b ) ) )

11 1
11 ( ani ( ani a ( ani a a ) ) ( ani a ( ani a a ) ) )

Implikację a=>b można też zapisać

( ani ( ani ( ani a a ) b ) ( ani ( ani a a ) b ) )

Co odpowiada definicji

( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) )

Z powyższych tworzymy zdanie, w którym mamy zdanie b przy założeniu zdefiniowania implikacji

( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ) b )
   ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ) b ) )

Definiujemy też tradycyjne operatory logiczne (równoważność to równość):

  • negację
( = ~ ( \l x ( ani x x ) ) )
  • koniunkcję
( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
  • elternatywę
( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
  • kwantyfikator wielki - działa na funkcje
( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
  • istnienie
( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )

Łączymy je i dostajemy zdanie, które mówi, że jeśli zastosujemy te symbole, to b

( => ( = ~ ( \l x ( ani x x ) ) )
   ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
      ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
         ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
            ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
               b
            )
         )
      )
   )
)

Wstawiamy je do poprzedniego wielkiego zdania

( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
   ( => ( = ~ ( \l x ( ani x x ) ) )
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
         ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
               ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
                  b
               )
            )
         )
      )
   )
) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
   ( => ( = ~ ( \l x ( ani x x ) ) )
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
         ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
               ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
                  b
               )
            )
         )
      )
   )
) )

Teraz w zdaniu b można korzystać z operatorów logicznych i kwantyfikatorów, a całość może działać bez wykorzystywania zewnętrznych twierdzeń.

Można też opisać liczby naturalne. . oznacza liczbę zero, a 0 będzie raczej cyfrą (funkcją). Definicje się kończą, a aksjomaty wymagają chyba założenia istnienia. Aksjomaty przybierają postać:

( \E . )
( \E naturalna )
( \E 'N )
( naturalna . )
( \A ( \l x ( naturalna ( 'N x ) ) ) )
( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
( \A ( \l x ( \A ( \l y ( =>
   ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
   ( ~ ( = ( 'N x ) ( 'N y ) ) )
) ) ) ) )
( \A ( \l x ( =>
   ( & ( x . ) ( \A ( \l y ( =>
      ( & ( naturalna y ) ( x y ) )
      ( x ( 'N y ) )
   ) ) ) )
   ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
) ) )

Definicja dodawania:

( \E + )
( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
( \A ( \l x ( \A ( \l y ( => 
   ( & ( naturalna x ) ( naturalna y ) )
   ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
) ) ) ) )

I mnożenia:

( \E * )
( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
( \A ( \l x ( \A ( \l y ( => 
   ( & ( naturalna x ) ( naturalna y ) )
   ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
) ) ) ) )

To znowu zbieramy

( => ( \E . )
   ( => ( \E naturalna )
      ( => ( \E 'N )
         ( => ( naturalna . )
            ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
               ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
                  ( => ( \A ( \l x ( \A ( \l y ( =>
                     ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
                     ( ~ ( = ( 'N x ) ( 'N y ) ) )
                  ) ) ) ) )
                     ( => ( \A ( \l x ( =>
                        ( & ( x . ) ( \A ( \l y ( =>
                           ( & ( naturalna y ) ( x y ) )
                           ( x ( 'N y ) )
                        ) ) ) )
                        ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
                     ) ) )
                        ( =>  ( \E + )
                           ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
                              ( => ( \A ( \l x ( \A ( \l y ( => 
                                 ( & ( naturalna x ) ( naturalna y ) )
                                 ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
                              ) ) ) ) )
                                 ( => ( \E * )
                                    ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
                                       ( => ( \A ( \l x ( \A ( \l y ( => 
                                          ( & ( naturalna x ) ( naturalna y ) )
                                          ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
                                       ) ) ) ) )
                                          b
                                       )
                                    )
                                 )
                              )
                           )
                        )
                     )
                  )
               )
            )
         )
      )
   )
)

i wstawiamy do z poprzednimi załorzeniami:

( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
   ( => ( = ~ ( \l x ( ani x x ) ) )
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
         ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
               ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
                  ( => ( \E . )
                     ( => ( \E naturalna )
                        ( => ( \E 'N )
                           ( => ( naturalna . )
                              ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
                                 ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
                                    ( => ( \A ( \l x ( \A ( \l y ( =>
                                       ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
                                       ( ~ ( = ( 'N x ) ( 'N y ) ) )
                                    ) ) ) ) )
                                       ( => ( \A ( \l x ( =>
                                          ( & ( x . ) ( \A ( \l y ( =>
                                             ( & ( naturalna y ) ( x y ) )
                                             ( x ( 'N y ) )
                                          ) ) ) )
                                          ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
                                       ) ) )
                                          ( =>  ( \E + )
                                             ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
                                                ( => ( \A ( \l x ( \A ( \l y ( => 
                                                   ( & ( naturalna x ) ( naturalna y ) )
                                                   ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
                                                ) ) ) ) )
                                                   ( => ( \E * )
                                                      ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
                                                         ( => ( \A ( \l x ( \A ( \l y ( => 
                                                            ( & ( naturalna x ) ( naturalna y ) )
                                                            ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
                                                         ) ) ) ) )
                                                            b
                                                         )
                                                      )
                                                   )
                                                )
                                             )
                                          )
                                       )
                                    )
                                 )
                              )
                           )
                        )
                     )
                  )
               )
            )
         )
      )
   )
) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
   ( => ( = ~ ( \l x ( ani x x ) ) )
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
         ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
               ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
                  ( => ( \E . )
                     ( => ( \E naturalna )
                        ( => ( \E 'N )
                           ( => ( naturalna . )
                              ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
                                 ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
                                    ( => ( \A ( \l x ( \A ( \l y ( =>
                                       ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
                                       ( ~ ( = ( 'N x ) ( 'N y ) ) )
                                    ) ) ) ) )
                                       ( => ( \A ( \l x ( =>
                                          ( & ( x . ) ( \A ( \l y ( =>
                                             ( & ( naturalna y ) ( x y ) )
                                             ( x ( 'N y ) )
                                          ) ) ) )
                                          ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
                                       ) ) )
                                          ( =>  ( \E + )
                                             ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
                                                ( => ( \A ( \l x ( \A ( \l y ( => 
                                                   ( & ( naturalna x ) ( naturalna y ) )
                                                   ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
                                                ) ) ) ) )
                                                   ( => ( \E * )
                                                      ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
                                                         ( => ( \A ( \l x ( \A ( \l y ( => 
                                                            ( & ( naturalna x ) ( naturalna y ) )
                                                            ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
                                                         ) ) ) ) )
                                                            b
                                                         )
                                                      )
                                                   )
                                                )
                                             )
                                          )
                                       )
                                    )
                                 )
                              )
                           )
                        )
                     )
                  )
               )
            )
         )
      )
   )
) )

Wreszcie możemy zapisać 2+2=4, czyli 0''+0''=0''''

( = ( 'N ( 'N ( 'N ( 'N . ) ) ) ) ( + ( 'N ( 'N . ) ) ( 'N ( 'N . ) ) ) )

A więc po wstawieniu

( ani ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
   ( => ( = ~ ( \l x ( ani x x ) ) )
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
         ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
               ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
                  ( => ( \E . )
                     ( => ( \E naturalna )
                        ( => ( \E 'N )
                           ( => ( naturalna . )
                              ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
                                 ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
                                    ( => ( \A ( \l x ( \A ( \l y ( =>
                                       ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
                                       ( ~ ( = ( 'N x ) ( 'N y ) ) )
                                    ) ) ) ) )
                                       ( => ( \A ( \l x ( =>
                                          ( & ( x . ) ( \A ( \l y ( =>
                                             ( & ( naturalna y ) ( x y ) )
                                             ( x ( 'N y ) )
                                          ) ) ) )
                                          ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
                                       ) ) )
                                          ( =>  ( \E + )
                                             ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
                                                ( => ( \A ( \l x ( \A ( \l y ( => 
                                                   ( & ( naturalna x ) ( naturalna y ) )
                                                   ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
                                                ) ) ) ) )
                                                   ( => ( \E * )
                                                      ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
                                                         ( => ( \A ( \l x ( \A ( \l y ( => 
                                                            ( & ( naturalna x ) ( naturalna y ) )
                                                            ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
                                                         ) ) ) ) )
                                                            ( = ( 'N ( 'N ( 'N ( 'N . ) ) ) ) ( + ( 'N ( 'N . ) ) ( 'N ( 'N . ) ) ) )
                                                         )
                                                      )
                                                   )
                                                )
                                             )
                                          )
                                       )
                                    )
                                 )
                              )
                           )
                        )
                     )
                  )
               )
            )
         )
      )
   )
) ( ani ( ani ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) ( = => ( \l x ( \l y ( ani ( ani ( ani x x ) y ) ( ani ( ani x x ) y ) ) ) ) ) )
   ( => ( = ~ ( \l x ( ani x x ) ) )
      ( => ( = & ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
         ( => ( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
            ( => ( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
               ( => ( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )
                  ( => ( \E . )
                     ( => ( \E naturalna )
                        ( => ( \E 'N )
                           ( => ( naturalna . )
                              ( => ( \A ( \l x ( naturalna ( 'N x ) ) ) )
                                 ( => ( ~ ( \V ( \l x ( & ( naturalna x ) ( =  ( 'N x ) . ) ) ) ) )
                                    ( => ( \A ( \l x ( \A ( \l y ( =>
                                       ( & ( & ( naturalna x ) ( naturalna y ) ) ( ~ ( = x y ) ) )
                                       ( ~ ( = ( 'N x ) ( 'N y ) ) )
                                    ) ) ) ) )
                                       ( => ( \A ( \l x ( =>
                                          ( & ( x . ) ( \A ( \l y ( =>
                                             ( & ( naturalna y ) ( x y ) )
                                             ( x ( 'N y ) )
                                          ) ) ) )
                                          ( \A ( \l y ( => ( naturalna y ) ( x y ) ) ) )
                                       ) ) )
                                          ( =>  ( \E + )
                                             ( => ( \A ( \l x ( => ( naturalna x ) ( = x ( + . x) ) ) ) )
                                                ( => ( \A ( \l x ( \A ( \l y ( => 
                                                   ( & ( naturalna x ) ( naturalna y ) )
                                                   ( = ( + ( 'N y ) x  ) ( 'N ( + y x ) ) )
                                                ) ) ) ) )
                                                   ( => ( \E * )
                                                      ( => ( \A ( \l x ( => ( naturalna x ) ( = . ( * . x) ) ) ) )
                                                         ( => ( \A ( \l x ( \A ( \l y ( => 
                                                            ( & ( naturalna x ) ( naturalna y ) )
                                                            ( = ( * ( 'N y ) x  ) ( + x ( * y x ) ) )
                                                         ) ) ) ) )
                                                            ( = ( 'N ( 'N ( 'N ( 'N . ) ) ) ) ( + ( 'N ( 'N . ) ) ( 'N ( 'N . ) ) ) )
                                                         )
                                                      )
                                                   )
                                                )
                                             )
                                          )
                                       )
                                    )
                                 )
                              )
                           )
                        )
                     )
                  )
               )
            )
         )
      )
   )
) )

Można by oczywiscie trochę krócej.