Logiczny zapis matematyki

Z Conlanger
Przejdź do nawigacji Przejdź do wyszukiwania

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 ) ) ) ) )
  • alternatywę
( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
  • kwantyfikator wielki - działa na funkcje
( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )
  • istnienie
( = \E ( \l y ( \V ( \l x ( = x y ) ) ) ) )

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

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

Wstawiamy je do poprzedniego wielkiego zdania

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

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

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

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

Definicja dodawania:

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

I mnożenia:

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

To znowu zbieramy

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

i wstawiamy do z poprzednimi załorzeniami:

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

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

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

A więc po wstawieniu

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

Można by oczywiscie trochę krócej.

Następny etap to zbiory.

Warto dorobić kilka definicji

( = nie ( \A ( \l x ( & x ( ~ x ) ) ) )
( = tak ( ~ nie ) )
( = albo ( \l x ( \l y ( ani ( ani x y ) ( & x y ) ) ) ) )
( = \V_ ( \l x ( \l y ( \V ( \l z ( & ( x z ) ( y z ) ) ) ) ) ) )
( = \A_ ( \l x ( \l y ( \V ( \l z ( => ( x z ) ( y z ) ) ) ) ) ) )

Oryginalnie założę, że nie wszystko jest zbiorem (ale elementy wszystkiego tworzą zbiór zbiorem).


( \E zbior )
( \E \w )
  • Aksjomat ekstensjonalności
( \A_ zbior ( \l x ( \A_ zbior ( \l y ( => ( \A ( \l z ( = ( \w x z ) ( \w y z ) ) ) ) ( = x y ) ) ) ) ) )
  • Aksjomat podzbioru (dla ( = y ( \l z tak ) ) mamy tworzenie zbioru)
( \A ( \l x ( \A ( \l y ( \A ( \l z ( = ( \w ( {f y x ) z ) ( & ( \w x z ) ( y z ) ) ) ) ) ) ) ) ) )
( \A_ zbior ( \l x ( \A ( \l y ( ( zbior ( {f y x ) ) ) ) ) ) )
  • aksjomat pary
( \A ( \l x ( \A ( \l y ( \ A ( \l z ( = ( \w ( {2 x y ) z ) ( lub ( = x z ) ( = y z ) ) ) ) ) ) ) ) )
( \A ( \l x ( \A ( \l y ( zbior ( {2 x y ) ) ) ) ) )
  • aksjomat sumy
( \A ( \l x ( \A ( \l y ( = ( \w ( \U x ) y ) ( \V_ ( \w x ) ( \l z ( \w z y ) ) ) ) ) ) ) )
( \A ( \l x ( zbior ( \U x ) ) ) )
  • aksjomat zbioru potęgowego
( = \c ( \l x ( \l y ( \A_ ( \w y ) ( \w x ) ) ) ) )
( \A ( \l x ( = ( \w ( \P x ) ) ( \c x ) ) ) )
( \A_ zbior ( \l x ( zbior ( \P x ) ) ) )
  • aksjomat nieskończoności
( = ( \w \N ) naturalna )
  • aksjomat zastępowania
( \A ( \l x ( \A ( \l y ( = ( \w ( {z y x ) ) ( \l z ( \V_ ( \w x ) ( \l t ( = ( y t ) ( z ) ) ) ) ) ) ) ) ) )
  • aksjomat regularności
  • aksjomat wyboru