Logiczny zapis matematyki

Z Conlanger
Wersja z dnia 19:48, 24 maj 2009 autorstwa BartekChom (dyskusja | edycje) (Utworzył nową stronę „Częścią logicznego języka jest zapis matematyczny. W jednej z wersji: Używa się 84 znaków (dostępnych bezpośrednio z klawiatury): <pre> a ...”)
(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
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
a\b 0 1
0
1

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