В математической логике , то Friedman перевод определенная трансформация интуиционистских формул . Среди прочего, его можно использовать, чтобы показать, что Π 0 2 -теоремы различных теорий первого порядка классической математики также являются теоремами интуиционистской математики. Он назван в честь его первооткрывателя Харви Фридмана .
Определение
Пусть и Б быть интуиционистские формулы, где нет свободных переменная B не количественно A . Перевод Б определяется заменой каждого атомного подформульности C из A по C ∨ B . Для целей перевода ⊥ также считается атомарной формулой, поэтому она заменяется на ⊥ ∨ B (что эквивалентно B ). Обратите внимание , что ¬ определяется как сокращение для A → ⊥, следовательно , (¬ A ) B = A B → B .
Заявление
Перевод Фридмана можно использовать, чтобы показать закрытие многих интуиционистских теорий в соответствии с правилом Маркова и получить результаты частичной консервативности . Ключевым условием является то, что предложения логики разрешимы, что позволяет неквантифицированным теоремам интуиционистской и классической теорий совпадать.
Например, если A доказуемо в арифметике Гейтинга (HA), то A B также доказуемо в HA. [1] Кроме того, если является Σ 0 1 -формула , то Б в HA , эквивалентной A ∨ B . Это означает, что:
- Арифметика Гейтинга замкнута согласно примитивно-рекурсивному правилу Маркова (MP PR ): если формула ¬¬ A выводима в HA, где A - Σ 0 1 -формула, то A также выводима в HA.
- Арифметика Пеано Π 0 2 -консервативна по сравнению с арифметикой Гейтинга: если арифметика Пеано доказывает Π 0 2 -формулу A , то A уже доказуема в HA.
Смотрите также
Заметки
- ^ Харви Фридман. Классически и интуитивно доказуемо рекурсивные функции. В Скотт, Д.С. и Мюллер, GH Editors, Higher Set Theory, Volume 699 of Lecture Notes по математике, Springer Verlag (1978), стр. 21–28. DOI : 10.1007 / BFb0103100