перевод Фридмана

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

Определение

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

Приложение

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

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

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

См. также

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