Конструктивная математика. Занятие 1

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

«Вот они, на столе под стопкой бумаг»

полезнее неконструктивного

«Вчера я зашел с ними домой, и с тех пор никто из дома не выходил».

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