Между бессмыслицей и непознаваемым. Что мы можем сформулировать, проверить, доказать, занятие 1

Многие согласятся, что математика изучает формальные факты. Сложнее определить, что такое формальный факт и какие методы изучения правильные. До какого-то момента допустимость методов устанавливалась интуитивно. Но для избежания противоречий, для доказательства недоказуемости, а также для алгоритмической проверки некоторых утверждений полезно сформулировать, о каком формализме идёт речь. Обсуждением вариантов этого мы и займёмся.
Примерные темы курса.

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

Курс предполагается доступным школьникам (хотя в правдивость некоторых примеров придётся поверить на слово); с другой стороны, я постараюсь, чтобы для студентов (не изучавших логику сверх общей программы) было новым более половины рассказанного.