フリードマン翻訳

数理論理学において、フリードマン変換は直観主義 の公式の特定の変換である。とりわけ、これは古典数学のさまざまな第一階理論のΠ ⁰ ₂定理が直観主義数学の定理でもあることを示すために使用できる。これは発見者であるハーヴェイ・フリードマンにちなんで名付けられている。

AとB を直観主義式とし、 B の自由変数は A では量化されていないものとする。翻訳A Bは、A^の各原子部分式C をC ∨ Bに置き換えることによって定義される。翻訳の目的上、 ⊥ も原子式であると考えられるため、⊥ ∨ B ( Bと同等) に置き換えられる。 ¬ A はA → ⊥の省略形として定義されているため、 (¬ A ) ^B = A ^B → Bとなることに留意する。

フリードマン変換は、マルコフ規則の下での多くの直観主義理論の閉包を示し、部分的な保守性の結果を得るために使用できます。重要な条件は、論理の文が決定可能であり、直観主義理論と古典理論の非定量化定理が一致することです。 ${\displaystyle \Delta _{0}^{0}}$

例えば、Aがヘイティング算術（HA）で証明可能であれば、A ^BもHAで証明可能です。^[1]さらに、AがΣ0 ¹ _-式であれば、A ^BはHAではA ∨ Bと同等です。B = Aと設定すると、次のようになります。

• Heyting 算術は原始再帰マルコフ規則 (MP _PR ) の下で閉じています。つまり、式 ¬¬ A がHA で証明可能で、Aが Σ ⁰ ₁式である場合、Aも HA で証明可能です。
• ペアノ算術はヘイティング算術に対してΠ ⁰ _{2保存的です。つまり、ペアノ算術が Π} ⁰ ₂式Aを証明する場合、A はHA ですでに証明可能です。

• ゲーデル＝ゲンツェンの負の翻訳