ИСТИНА |
Войти в систему Регистрация |
|
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
В проекте рассматривается ряд актуальных вопросов в области формальной арифметики и теории доказательств. Первый из них посвящен исследованию новых естественных вариантов схем рефлексии для арифметических теорий, связанных с теоретико-модельным понятием определимого элемента, а также соотношений между этими схемами и другими близкими к ним формами рефлексии, непротиворечивости и индукции. Новые принципы позволят по-другому взглянуть на связь между теоретико-модельными и синтаксическими доказательствами результатов о консервативности, а также расширят набор средств для выразимости одних принципов и схем через другие. Второй вопрос связан с одной из центральных открытых проблем в области логики доказуемости, а именно, с проблемой изоморфизма алгебр доказуемости формальных теорий. В рамках проводимого исследования предполагается построить ряд новых примеров пар теорий с неизоморфными алгебрами доказуемости, исследовать вопрос об изоморфизме для П_1-аксиоматизированных расширений исходной теории и тем самым усилить имеющиеся результаты об изоморфизмах алгебр доказуемости, приблизив друг к другу существующие необходимые и достаточные условия изоморфизма таких алгебр. Помимо этого планируется исследовать возможность обобщения этих результатов на случай полимодальных алгебр доказуемости, получаемых в результате обогащения алгебр доказуемости операторами, индуцируемыми на ней сильными предикатами доказуемости.
The aim of this project is to study several topical questions in proof theory and formal arithmetic. The first is devoted to the investigation of new natural variants of reflection principles for arithmetical theories related to the model-theoretic notion of definable element, as well as the relationship between these schemata and other similar forms of reflection, consistency and induction. The new principles will provide different perspective on the relationship between model-theoretic and syntactic proofs of conservativity results, and also expand the set of tools to express one principles and schemata in terms of another. The second question is related to one of the central open problems in the field of provability logic, namely, the isomorphism problem for provability algebras of formal theories. As a part of this study it is expected to construct a new series of examples of pairs of theories with non-isomorphic provability algebras, to investigate the isomorphism problem for П_1-axiomatized extensions of arithmetical theories and thereby to strengthen the existing results on isomorphisms of provability algebras, reducing the gap between the necessary and sufficient conditions for the isomorphism of such algebras. In addition, it is planned to investigate the possibility of generalizing these results to the case of polymodal provability algebras, obtained by expanding provability algebras with the operators, induced by the strong provability predicates.
В результате исследований предполагается получить характеризацию схем локальной омега-непротиворечивости в терминах схем локальной и равномерной рефлексии для арифметической теории, что позволит получить результат о невыводимости схемы омега-непротиворечивости (и её ограниченных вариантов) из схемы локальной рефлексии для широкого класса арифметических теорий. Планируется ввести естественные аналоги схем индукции с определимыми параметрами для схем рефлексии, а именно, схемы равномерной рефлексии с Sigma_n-определимыми параметрами, доказать эквивалентность этих схем соответствующим схемам локальной рефлексии, а также выразить с их помощью указанные выше схемы индукции. С помощью этих новых принципов предполагается дать новое теоретико-модельное доказательство консервативности схемы равномерной рефлексии над схемой локальной рефлексии, а также лучше понять связь между теоретико-модельными и синтаксическими доказательствами результатов о консервативности. В исследованиях, связанных с алгебрами доказуемости, предполагается существенно расширить имеющийся набор примеров пар теорий с неизоморфными алгебрами и понизить границу из теоремы Шаврукова о неизоморфизме с равномерной Sigma_1-рефлексии до локальной Sigma_1-рефлексии. Предполагается выяснить, применимо ли достаточное условие неизоморфизма Адамссона к парам теорий вида T и U, где U есть П_1-аксиоматизированное расширение T. В перспективе планируется приблизить друг к другу имеющиеся необходимые и достаточные условия изоморфизма, тем самым усилив имеющиеся результаты. Для полимодальных алгебр доказуемости, предполагается обобщить теорему Шаврукова об изоморфизме, а также построить новые примеры пар теорий с неизоморфными полимодальными алгебрами доказуемости, но изоморфными алгебрами доказуемости.
Л. Д. Беклемишевым получен ряд важных результатов в области теории доказательств, формальной арифметики и логики доказуемости. Доказана теорема о классификации пропозициональных логик доказуемости. Получена характеризация ограниченных правил индукции в арифметике в терминах итерированных схем рефлексии. Найдены классы доказуемо тотальных вычислимых функций для фрагментов арифметики с беспараметрической индукцией. Предложен подход к ординальной теории доказательств на основе понятия алгебры доказуемости. Этот абстрактный алгебраический подход позволяет по новому взглянуть на ряд классических результатов в теории доказательств. В частности, из алгебры доказуемости для элементарной арифметики можно каноническим образом извлечь естественную систему обозначений для ординала epsilon_0 и на этой основе получить новое доказательство непротиворечивости арифметики Пеано с помощью трансфинитной индукции (теорему Генцена). Изучение алгебр доказуемости позволило также дать естественную характеризацию класса доказуемо тотальных вычислимых функций арифметики Пеано и привело к новым простым примерам утверждений комбинаторного характера, не выводимым в арифметике Пеано. Е. А. Колмаковым совместно с Л. Д. Беклемишевым исследовано понятие доказуемой n-доказуемости. Множества доказуемо n-доказуемых предложений для различных фрагментов арифметики охарактеризованы в терминах итерированных схем локальной рефлексии. По результатам работы опубликована статья: E. Kolmakov, L. Beklemishev. Axiomatization of provable n-provability. Journal of Symbolic Logic, 84 (2):849-869, 2019. На этой основе предложены новые подходы для построения примеров теорий с неизморофными бимодальными алгебрами доказуемости.
грант РФФИ |
# | Сроки | Название |
1 | 1 октября 2019 г.-31 декабря 2019 г. | Схемы рефлексии и алгебры доказуемости |
Результаты этапа: |
Для прикрепления результата сначала выберете тип результата (статьи, книги, ...). После чего введите несколько символов в поле поиска прикрепляемого результата, затем выберете один из предложенных и нажмите кнопку "Добавить".