Юрий Георгиевич Кудряшов

Принцип исключенного третьего говорит, что любое утверждение либо истинно, либо ложно.

В этом курсе мы откажемся от принципа исключенного третьего. Мы не сможем ни доказывать от противного, ни перебирать случаи. Зато все наши доказательства будут в каком-то смысле конструктивны: доказательство существования объекта всегда можно будет превратить в компьютерную программу, которая строит этот объект.

На практике конструктивные доказательства полезнее неконструктивных. Например, если вы хотите доказать, что у вас дома есть ключи, конструктивное доказательство

«Вот они, на столе под стопкой бумаг» полезнее неконструктивного
«Вчера я зашел с ними домой, и с тех пор никто из дома не выходил». Другой пример: чтобы конструктивно доказать, что последовательность стремится к нулю, надо научиться по числу $\varepsilon\gt0$ предъявлять номер, начиная с которого все члены последовательности лежат в интервале $(-\varepsilon, \varepsilon)$.

Я расскажу о некоторых утверждениях конструктивной математики и о её связи с компьютерными системами доказательств.

Для понимания курса желательно уметь работать с логическими формулами вроде $$\forall \varepsilon > 0\,\exists N \in \mathbb{N}\,\forall m, n > N\,|a_m-a_n|\lt\varepsilon$$ (для любого положительного $\varepsilon$ найдётся натуральное $N$, такое что для $m, n>N$ модуль разности $a_m-a_n$ меньше $\varepsilon$). Кроме того, может быть полезно (но это не обязательно) знать определение действительных чисел и какую-нибудь аксиоматику формальной логики.