Logiczny zapis matematyki

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

( = ~ ( \l x ( ani x x ) ) )
( = i ( \l x ( \l y ( ani ( ~ x ) ( ~ y ) ) ) ) )
( = lub ( \l x ( \l y ( ~ ( ani  x y ) ) ) ) )
( = \A ( \l y ( ~ ( \V ( \l x ( ~ ( y x ) ) ) ) ) )