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

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

Определение

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

Заявление

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

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

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

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

Примечания

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