Ю. Г. Кудряшов планирует провести 4 занятия.
Доступны 4 видеозаписи курса.
Принцип исключенного третьего говорит, что любое утверждение либо истинно, либо ложно.
В этом курсе мы откажемся от принципа исключенного третьего. Мы не сможем ни доказывать от противного, ни перебирать случаи. Зато все наши доказательства будут в каком-то смысле конструктивны: доказательство существования объекта всегда можно будет превратить в компьютерную программу, которая строит этот объект.
На практике конструктивные доказательства полезнее неконструктивных. Например,
если вы хотите доказать, что у вас дома есть ключи, конструктивное
доказательство
Я расскажу о некоторых утверждениях конструктивной математики и о её связи с компьютерными системами доказательств.
Для понимания курса желательно уметь работать с логическими формулами вроде $$\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$). Кроме того, может быть полезно (но это не обязательно) знать определение действительных чисел и какую-нибудь аксиоматику формальной логики.