直観主義の公式のための標準形式?

DNFs/CNFsとprenex normal
formは、一般に直観主義論理のためには存在しないことはよく知られている。

ILの数式正規化に関する素晴らしい結果はありますか?私はこれをグーグルで試してみましたが、結果はちょうど証明のための通常のフォームについてのものになります。

ベストアンサー

あなたがこれを取ることができる2つの主な方法があります。

  1. If you are interested in provability, then what you
    want is the Gödel-Tarski embedding of intuitionistic logic into
    classical S4 modal logic. The idea is that you can interpret the
    box modality of modal logic as a “provability” modality, and then
    stick a box in front of each connective. Then you can put the
    formula into whatever variant of modal CNF you need.

    See Mints’ paper The Gödel-Tarski Translations of
    Intuitionistic Propositional Formulas
    .

  2. If you are interested in retaining the ability to translate
    intuitionistic proofs, then one popular idea is to use Tarski’s
    “high school identities” to put intuitionistic formulas into a
    normal form related to the exponential polynomials. This gives a
    normal form for types, whose translation preserves the beta-eta
    equivalence of proofs of that type.

    See Danko Ilik’s The exp-log normal form of types.

これらの論文の両方とも、命題の事例に関するものです。私は一次数量子で何が起こるのか分かりません。

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です