Лектор: Кузнецов Степан Львович (д.ф.-м.н., в.н.с., Математический институт им. В.А. Стеклова РАН, г. Москва)
Даты: Пожалуйста, обратите внимание, что указано время в Новосибирске.
17 ноября 2025 г. (понедельник), 16:20-17:55
20 ноября 2025 г. (четверг), 16:20-17:55
21 ноября 2025 г. (пятница), 16:20-17:55
Аннотация:
Для аксиоматизации некоторых логик не хватает систем с конечными доказательствами, и используются доказательства бесконечные (инфинитарные). Бесконечные доказательства бывают "широкие" и "высокие". В первых используются правила с бесконечным числом (омега-правила), но при этом любой путь от целевой формулы вверх по дереву вывода конечен. Во вторых, наоборот, правила имеют конечное число посылок, зато допускаются, с определёнными ограничениями, бесконечные ветви вывода. Это соответствует идее бесконечного спуска, а если такой нефундированный вывод оказывается периодическим (циклическим), - то той или иной форме принципа индукции. В рамках мини-курса мы обсудим системы с бесконечными доказательствами для двух семейств неклассических логик - модальных логик с модальностями доказуемости и с модальностями транзитивного замыкания и субструктурных логических систем с итерацией Клини.