Аннотация:
В продолжение доклада С. Л. Кузнецова будет рассказано о недавних результатах, касающихся инфинитарной логики действий $\mathrm{ACT}_\omega$ и ее расширения экспоненциальной модальностью. Сначала будет показано, как построить секвенции с «большими» доказательствами для самой инфинитарной логики действий и тем самым доказать, что замыкающий ординал оператора непосредственной выводимости в $\mathrm{ACT}_\omega$ равен $\omega^\omega$. После этого будут сформулированы результаты о нижней оценке сложности задачи выводимости в некоторых расширениях $\mathrm{ACT}_\omega$. Интерес к этим результатам связан с тем, что возникающие сложностные классы принадлежат гиперарифметической иерархии. На первом из двух докладов планируется дать введение в гиперарифметическую иерархию, в частности, определить полное множество, которое будет использоваться для доказательства нижних оценок. Основное описание конструкции, вероятно, будет представлено уже на втором докладе 20 марта.
|
