Перевод Фридмана - Friedman translation

В математическая логика, то Перевод Фридмана это некая трансформация интуиционистский формулы. Среди прочего его можно использовать, чтобы показать, что Π⁰₂ -теоремы различных теории первого порядка классической математики - это также теоремы интуиционистской математики. Он назван в честь его первооткрывателя, Харви Фридман.

Определение

Позволять А и B быть интуиционистскими формулами, где нет свободной переменной B количественно оценивается в А. Перевод А^B определяется заменой каждой атомарной подформулы C из А к C ∨ B. Для целей перевода ⊥ также считается атомарной формулой, поэтому ее заменяют на ⊥ ∨ B (что эквивалентно B). Обратите внимание, что ¬А определяется как сокращение от А → ⊥, следовательно (¬А)^B = А^B → B.

Заявление

Перевод Фридмана может быть использован для демонстрации того, что многие интуиционистские теории закрыты. Правило Маркова, и получить частичная консервативность полученные результаты. Ключевым условием является то, что ${displaystyle Delta _{0}^{0}}$ предложения логики разрешимы, что позволяет неквантифицированным теоремам интуиционистской и классической теорий совпадать.

Например, если А доказуемо в Арифметика Гейтинга (HA), то А^B также доказуемо в HA.^[1] Более того, если А это Σ⁰₁-формула, тогда А^B в HA эквивалентно А ∨ B. Это означает, что:

• Арифметика Гейтинга замыкается примитивно рекурсивным правилом Маркова (MP_PR): если формула ¬¬А доказуемо в HA, где А является Σ⁰₁-формула, то А также доказуемо в HA.
• Арифметика Пеано является Π⁰₂-консервативен по арифметике Гейтинга: если арифметика Пеано доказывает⁰₂-формула А, тогда А уже доказуемо в HA.

Смотрите также

• Негативный перевод Гёделя – Гентцена

Примечания

1. Харви Фридман. Классически и интуиционистски доказуемо рекурсивные функции. В Скотт, Д. С. и Мюллер, Г. Х. Редакторы, Высшая теория множеств, том 699 конспектов лекций по математике, Springer Verlag (1978), стр. 21–28. Дои:10.1007 / BFb0103100