Многие согласятся, что математика изучает формальные факты. Сложнее определить,
что такое формальный факт и какие методы изучения правильные. До какого-то
момента допустимость методов устанавливалась интуитивно. Но для избежания
противоречий, для доказательства недоказуемости, а также для алгоритмической
проверки некоторых утверждений полезно сформулировать, о каком формализме идёт
речь. Обсуждением вариантов этого мы и займёмся.
Примерные темы курса.
- Формальные утверждения и формальные рассуждения. Важность мелочей. Выразимость
и невыразимость понятий на основе заданных свойств. Исчисление высказываний по
привычным правилам рассуждений, интуиционизм, генценовское исчисление
секвенций. Исчисление Ламбека (как интерпретировать эксперименты лингвистов
как доказательства алгебраических фактов).
- Доказуемость и недоказуемость. Консервативные расширения —
меняет ли добавление новых понятий свойства старых? Равнонепротиворечивость:
теории говорят совсем о разном, но ерунды в них доказуемо поровну.
- Выразимость, истинность и доказуемость. Невыразимость истины и недоказуемость
некоторых истин.
- Зачем себя ограничивать? Теория множеств и избежание противоречий. Устранение
кванторов (в слабых теориях). Более сложные случаи разрешимости теорий.
Проверяемые утверждения в неразрешимых теориях.
Курс предполагается доступным школьникам (хотя в правдивость некоторых
примеров придётся поверить на слово); с другой стороны, я постараюсь, чтобы
для студентов (не изучавших логику сверх общей программы) было новым более
половины рассказанного.
