Алгебры доказуемости

Аксиоматические системы, такие как арифметика Пеано и теория множеств Цермело–Френкеля, были придуманы в начале XX века как строгая математическая модель понятия доказуемости. Такая модель нужна, если мы хотим установить недоказуемость того или иного утверждения из тех или иных аксиом. Её изучением занимается особое направление в математической логике — теория доказательств.
Первые примеры недоказуемых и неопровержимых элементарно-арифметических утверждений были обнаружены Гёделем. Однако вплоть до конца 1970-х годов все известные факты такого рода были получены либо путем арифметического кодирования некоторых утверждений из самой логики, либо относились к свойствам бесконечных множеств (наиболее известный пример — гипотеза континуума). В 1977 году Дж. Парис и Л. Харрингтон нашли первые примеры недоказуемых в арифметике Пеано естественных утверждений из конечной комбинаторики. С тех пор были обнаружены и другие подобные утверждения, однако до сих пор таких примеров известно сравнительно мало.
В докладе будет рассказано об одном простом варианте комбинаторного утверждения, независимого от аксиом арифметики, найденного докладчиком, а также об идеях, на которых он основан.
Эти идеи связаны с общим подходом к изучению аксиоматических систем с алгебраической точки зрения. Будут описаны алгебраические структуры, возникающие при изучении формальной доказуемости, и приведены некоторые применения этих структур к вопросу о порядках роста вычислимых функций в арифметике. Также будет рассказано о топологической точке зрения на алгебры доказуемости, которая приводит к изучению некоторого специфического класса «разреженных» пространств.
Специальных знаний по математической логике для понимания доклада не требуется.