Loading article…
証明論および構成的数学において、前提の独立性の原理（IP）は、φと∃xθが形式理論における文であり、 φ→ ∃xθが証明可能であるならば、∃x (φ→θ)も証明可能であると述べている。ここで、xはφの自由変数であってはならず、θはφに依存する述語となり得る。
この原理の主な適用分野は直観主義論理の研究であり、そこではこの原理は一般的には成り立たない。その重要な等価な特殊ケースについては後述する。この原理は古典論理では成り立つ。
よくあることだが、議論の領域は存在することが前提とされている。つまり、理論の一部は少なくとも何らかの項で構成されている。議論のために、そのような項の1つを として区別する。自然数の理論では、この役割は数7によって担われる。以下では、φとψはxに依存しない命題を表し、θはxに依存できる述語である。
以下のことは容易に証明できる。
最初のシナリオでは、前提で制約されている何らかのx が結論で再利用されますが、一般的にはそれを検証するのは事前のaではありません。2 番目のシナリオでは、特に値a が原理の結論を検証します。したがって、これら 2 つのケースでは、何らかのx が結論を検証します。
第三に、上記の２点とは対照的に、φを証明または拒否する方法が不明な場合を考えてみましょう。中核となるケースは、φが式∃ z θ( z )である場合で、この場合、前件φ → ∃ x θは自明になります。「θが充足可能であれば、θは充足可能である」。説明のために、θは算術における決定可能な述語であると仮定しましょう。つまり、任意の数bに対して、命題θ( b )の真偽値を容易に調べることができます。より具体的には、θは、証明可能性が不明な数学的予想の形式的証明のインデックスがxであることを表します。確かに、ここで∃ x (φ → θ)を確立する１つの方法は、特定のインデックスxを提供し、それが実際にθを満たすことが示される（そして、ある値zがθを満たすという仮定によって助けられる）ことです。しかし、そのようなxを解明することは不可能である（今のところ不可能であり、おそらく今後も不可能であろう）。なぜなら、そのようなx は、まだ証明も否定もされていない予想の証明を正確に符号化しているからである。
上記の算術例は、いわゆる弱い反例を示しています。存在主張∃ x (φ → θ) は直観主義的な手段では証明できません。φ → θ を検証するxを調べることができれば、この予想は解決されます。
例えば、次のような古典的な議論を考えてみましょう。ゴールドバッハ予想には証明があるか、ないかのどちらかです。もし証明がないとすれば、証明があると仮定するのは不合理であり、そこからどんな結論も導き出されます。特に、証明があるという結論が導き出されます。したがって、ゴールドバッハ予想に証明があると仮定すれば、ある自然数インデックスxが存在し、 xはそのような証明のインデックスとなります。
この問題は、直観主義的証明に対するBHK解釈を用いてアプローチすることも可能であり、これは古典的な証明計算と比較されるべきである。BHKによれば、 φ → ∃ x θの証明は、φ の証明を受け取り、 ∃ x θの証明を返す関数から構成される。ここでは、証明自体が関数への入力として機能し、可能な場合はxを構成するために使用できる。∃ x (φ → θ)の証明は、特定のxと、φ の証明を、x がその値を持つ θ の証明に変換する関数を示す必要がある。証明計算では、弱い反例と同様に、適切なx は、適合する φ に関連付けられたより多くの入力を使用してのみ与えられる。
実際、違反モデルを用いることで、前提φ → ∃ x θは原理によって認められた一般的な存在証明には不十分であることが確立されている。
前提が弱められると、含意は強められる。ここで重要なのは、否定文の形の前提、φ := ¬η である。
算術において¬η → ∃ x θの証明が存在するならば、∃ x (¬η → θ) の証明も存在するということがメタ理論的に確立されている。
これが一般的な集合論にも当てはまるかどうかは不明である。[ 1 ]
存在量化子を含まないφの場合、直観主義論理上の理論は、この種の規則に関して概して良好な振る舞いを示す。
前述のとおり、固定されたφと任意のθに対する前提の独立性の原理は、φの証明からも、φの否定からも導かれる。したがって、排中律を公理的に仮定すれば、この原理は妥当である。
例えば、ここでは∃ x ((∃ y θ) → θ)が常に成り立つ。より具体的には、次の命題を考えてみよう。
これは古典的に証明可能であり、次のように証明できます。ゴールドバッハ予想の証明の指標が存在するか、存在しないかのどちらかです。一方、指標が存在する場合、その指標は上記の命題における有効なxとしても機能します。他方、そのような指標が存在しない場合、そのような指標が存在することは矛盾であり、爆発的にあらゆる結論が導き出されます。特に、x=7はゴールドバッハ予想の証明の指標であることが導き出されます。どちらの場合も、命題を検証する何らかの指標が存在します。
構成的には、あるxを用意し、そのxに対して θ が成り立つことを示せるようにする必要がある（そして、φ が有効であると仮定し、したがってあるyに対して∃ y θ も成り立つことを前提とする）。従来は、φ に関する 2 つの仮説から出発して、同じ興味深い結論を導き出すだけで十分であった。後者の枠組みでは、いずれにせよ何らかのx が存在すると主張され、論理的にはそれを明示する必要はない。
IP とより短い∃ x ((∃ y θ) → θ)は命題論理に類似するものを持つ。直観主義計算では、有限形式
前提においてその情報を表現していると理解できる連言のペアのうち、どの命題を含意するかを定める必要はない。これは、より簡潔ではあるが実際には同等の、いわゆるダーク・ジェントリーの原理に帰着する。。この図式は、直観主義的なconsequentia mirabilisの形式を通して、否定命題に対する厳密に弱い排中律（WLEM）を暗示している。
クライゼル・パトナム論理は、直観主義論理から、否定命題にこの図式を採用することによって得られる。は依然として選言の性質を持つ。対応する規則は直観主義論理における許容規則である。
