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

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

Ю. Г. Кудряшов планирует провести 4 занятия.

Доступны 4 видеозаписи курса.

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

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

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

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

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

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

Другой пример: чтобы конструктивно доказать, что последовательность стремится к нулю, надо научиться по числу ε>0 предъявлять номер, начиная с которого все члены последовательности лежат в интервале (−ε,ε).

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

Для понимания курса желательно уметь работать с логическими формулами вроде

∀ε>0∃N∈N∀m,n>N|am−an|<ε

(для любого положительного  ε найдётся натуральное N, такое что для m, n>N модуль разности am−an меньше ε). Кроме того, может быть полезно (но это не обязательно) знать определение действительных чисел и какую-нибудь аксиоматику формальной логики.

Organization Committee e-mail:
dubna@mccme.ru