x, y, z

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

Юрий Кудряшов

Комментарии: 0
Часть 1

Часть 2

Часть 3

Часть 4

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

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

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

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

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

$\forall\varepsilon>0\ \exists N\in\mathbb{N}\ \forall m,n>N\ |a_m-a_n|<\varepsilon$

(для любого положительного $\varepsilon$ найдётся натуральное $N$, такое что для $m,n>N$ модуль разности $a_m-a_n$ меньше $\varepsilon$).

Кроме того, может быть полезно (но это не обязательно) знать определение действительных чисел и какую-нибудь аксиоматику формальной логики.

Кудряшов Юрий Георгиевич
Летняя школа «Современная математика», г. Дубна
24-27 июля 2017 г.
Комментарии: 0