Аннотация:
В декабре 2021 г. Харви Фридман [1] сформулировал несколько вопросов, касающихся теории IOpen (расширения арифметики Робинсона Q схемой индукции по бескванторным формулам) и некоторых её фрагментов. Фридман рассматривал следующие теории:
I(lit): Q + индукция по атомарным формулам и их отрицаниям (литералам);
I(=): Q + индукция по формулам вида s = t, для любых термов s,t;
I(not =), I(<=) определяются аналогично.
Вот некоторые из поставленных задач:
1) Верно ли, что IOpen строго содержит I(lit)?
2) Какие отношения включения выполнены между сформулированными выше теориями?
3) Какие интересные математические теоремы могут быть эквивалентны I(lit) над Q?
Мы докажем, что ответ на первый вопрос отрицательный, установим практически все отношения из второго вопроса и докажем, что I(lit) не является конечно аксиоматизируемой теорией (что указывает на отсутствие ожидаемого ответа на вопрос из п. 3). Также мы рассмотрим некоторые другие вопросы, связанные с этими теориями.
[1] H. Friedman. 919: Proof theory of arithmetic/2. FOM posting, 12 Dec. 2021.
Обратная связь: