Схемы рефлексии в формальной арифметике

Настоящая диссертация посвящена исследованию схем рефлексии для фрагментов формальной арифметики Пеано и применению этих схем к вопросам сравнения и классификации арифметических теорий.

Схемы рефлексии возникли в математической логике вскоре после доказательства Гёделем его фундаментальных теорем о неполноте [17]. 1 Для данной теории Т эти схемы представляют собой варианты формализации утверждения «если формула (р доказуема в Т, то (р истинна». Они дают примеры истинных, но недоказуемых утверждений, обобщающих первый известный пример такого рода — гёделевскую формулу непротиворечивости теории Т.

Тьюринг [43] ввёл в рассмотрение прогрессии теорий, получаемые итерированием процесса пополнения теории схемой рефлексии, и предложил возможный подход к ординальной классификации арифметических теорий на основе таких прогрессий. В дальнейшем этот подход был проанализирован и развит Феферманом в [15]. Построенные Тьюрингом и Феферманом примеры показали, что на пути подобной классификации встают существенные трудности, связанные с проблемой канонического выбора итерированных схем рефлексии и связанным с ней вопросом о естественном представлении ординалов в арифметике.

Крайзель и Леви в [20] показали, что схемы рефлексии являются удобным инструментом для изучения вопросов сложности аксиоматизации формальных теорий. Ими была доказана дедуктивная эквивалентность так называемой равномерной схемы рефлексии для примитивно рекурсивной арифметики и полной схемы индукции, откуда, в частности, вытекает невозможность задания арифметики Пеано множеством аксиом ограниченной кванторной сложности. В этой же работе была доказана эквивалентность схемы трансфинитной индукции до ординала со и равномерной схемы рефлексии для арифметики Пеано. В дальнейшем были установлены тесные связи между схемами рефлексии и другими истинными невыводимыми утверждениями, включая известные комбинаторные принципы Париса-Харрингтона.

В диссертации получено решение ряда важных вопросов о схемах рефлексии, что позволило сделать аппарат этих схем универсальным.

1 Схемы рефлексии появились впервые, по-видимому, в работе Россера 1937 г. [34]. При этом Россер ссылается на неопубликованные результаты Клини, рассмотревшего в 1935 г. вариант логического правила, эквивалентный, в современной терминологии, равномерной схеме рефлексии (см. ниже § 2.1). инструментом анализа и ординальной классификации арифметических теорий. Описание исследуемой теории в терминах схем рефлексии позволяет использовать свойства таких схем для получения разнообразных результатов о её строении и соотношении с другими теориями, в частности, результатов о независимости, аксиоматизируемости, (частичной) консервативности и характеризации классов доказуемо тотальных вычислимых функций.

Одно из наиболее активно развивающихся в последнее время направлений математической логики связано с изучением подсистем, или фрагментов, формальной арифметики Пеано РА. Интерес к этим вопросам был вызван прежде всего обнаружившимися связями с теорией сложности вычислений и попытками формализации понятия эффективного (feasible) доказательства. Монография [18] содержит накопленные в этой области к 1993 году основные результаты и обширную библиографию.

В настоящей работе подход, основанный на схемах рефлексии, применён к исследованию иерархий фрагментов РА. Изучены взаимосвязи схем рефлексии и основных форм индукции ограниченной арифметической сложности. Как следствие получен ряд новых результатов, относящихся к иерархиям фрагментов РА, определяемых правилом индукции и схемой индукции без параметров ограниченной арифметической сложности.

К основным результатам диссертации можно отнести следующие.

1) Точная характеризация правил индукции ограниченной арифметической сложности в терминах схем рефлексии (теоремы 2, 3, 4 диссертации) .

Существенной чертой полученной характеризации является её инвариантность, то есть независимость от выбора базисной теории достаточно широкого класса, над которой эти правила рассматриваются. В частности, это позволяет получить естественную аксиоматизацию с помощью схем аксиом замыканий произвольных достаточно сильных арифметических теорий относительно правил индукции (следствия 3.16, 3.18 и 5.24).

2) Точная характеризация схем беспараметрической индукции ограниченной арифметической сложности в терминах схем рефлексии (теорема 5).

Возникающие при этом так называемые локальные схемы рефлексии в простейшем случае были известны еще со времени работы Тьюринга. Однако, их связь с фрагментами РА или другими формальными системами, определяемыми независимым образом, ранее не была известна.

3) Детально изучено строение иерархии локальных схем рефлексии над произвольной достаточно сильной арифметической теорией. В частности, получены оптимальные в смысле арифметической сложности результаты о консервативности для этой иерархии (теорема 1), а также результаты о связи равномерной и локальной схем рефлексии (теорема 6, предложения 6.27 и 6.28).

Вместе с результатами 2) это позволяет дать ответ на ряд вопросов о схемах беспараметрической индукции в арифметике, а также получить новое конструктивное доказательство некоторых результатов об этих схемах, для которых ранее было известно лишь неконструктивное теоретико-модельное доказательство.

4) Получен ответ на стоявший в области фрагментов арифметики вопрос о доказуемо тотальных вычислимых функциях теории, аксиоматизируемой схемой индукции для Пг-формул без параметров. Показано, что класс таких функций совпадает с примитивно рекурсивными функциями (следствие 6.9). Расширение этой теории схемой индукции для Егформул с параметрами имеет более широкий класс доказуемо тотальных вычислимых функций, совпадающий с классом дважды рекурсивных функций в смысле Р. Петер (предложение 7.29). Эти результаты, по-видимому, являются наиболее интересными приложениеми результатов 2) и 3).

5) Построение иерархий итерированных схем рефлексии с естественными свойствами, позволяющее обобщить на такие схемы результаты о консервативности из 3). В частности, показано, что для таких иерархий, а раз итерированная схема локальной рефлексии, где, а — конструктивный ординал, доказывает те же Пх-предложения, что и иа раз итерированное утверждение о непротиворечивости (теорема 7).

В отличие от традиционного подхода, связанного с ординальными границами доказуемости трансфинитной индукции в формальных теориях (см., например, [29]), изложенный в диссертации подход дает более тонкую классификацию, позволяющую различить теории уже на уровне их Последствий. На основе этого подхода получено обобщение на более широкий класс теорий теоремы Шмерля [35] о тонкой структуре иерархии итерированных схем равномерной рефлексии над примитивно рекурсивной арифметикой и вычислены ординалы основных фрагментов РА (теорема 8, следствие 7.25). Также получены обобщения результатов 4) на схемы беспараметрической индукции арифметической сложности Пп для произвольного п > 2 (предложение 7.29).

Применяемые в диссертации методы можно разделить на три группы. К первой группе относятся широко известные методы структурной теории доказательств, используемые при получении характеризаций 1) и 2), такие как техника устранения сечения и сколемизация. Отметим, что применяемый нами для анализа правила Еп-индукции вариант техники сколемизации является усовершенствованием техники «операторных теорий» работы [37].

Ко второй группе относится нетрадиционная техника, используемая для анализа схем локальной рефлексии. Ключевую роль здесь играет логика доказуемости и связанные с ней модели Крипке. Первые применения подобной техники к анализу схем рефлексии содержатся в работах [11, 1].

Наконец, подход, предлагаемый нами для построения иерархий итерированных схем рефлексии, использует некоторые идеи работ [15, 35]. Введенное в диссертации понятие гладкой прогрессии теорий позволяет существенно упростить построение итерированных схем рефлексии, делая ненужным использование языка теории рекурсии и его формализации в арифметике, а также использование так называемых фундаментальных последовательностей ординальных обозначений. При этом достигается большая общность результатов и, в некотором смысле, каноничность определяемых посредством этой конструкции схем.

1 Основные понятия.

1. С. Н. Артёмов. Расширения арифметики и модальные логики. Канд. дисс., Математический институт им. В. А. Стеклова РАН, Москва, 1979.

2. С. Н. Артёмов. Приложения модальной логики в теории доказательств. В сб. Вопросы кибернетики. Неклассические логики и их применения, стр. 3−20. Наука, Москва, 1982.

3. C.B. Горячев. Об интерпретируемости некоторых расширений арифметики. Математические заметки, 40:561−572, 1986.

4. Н. Катленд. Вычислимость.

Введение

в теорию рекурсивных функций. Мир, Москва, 1983. Пер. с англ. под ред. С. Ю. Маслова.

5. Г. Е. Минц. Бескванторные и однокванторные системы. Зап. науч. семинаров ЛОМИ, 20:115−133, 1971.

6. A.A. Мучник. О двух подходах к классификации рекурсивных функций. В сб. Проблемы математической логики: сложность алгоритмов и классы вычислимых функций, под ред. A.A. Мучника и В. А. Козмидиади, стр. 123−138. МИР, Москва, 1970.

7. В. П. Оревков. Нижние оценки увеличения сложности выводов после устранения сечений. Записки науч. сем. ЛОМИ, 88:137−162, 1979.

8. Р. Петер. Рекурсивные функции. ИЛ, Москва, 1954.

9. К. Сморинский. Теоремы о неполноте. В сб. Справочная книга по математической логике, под ред. Дж. Барвайса, т. 4 «Теория доказательств», стр. 9−53. Москва, Наука, 1983.

10. X. Швихтенберг. Теория доказательств: некоторые приложения устранения сечения. В сб. Справочная книга по математической логике, под ред. Дж. Барвайса, т. 4 «Теория доказательств», стр. 54−83. Москва, Наука, 1983.

11. G. Boolos. Reflection principles and iterated consistency assertions. Journal of Symbolic Logic, 44:33−35, 1979.

12. G. Boolos. The Logic of Provability. Cambridge University Press, Cambridge, 1993.

13. W. Buchholz and S. Wainer. Provably computable functions and the fast growing hierarchy. In Contemporary Math. 65, pages 179−198, 1987.

14. S. Feferman. Arithmetization of metamathematics in a general setting. Fundamenta Mathematicae, 49:35−92, 1960.

15. S. Feferman. Transfinite recursive progressions of axiomatic theories. Journal of Symbolic Logic, 27:259−316, 1962.

16. H. Gaifman and C. Dimitracopoulos. Fragments of Peano’s arithmetic and the MDRP theorem. In Logic and algorithmic (Zurich, 1980), (Monograph. Enseign. Math., 30), pages 187−206. Geneve, University of Geneve, 1982.

17. K. Godel. Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I. Monatshefte fur Mathematik und Physik, 38:173−198, 1931.

18. P. Hajek and P. Pudlak. Metamathematics of First Order Arithmetic. Springer-Verlag, Berlin, 1993.

19. R. Kaye, J. Paris, and C. Dimitracopoulos. On parameter free induction schemas. Journal of Symbolic Logic, 53(4):1082−1097, 1988.

20. G. Kreisel and A. Levy. Reflection principles and their use for establishing the complexity of axiomatic systems. Zeitschrift f. math. Logik und Grundlagen d. Math., 14:97−142, 1968.

21. D. Leivant. The optimality of induction as an axiomatization of arithmetic. Journal of Symbolic Logic, 48:182−184, 1983.

22. P. Lindstrom. On partially conservative sentences and interpretability. Proceedings of the AMS, 91(3):436−443, 1984.

23. M.H. Lob. Solution of a problem of Leon Henkin. Journal of Symbolic Logic, 20:115−118, 1955.

24. M.H. Lob and S.S. Wainer. Hierarchies of number-theoretic functions. Archive for Mathematical Logic, 13:39−51, 97−113, 1970.

25. H. Ono. Reflection principles for fragments of arithmetic. Zeitschrift f. math. Logik und Grundl, d. Math., 33(4):317−333, 1987.

26. C. Parsons. Hierarchies of primitive recursive functions. Zeitschrift f. math. Logik und Grundlagen d. Math., 14(4):357−376, 1968.

27. C. Parsons. On a number-theoretic choice schema and its relation to induction. In A. Kino, J. Myhill, and R.E. Vessley, editors, Intuitionism and Proof Theory, pages 459−473. North Holland, Amsterdam, 1970.

28. C. Parsons. On n-quantifier induction. Journal of Symbolic Logic, 37(3) :466—482, 1972.

29. W. Pohlers. Proof Theory. An Introduction. Lecture Notes in Mathematics 1407. Springer-Verlag, Berlin, 1989.

30. L.J. Pozsgay. Godel’s Second Theorem for Elementary Arithmetic. Zeitschrift f. math. Logik und Grundlagen d. Math., 14:67−80, 1968.

31. J.W. Robbin. Subrecursive hierarchies. PhD thesis, Princeton University, Princeton, 1965.

32. H.E. Rose. Subrecursion: Functions and Hierarchies. Clarendon Press, Oxford, 1984.

33. J. Rosenstein. Linear Orderings. Academic Press, New York, 1982.

34. J.B. Rosser. Godel Theorems for non-constructive logics. Journal of Symbolic Logic, 2:129−137, 1937.

35. U.R. Schmerl. A fine structure generated by reflection formulas over Primitive Recursive Arithmetic. In M. Boffa, D. van Dalen, and K. McAloon, editors, Logic Colloquium'78, pages 335−350. North Holland, Amsterdam, 1979.

36. H. Schwichtenberg. Rekursionszahlen und die Grzegorczyk-Hierarchie. Archive for Mathematical Logic, 12:85−97, 1969.

37. W. Sieg. Fragments of arithmetic. Annals of Pure and Applied Logic, 28:33−71, 1985.

38. W. Sieg. Herbrand analyses. Archive for Mathematical Logic, 30:409 441, 1991.

39. C. Smoryriski. Self-Reference and Modal Logic. Springer-Verlag, Berlin, 1985.

40. R. Sommer. Ordinal arithmetic in IA q. In P. Clote and J. Krajicek, editors, Arithmetic, Proof theory, and Computational complexity, pages 320−363. Oxford University Press, 1992.

41. R. Sommer. Transfinite induction within Peano arithmetic. Annals of Pure and Applied Logic, 76(3):231−289, 1995.

42. R. Statman. Bounds for proof-search and speed-up in the predicate calculus. Annals of Mathematical Logic, 15:225−287, 1978.

43. A.M. Turing. System of logics based on ordinals. Proc. London Math. Soc., ser. 2, 45:161−228, 1939.

44. A. Visser. The formalization of interpretability. Studia Logica, 50(1):81−106, 1991.

45. A. Wilkie and J. Paris. On the scheme of induction for bounded arithmetic formulas. Annals of Pure and Applied Logic, 35:261−302, 1987. Работы автора по теме диссертации.

46. Л. Д. Беклемишев. Независимые нумерации теорий и рекурсивных прогрессий. Сибирский математический журнал, 33(5):22−46, 1992.

47. Л. Д. Беклемишев. Об ограниченном правиле индукции и итерированных схемах рефлексии над кальмаровской элементарной арифметикой. В сб. Теоретические и прикладные аспекты математических исследований, под ред. О. Б. Лупанова. Москва, МГУ, 1994, стр. 36−39.

48. L.D. Beklemishev. On bimodal logics of provability. Annals of Pure and Applied Logic, 68:115−160, 1994.

49. L.D. Beklemishev. Iterated local reflection versus iterated consistency. Annals of Pure and Applied Logic, 75:25−48, 1995.

50. L.D. Beklemishev. Notes on local reflection principles. Logic Group Preprint Series 133, University of Utrecht, 1995, 8 p.

51. L.D. Beklemishev. Remarks on Magari algebras of PA and /A0 + EXP. In Logic and Algebra, P. Agliano, A. Ursini, eds., pages 317−325. Marcel Dekker, New York, 1996.

52. L.D. Beklemishev. Induction rules, reflection principles, and provably recursive functions. Annals of Pure and Applied Logic, 85:193−242, 1997.

53. L.D. Beklemishev. Parameter free induction and reflection. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Computational Logic and Proof Theory. Lecture Notes in Computer Science 1289. SpringerVerlag, Berlin, 1997, pp. 103−113.

54. L.D. Beklemishev. A proof-theoretic analysis of collection. Archive for Mathematical Logic, 34(4−5) :216−238, 1998.