WikiDer > Перевод Фридмана

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

Определение

Позволять А и 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.

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

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

Примечания