Алфавитом называется произвольное множество. Его элементы называются символами. Произвольная конечная последовательность символов называется словом. Слово может быть пустым.

Исчисление высказываний L определяется следующим образом:

Его алфавит состоит из символов , называемых логическими, и из символов, принадлежащих произвольному множеству Р, называемых нелогическими символами или буквами.

Синтаксис исчисления L определяется с помощью наименьшего подмножества S множества слов, такого, что

1) Р S;

2) Если  AS  и  BS , то   AS  и   (AB)  S.

Элементы множества  S  называются  (пропозициональными) формулами. Таким образом, формулами называются  слова, определяемые по индукции с помощью правил 1 – 2 из логических и нелогических символов.

Аксиомами исчисления L называются формулы:

(A1)      A(BA),

(A2)      (A (BC))  ((AB)  (AC)),

(A3)      (BA)  ((BA) B).

Здесь A, B, C – произвольные формулы. Поэтому в действительности мы имеем бесконечное множество аксиом, в каждой из групп A1, A2 и A3.

Правилом вывода Modus Ponens называется множество троек формул (A,AB,B), которое позволяет паре формул (A,AB) поставить в соответствие формулу B, называющуюся непосредственным следствием этих формул. Правило вывода Modus Ponens обозначается через MP и записывается, как

  MP

Формула A называется выводимой в исчислении L из формул X₁, X₂, …, X_k, если существует последовательность формул:  A₁, A₂, A₃, …, A_n,  такая, что для каждого  формула A_i является либо аксиомой исчисления L, либо элементом множества {X₁,  …,  X_k} , либо непосредственным следствием формул A_p и A_q, при некоторых 1  p, q  i-1. В этом случае последовательность: A₁, A₂, A₃, …, A_n  называется выводом формулы  A. Для обозначения выводимости формулы  A  в исчислении  L  из формул X₁, …, X_k применяется запись:

X₁, X₂, …, X_{k    L}   A .

Если для вывода формулы A достаточно аксиом, то А называется теоремой теории L, а выводимость из пустого множества формул записывается, как 

 _L А .

Лемма.  Имеет место теорема    _L  АА.

Доказательство. Построим вывод формулы АА из аксиом (А1) – (А3) следующим образом:

А₁ будет аксиомой (А2) для формул А, B = (АА), С = А;

А₂ будет аксиомой (А1) для формул А, В = (АА);

получим:

А₁=(А ((АА) А)) ((А(АА)) (АА)),

А₂=А((АА) А).

Применяя правило вывода   MP , будем иметь непосредственное следствие формул  A₂  и A₁:

А₃=(А(АА)) (АА).

Следующая формула получается из аксиомы  (А1) подстановкой В = А:

А₄=А(АА).

Применяя правило вывода MP, получим:

А₅ = АА.

Последовательность формул:  A₁, A₂, A₃, А₄, А₅ = (АА) является искомым выводом формулы АА.