直観主義論理

直観主義論理は、より一般的には構成的論理とも呼ばれ、構成的証明の概念をより忠実に反映することで古典論理で使用されるシステムとは異なる記号論理のシステムを指します。特に、直観主義論理のシステムは、古典論理における基本的な推論規則である排中律と二重否定除去を前提としていません。

形式化された直観主義論理は、もともとアーレント・ヘイティングによって、 LEJ・ブラウワーの直観主義プログラムの形式的な基礎を提供するために開発された。証明論的観点から見ると、ヘイティングの計算は排中律と二重否定除去が取り除かれた古典論理の制限である。排中律と二重否定除去は、いくつかの命題についてはケースバイケースで証明できるが、古典論理のように普遍的に成り立つわけではない。直観主義論理の標準的な説明は、BHK解釈である。^[1]

直観主義論理の意味論の体系はいくつか研究されてきた。これらの意味論の 1 つは、古典的なブール値意味論を反映しているが、ブール代数の代わりにヘイティング代数を使用する。別の意味論ではクリプキモデルを使用する。しかし、これらはヘイティングの演繹体系を研究するための技術的な手段であり、ブローワーの元々の非形式的な意味論的直観を形式化したものではない。「構成的真理」（単なる妥当性や証明可能性ではなく）という有意義な概念を提供することにより、そのような直観を捉えていると主張する意味体系としては、クルト・ゲーデルの弁証法的解釈、スティーヴン・コール・クリーネの実現可能性、ユーリ・メドヴェージェフの有限問題の論理^[2] 、またはギオルギ・ジャパリゼの計算可能性論理がある。しかし、そのような意味論は、ヘイティングの論理よりも適切に強い論理を執拗に誘導する。一部の著者は、これはヘイティングの計算自体の不十分さの兆候である可能性があり、ヘイティングの計算は構成的論理としては不完全であると主張している。^[3]

古典論理の意味論では、命題式には、どちらのケースについても直接的な証拠があるかどうかに関係なく、2 要素セット (それぞれ「真」と「偽」) から真理値が割り当てられます。これは、「真」または「偽」以外の真理値の可能性を排除するため、「排中律」と呼ばれます。対照的に、直観主義論理の命題式には明確な真理値が割り当てられず、直接的な証拠、つまり証明がある場合にのみ「真」とみなされます。また、命題式が直接的な証拠によって「真」になるのではなく、カリー-ハワードの意味での証明が含まれているとも言えます。したがって、直観主義論理の操作では、真理値ではなく、証拠と証明可能性に関して 正当性が保持されます。${\displaystyle \{\top ,\bot \}}$

直観主義論理は、数学における構成主義へのアプローチを開発する際によく使われるツールです。構成主義論理の使用は一般に、数学者や哲学者の間で議論の的となってきました (たとえば、ブラウワーとヒルベルトの論争を参照)。構成主義論理の使用に対する一般的な反対意見は、前述の古典論理の 2 つの中心的規則、排中律と二重否定消去法が欠けていることです。デイヴィッド ヒルベルトは、これらが数学の実践にとって非常に重要であると考え、次のように書いています。

「数学者から排中律を奪うことは、たとえば天文学者に望遠鏡を禁止したり、ボクサーに拳の使用を禁止したりするのと同じである。存在の表明と排中律を禁止することは、数学という科学を完全に放棄することに等しい。」^[4]

直観主義論理は、これらの規則を利用できないという課題があるにもかかわらず、数学において実用化されている。その理由の 1 つは、その制約により存在特性を持つ証明が生成され、他の形式の数学的構成主義にも適しているためである。非公式には、これは、オブジェクトが存在するという構成的証明がある場合、その構成的証明をそのオブジェクトの例を生成するアルゴリズムとして使用できることを意味します。これは、証明とアルゴリズムの間のCurry-Howard 対応と呼ばれる原理です。直観主義論理のこの特定の側面が非常に価値がある理由の 1 つは、実践者が証明支援ツールと呼ばれるさまざまなコンピューター ツールを利用できることです。これらのツールは、通常、数学的証明の公開とレビューに必要な通常の人間によるチェックが不可能な大規模な証明の生成と検証をユーザーによって支援します。そのため、証明支援ツール ( AgdaやCoqなど) を使用すると、現代の数学者や論理学者は、手作業だけで作成およびチェックできるものを超えた、非常に複雑なシステムを開発および証明できます。形式検証なしでは満足に検証できない証明の一例として、有名な四色定理の証明が挙げられます。この定理は 100 年以上も数学者を悩ませていましたが、反例の大半を排除しながらも、証明を完了するにはコンピュータ プログラムが必要となるほど十分な可能性を残す証明が開発されました。この証明はしばらく議論を呼んでいましたが、後に Coq を使用して検証されました。

直観主義論理の式の構文は、命題論理や一階述語論理に似ています。しかし、直観主義接続詞は古典論理と同じようには互いに関して定義できないため、その選択が重要になります。直観主義命題論理 (IPL) では、通常、基本接続詞として →、∧、∨、⊥ を使用し、¬ A を( A → ⊥)の省略形として扱います。直観主義一階述語論理では、量指定子∃ と ∀ の両方が必要です。

直観主義論理は、次のようなヒルベルト式の計算法を使って定義することができます。これは、古典的な命題論理を公理化する方法^{[ broken anchar ]}に似ています。^[5]

命題論理では、推論規則はmodus ponensである。

• MP: から推測する${\displaystyle \phi \to \psi }$${\displaystyle \phi}$${\displaystyle \psi}$

そして公理は

• その後-1:${\displaystyle \psi \to (\phi \to \psi )}$
• その後-2:${\displaystyle {\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}(\chi \to \phi )\to (\chi \to \psi ){\big )}}$
• AND-1:${\displaystyle \phi \land \chi \to \phi }$
• AND-2:${\displaystyle \phi \land \chi \to \chi }$
• AND-3:${\displaystyle \phi \to {\big (}\chi \to (\phi \land \chi ){\big )}}$
• または-1:${\displaystyle \phi \to \phi \lor \chi }$
• または-2:${\displaystyle \chi \to \phi \lor \chi }$
• OR-3:${\displaystyle (\phi \to \psi )\to {\Big (}(\chi \to \psi )\to {\big (}(\phi \lor \chi )\to \psi ){\Big )}}$
• 間違い：${\displaystyle \bot \to \phi }$

これを一階述語論理のシステムにするために、一般化規則は

• ${\displaystyle \forall }$-GEN: から推測し、が空いていない場合${\displaystyle \psi \to \phi }$${\displaystyle \psi \to (\forall x\ \phi )}$${\displaystyle x}$${\displaystyle \psi }$
• ${\displaystyle \exists }$-GEN: から推測し、が空いていない場合${\displaystyle \phi \to \psi }$${\displaystyle (\exists x\ \phi )\to \psi }$${\displaystyle x}$${\displaystyle \psi }$

公理とともに追加される

• PRED-1: 、項が内の変数に自由に置換できる場合（つまり、 内のどの変数も内で束縛されない場合）${\displaystyle (\forall x\ \phi (x))\to \phi (t)}$${\displaystyle t}$${\displaystyle x}$${\displaystyle \phi }$${\displaystyle t}$${\displaystyle \phi (t)}$
• PRED-2: PRED-1と同じ制限あり${\displaystyle \phi (t)\to (\exists x\ \phi (x))}$

を の省略形としてではなく否定の接続詞として含めたい場合は、次の文を追加すれば十分です。 ${\displaystyle \neg }$${\displaystyle \phi \to \bot }$

• NOT-1':${\displaystyle (\phi \to \bot )\to \neg \phi }$
• NOT-2':${\displaystyle \neg \phi \to (\phi \to \bot )}$

接続詞（偽）を省略したい場合は、いくつかの代替手段があります。たとえば、3つの公理FALSE、NOT-1'、NOT-2'を次の2つの公理に置き換えることができます。 ${\displaystyle \bot }$

• NOT-1:${\displaystyle (\phi \to \chi )\to {\big (}(\phi \to \neg \chi )\to \neg \phi {\big )}}$
• NOT-2:${\displaystyle \chi \to (\neg \chi \to \psi )}$

命題計算§公理と同様。NOT-1 の代替はまたは です。 ${\displaystyle (\phi \to \neg \chi )\to (\chi \to \neg \phi )}$${\displaystyle (\phi \to \neg \phi )\to \neg \phi }$

同値を表す接続詞は、を表す略語として扱うことができる。あるいは、公理を追加することもできる。 ${\displaystyle \leftrightarrow }$${\displaystyle \phi \leftrightarrow \chi }$${\displaystyle (\phi \to \chi )\land (\chi \to \phi )}$

• IFF-1:${\displaystyle (\phi \leftrightarrow \chi )\to (\phi \to \chi )}$
• IFF-2:${\displaystyle (\phi \leftrightarrow \chi )\to (\chi \to \phi )}$
• IFF-3:${\displaystyle (\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))}$

IFF-1 と IFF-2 は、必要に応じて、結合を使用して 1 つの公理に組み合わせることができます。 ${\displaystyle (\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))}$

ゲルハルト・ゲンツェンは、彼の体系 LK (古典論理のシーケント計算) を単純に制限すると、直観論理に関して健全かつ完全な体系になることを発見しました。彼はこの体系を LJ と呼びました。LK では、シーケントの結論側に任意の数の式を出現させることができます。対照的に、LJ ではこの位置に最大 1 つの式しか出現させられません。

LKの他の派生形は直観的な導出に限定されていますが、それでもシーケント内で複数の結論を導き出すことができます。LJ' ^[6]はその一例です。

純粋論理の定理は、公理と推論規則から証明できる命題です。たとえば、THEN-1 を THEN-2 で使用すると、 になります。後者のヒルベルト システムを使用した正式な証明は、そのページに記載されています。 の場合、は を意味します。言葉で言うと、「が成り立つということは が不合理であることを意味するので、が成り立つ場合は、 が成り立たない となります。」命題の対称性により、実際には次の式が得られます。 ${\displaystyle {\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}\phi \to (\chi \to \psi ){\big )}}$${\displaystyle \bot }$${\displaystyle \psi }$${\displaystyle (\chi \to \neg \phi )\to (\phi \to \neg \chi )}$${\displaystyle \chi }$${\displaystyle \phi }$${\displaystyle \phi }$${\displaystyle \chi }$

${\displaystyle (\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )}$

直観主義論理の定理を古典論理の観点から説明すると、古典論理の弱体化として理解できる。つまり、古典論理では行えなかった新しい推論を許さず、推論者に許す推論内容についてはより保守的である。直観主義論理の各定理は古典論理の定理であるが、その逆は成り立たない。古典論理の多くのトートロジーは直観主義論理の定理ではない。特に、上で述べたように、直観主義論理の主な目的の 1 つは、排中律を肯定せず、非構成的証明による背理法の使用を無効にすることである。非構成的証明は、存在が証明されるオブジェクトの明示的な例を提供せずに存在の主張を提供するために使用できる。

二重否定は排中律 ( PEM ) を肯定しません。PEM がどのような文脈でも支持されるとは限りませんが、反例も示すことができません。そのような反例は、古典論理では許可されていない推論 (特定の命題に対する法則の否定を推論すること) であるため、直観主義論理のような厳密な弱化では PEM は許可されません。正式には、任意の2 つの命題に対して、という単純な定理です。確立されたものが偽であると見なすことによって、これは確かに、法則の二重否定が極小論理ですでにトートロジーとして保持されていることを示しています。そして、矛盾することが確立されているので、排中律はすべての排中論理和に対して証明可能でさえありません。また、これは命題計算が常に古典論理と互換性があることも意味します。 ${\displaystyle {\big (}(\psi \lor (\psi \to \varphi ))\to \varphi {\big )}\leftrightarrow \varphi }$${\displaystyle \varphi }$${\displaystyle \neg \neg (\psi \lor \neg \psi )}$${\displaystyle \neg (\psi \lor \neg \psi )}$

排中律が命題を暗示すると仮定すると、対偶を 2 回適用し、二重否定の排中律を使用することで、厳密に古典的なさまざまなトートロジーの二重否定のバリエーションを証明できます。述語論理式では、一部の量化表現が否定されるため、状況はより複雑になります。

上記と同様に、形式の modus ponens から が成り立ちます。それらの関係は、常に新しい式を得るために使用できます。つまり、前提が弱められると、含意が強くなり、その逆も同様です。たとえば、 が成り立つ場合は も成り立ちますが、逆方向の図式は二重否定除去原理を意味することに注意してください。二重否定除去が可能な命題は、安定しているとも呼ばれます。直観主義論理は、限られた種類の命題に対してのみ安定性を証明します。排中律が成り立つ式は、選言三段論法 を使用して安定していることを証明できます。これについては、以下でより詳しく説明します。ただし、その逆は、手元の排中律自体が安定していない限り、一般には成り立ちません。 ${\displaystyle \psi \to ((\psi \to \varphi )\to \varphi )}$${\displaystyle \psi \to \neg \neg \psi }$${\displaystyle (\neg \neg \psi )\to \phi }$${\displaystyle \psi \to \phi }$

含意は、命題が何であれ、 と同等であることが証明できます。特別なケースとして、否定形式の命題 (ここでは ) は安定している、つまり は常に有効であることがわかります。 ${\displaystyle \psi \to \neg \phi }$${\displaystyle \neg \neg \psi \to \neg \phi }$${\displaystyle \psi =\neg \phi }$${\displaystyle \neg \neg \neg \phi \to \neg \phi }$

一般に、は より強く、 は より強く、 自体は、および の3 つの同値なステートメントを意味します。選言三段論法を使用すると、前の 4 つは確かに同値です。これにより、 の直観的に有効な導出も得られます。これは、恒等式と同値であるためです。 ${\displaystyle \neg \neg \psi \to \phi }$${\displaystyle \psi \to \phi }$${\displaystyle \neg \neg (\psi \to \phi )}$${\displaystyle \psi \to (\neg \neg \phi )}$${\displaystyle (\neg \neg \psi )\to (\neg \neg \phi )}$${\displaystyle \neg \phi \to \neg \psi }$${\displaystyle \neg \neg (\neg \neg \phi \to \phi )}$

が主張を表明する場合、その二重否定は単にの反証が矛盾するという主張を表明するだけです。このような単なる二重否定が証明されたとしても、のように、否定導入を通じて他のステートメントを否定するのにも役立ちます。二重否定の存在ステートメントは、特性を持つエンティティの存在を示すのではなく、そのようなエンティティが存在しないと仮定することの不合理さを示します。また、次のセクションの量指定子に関するすべての原則は、仮定の存在を前提とする含意の使用を説明しています。 ${\displaystyle \psi }$${\displaystyle \neg \neg \psi }$${\displaystyle \psi }$${\displaystyle (\phi \to \neg \psi )\to \neg \phi }$

存在量指定子（およびアトム）の前に2つの否定を追加することでステートメントを弱めることも、二重否定変換の中心的なステップです。これは、古典的な一階述語論理を直観主義論理に埋め込むものです。つまり、一階述語論理式が古典論理で証明可能であるのは、そのゲーデル-ゲンツェン変換が直観的に証明できる場合のみです。たとえば、形式の古典的な命題論理の定理の証明は 、の直観主義的証明に続いて二重否定除去を1回適用することで構成されます。したがって、直観主義論理は、構成的意味論で古典論理を拡張する手段と見なすことができます。 ${\displaystyle \psi \to \phi }$${\displaystyle \psi \to \neg \neg \phi }$

すでに最小限の論理で、 否定を使った含意に連言と選言を関連付ける次の定理を簡単に証明できます。

${\displaystyle (\phi \lor \psi )\to \neg (\neg \phi \land \neg \psi )}$

${\displaystyle (\phi \lor \psi )\to (\neg \phi \to \neg \neg \psi )}$、選言三段論法の弱められた変種

それぞれ

${\displaystyle (\phi \land \psi )\to \neg (\neg \phi \lor \neg \psi )}$

${\displaystyle (\phi \land \psi )\to \neg (\phi \to \neg \psi )}$同様に${\displaystyle (\phi \to \psi )\to \neg (\phi \land \neg \psi )}$

実際、これらのより強い変形は依然として成り立ちます。たとえば、前述のように、先行詞は二重否定されるか、または後述のように、先行詞側ですべてがに置き換えられる場合があります。ただし、これら 5 つの含意のいずれも、排中律 ( を考慮) または二重否定除去 (trueを考慮) を直ちに意味することなく、逆転させることはできません。したがって、左辺は右辺の可能な定義を構成しません。 ${\displaystyle \psi }$${\displaystyle \neg \neg \psi }$${\displaystyle \neg \psi }$${\displaystyle \phi }$${\displaystyle \phi }$

対照的に、古典的な命題論理では、これら 3 つの接続詞のうちの 1 つと否定を基本として、他の 2 つをそれに基づいて定義することができます。これは、たとえば、Łukasiewiczの命題論理の 3 つの公理で行われます。すべてを、 Peirce の矢印(NOR) やSheffer のストローク(NAND)などの唯一の十分な演算子に基づいて定義することもできます。同様に、古典的な一階述語論理では、量指定子の 1 つを、他の量指定子と否定に基づいて定義できます。これらは基本的に、このような接続詞をすべて単なるブール関数にする二価性の法則の結果です。直観主義論理では、二価性の法則が成立する必要はありません。その結果、基本的な接続詞のいずれも省略できず、上記の公理はすべて必要になります。したがって、接続詞と量指定子の間の古典的な同一性のほとんどは、一方向の直観主義論理の定理にすぎません。定理のいくつかは両方向に進み、つまり、後で説明するように同値です。

まず、命題 において が自由でない場合、 ${\displaystyle x}$${\displaystyle \varphi }$

${\displaystyle {\big (}\exists x\,(\phi (x)\to \varphi ){\big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

談話領域が空の場合、爆発原理により、存在論的陳述は何でも含意します。領域に少なくとも 1 つの項が含まれている場合、 について排中律を想定すると、上記の含意の逆も証明可能になり、2 つの辺が同等になります。この逆方向は、酒飲みのパラドックス(DP) と同等です。さらに、その存在論的かつ双対的な変形は、前提の独立性原理 (IP) によって与えられます。古典的には、上記の陳述はさらに、以下でさらに説明するより選言的な形式と同等です。ただし、建設的に、存在の主張は一般に見つけるのが困難です。 ${\displaystyle \forall x\,\phi (x)}$

議論領域が空でなく、さらに から独立している場合、そのような原理は命題論理における公式と同等です。ここで、公式は単に恒等式 を表現します。これは、 が偽の命題である場合に特別な場合に無矛盾律原理をもたらす、モーダス・ポネンスのカリー化された形式です。 ${\displaystyle \phi }$${\displaystyle x}$${\displaystyle (\phi \to \varphi )\to (\phi \to \varphi )}$ ${\displaystyle ((\phi \to \varphi )\land \phi )\to \varphi }$${\displaystyle \varphi }$${\displaystyle \neg (\phi \land \neg \phi )}$

元の含意に対する 誤った命題を考慮すると、重要な${\displaystyle \varphi }$

• ${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}$

言葉で言うと、「特性 を持たない実体が存在する場合、次のことは反証されます。各実体は特性 を持ちます。」 ${\displaystyle x}$${\displaystyle \phi }$${\displaystyle \phi }$

否定を含む量指定子の公式も、上で導出した無矛盾原理から直接導かれます。無矛盾原理の各例自体は、より具体的な からすでに導かれています。 が与えられた場合に矛盾を導くには、その否定（より強い ではなく）を確立するだけで十分であり、これにより二重否定の証明も重要になります。同様に、元の量指定子の公式は、に弱められた場合でも実際には依然として有効です。したがって、実際には、より強い定理が成立します。 ${\displaystyle \neg (\neg \neg \phi \land \neg \phi )}$${\displaystyle \neg \phi }$${\displaystyle \neg \neg \phi }$${\displaystyle \phi }$${\displaystyle \forall x\ \phi (x)}$${\displaystyle \forall x{\big (}(\phi (x)\to \varphi )\to \varphi {\big )}}$

${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\,\neg \neg \phi (x))}$

言葉で言うと、「特性を持たない実体が存在する場合、次のことは反証されます。各実体について、特性を持たないことを証明することはできません。」 ${\displaystyle x}$${\displaystyle \phi }$${\displaystyle \phi }$

第二に、

${\displaystyle {\big (}\forall x\,(\phi (x)\to \varphi ){\big )}\,\,\leftrightarrow \,\,{\big (}(\exists x\ \phi (x))\to \varphi {\big )}}$

同様の考察が当てはまる。ここでは存在論的部分は常に仮説であり、これは同値である。再び特別なケースを考えると、

• ${\displaystyle (\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))}$

証明された変換を使用すると、さらに 2 つの意味が得られます。 ${\displaystyle (\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )}$

${\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}$

${\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}$

もちろん、このような式の変形も導出でき、前件部に二重否定が含まれます。ここでの最初の式の特殊なケースは であり、これは確かに上記の同値性の箇条書きの - 方向よりも強力です。ここでの議論と以下の議論を簡潔にするために、式は一般に、前件部に二重否定を挿入する可能性のあるすべての要素を除いた弱められた形式で提示されます。 ${\displaystyle (\forall x\,\neg \phi (x))\to \neg (\exists x\,\neg \neg \phi (x))}$${\displaystyle \to }$

より一般的なバリエーションも存在します。述語とカリー化を組み込むと、次の一般化は、以下で説明する述語計算における含意と結合の関係も伴います。 ${\displaystyle \psi }$

${\displaystyle {\big (}\forall x\ \phi (x)\to (\psi (x)\to \varphi ){\big )}\,\,\leftrightarrow \,\,{\Big (}{\big (}\exists x\ \phi (x)\land \psi (x){\big )}\to \varphi {\Big )}}$

述語がすべての に対して明らかに偽である場合、この同値性は自明です。 がすべての に対して明らかに真である場合、スキーマは単純に前述の同値性に簡略化されます。クラス、、の言語では、この同値が偽である場合の特別なケースは、分離性の 2 つの特徴付けに相当します。 ${\displaystyle \psi }$${\displaystyle x}$${\displaystyle \psi }$${\displaystyle x}$${\displaystyle A=\{x\mid \phi (x)\}}$${\displaystyle B=\{x\mid \psi (x)\}}$${\displaystyle \varphi }$ ${\displaystyle A\cap B=\emptyset }$

${\displaystyle \forall (x\in A).x\notin B\,\,\leftrightarrow \,\,\neg \exists (x\in A).x\in B}$

量指定子の式には有限のバリエーションがあり、命題は 2 つだけです。

• ${\displaystyle (\neg \phi \lor \neg \psi )\to \neg (\phi \land \psi )}$
• ${\displaystyle (\neg \phi \land \neg \psi )\leftrightarrow \neg (\phi \lor \psi )}$

最初の原理は逆転できません。について を考えると、弱い排中律、つまり文 が意味されます。 しかし、直観主義論理だけでは の証明さえできません。 そのため特に、から主張を導く否定に対しては分配性原理は存在しません。 構成的読み方の非公式な例として、次のことを考えてみましょう。アリスとボブの両方がデートに現れなかったという決定的な証拠から、 2人のうちのどちらかに結びついて、この人が現れなかったという決定的な証拠を導くことはできません。 否定された命題は、単一の否定仮説から選言を許す古典的に有効なド・モルガンの法則 が自動的に構成的に成立しないという点で、比較的弱いです。 直観主義命題計算とその拡張の一部は、代わりに選言特性を示し、任意の選言の選言の1つが個別にも導出可能でなければならないことを意味しています。 ${\displaystyle \neg \psi }$${\displaystyle \phi }$${\displaystyle \neg \psi \lor \neg \neg \psi }$${\displaystyle \neg \psi \lor \neg \neg \psi \lor (\neg \neg \psi \to \psi )}$${\displaystyle \neg \phi \lor \neg \psi }$${\displaystyle \neg (\phi \land \psi )}$

これら2つの逆の変形、および二重否定の先行詞を持つ同等の変形については、すでに上で述べました。連言の否定への含意は、しばしば無矛盾原理から直接証明できます。この方法で、含意の混合形式を得ることもできます。たとえば、 。定理を連結すると、次のようになります 。${\displaystyle (\neg \phi \lor \psi )\to \neg (\phi \land \neg \psi )}$

• ${\displaystyle (\neg \neg \phi \lor \neg \neg \psi )\to \neg \neg (\phi \lor \psi )}$

その逆は弱い排中律を証明することになるため証明できません。

述語論理では、定数領域原理は有効ではありません。はより強い を意味しません。ただし、分配特性は任意の有限個の命題に対して成り立ちます。2 つの存在的に閉じた決定可能な述語に関するド・モルガンの法則の変形については、 LLPO を参照してください。 ${\displaystyle \forall x{\big (}\varphi \lor \psi (x){\big )}}$${\displaystyle \varphi \lor \forall x\,\psi (x)}$

一般的な同値性からは、 2 つの異なる接続詞を使用して 2 つの述語の非互換性を表現するimport-exportも得られます。

• ${\displaystyle (\phi \to \neg \psi )\leftrightarrow \neg (\phi \land \psi )}$

連言接続詞の対称性により、これもまた、すでに確立されている を意味します。否定連言の同値式は、カリー化とアンカリー化の特殊なケースとして理解できます。二重否定に関するさらに多くの考慮事項がここでも適用されます。そして、導入部で述べた連言と含意に関する不可逆定理の両方が、この同値から得られます。1 つは逆であり、 がよりも強いという理由だけで成立します。 ${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$${\displaystyle (\phi \to \psi )\to \neg (\phi \land \neg \psi )}$${\displaystyle \phi \to \psi }$${\displaystyle \phi \to \neg \neg \psi }$

次のセクションの原理を使用する場合、左側に否定をさらに追加した次の変形も当てはまります。

• ${\displaystyle \neg (\phi \to \psi )\leftrightarrow (\neg \neg \phi \land \neg \psi )}$

その結果、

• ${\displaystyle \neg \neg (\phi \land \psi )\leftrightarrow (\neg \neg \phi \land \neg \neg \psi )}$

すでに極小論理では、排中律がコンセクエンティア・ミラビリスと同値であることが証明されており、これはパースの法則の一例です。これは明らかに極小論理にすでに存在するモーダス・ポネンス と似ており、否定さえも含まない定理です。古典論理では、この含意は実際は同値です。を の形式とすると、排中律と爆発によりパースの法則が必然的に含まれることがわかります。 ${\displaystyle (\phi \lor \psi )\to ((\phi \to \psi )\to \psi )}$${\displaystyle \phi }$${\displaystyle \psi \to \varphi }$

直観主義論理では、 に関する定理の変形を次のように得ることができます。まず、を示唆するために、上で述べた の 2 つの異なる式を使用できることに注意してください。後者は、否定命題 の選言三段論法の形式です。直観主義論理では、強化された形式が依然として有効です。 ${\displaystyle \bot }$${\displaystyle \neg (\phi \land \psi )}$${\displaystyle (\neg \phi \vee \neg \psi )\to (\phi \to \neg \psi )}$${\displaystyle \neg \psi }$

• ${\displaystyle (\neg \phi \lor \psi )\to (\phi \to \psi )}$

前のセクションと同様に、との位置は入れ替わる可能性があり、導入部で述べたものよりも強力な原理となります。したがって、たとえば、直観的には「または」は「でない場合は」よりも強力な命題式ですが、これらは古典的には互換性があります。その含意は一般に逆転できません。なぜなら、それは直ちに排中律を意味するからです。 ${\displaystyle \neg \phi }$${\displaystyle \phi }$${\displaystyle P}$${\displaystyle Q}$${\displaystyle P}$${\displaystyle Q}$

矛盾と爆発を合わせると、より強い変形 も証明されます。また、これはの排中律が の二重否定消去法を意味することを示しています。 が固定されている場合、この含意は一般に逆転できません。ただし、は常に構成的に有効であるため、このようなすべての選言に対して二重否定消去法を仮定すると、古典論理も意味することになります。 ${\displaystyle (\neg \phi \lor \psi )\to (\neg \neg \phi \to \psi )}$${\displaystyle \psi }$${\displaystyle \psi }$${\displaystyle \neg \neg (\psi \lor \neg \psi )}$

もちろん、ここで確立した公式を組み合わせることで、さらに多くのバリエーションを得ることができます。たとえば、提示された選言三段論法は次のように一般化されます。

${\displaystyle {\Big (}{\big (}\exists x\ \neg \phi (x){\big )}\lor \varphi {\Big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

何らかの項が存在する場合、ここでの前提は を意味し、それ自体もここでの結論を意味します (これも、このセクションで言及されている最初の式です)。 ${\displaystyle \exists x{\big (}\phi (x)\to \varphi {\big )}}$

これらのセクションの議論の大部分は、極小論理にも同様に適用されます。しかし、一般的な を使用した選言三段論法に関しては、極小論理はせいぜい が を表すことを証明できます。ここでの結論は、爆発を使用して簡略化することしかできません。 ${\displaystyle \psi }$${\displaystyle (\neg \phi \lor \psi )\to (\neg \neg \phi \to \psi ')}$${\displaystyle \psi '}$${\displaystyle \neg \neg \psi \land (\psi \lor \neg \psi )}$${\displaystyle \psi }$

上記のリストには同値も含まれています。連言と選言を含む同値性は、 が実際に よりも強いことに由来します。同値の両側は、独立した含意の連言として理解できます。上記では、に対して不合理性が使用されています。機能的解釈では、これはif 節構造に対応します。したがって、たとえば「(または) ではない」は「 ではなく、 でもない」と同等です。 ${\displaystyle (P\lor Q)\to R}$${\displaystyle P\to R}$${\displaystyle \bot }$${\displaystyle R}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle P}$${\displaystyle Q}$

同値性自体は、一般に、含意（ ）の連言（ ）として定義され、次のように同等です。 ${\displaystyle \land }$${\displaystyle \to }$

• ${\displaystyle (\phi \leftrightarrow \psi )\leftrightarrow {\big (}(\phi \to \psi )\land (\psi \to \phi ){\big )}}$

これにより、次のような接続詞が定義可能になります。

• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )}$
• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )}$

同様に、およびは、たとえば直観主義接続詞の完全な基底です。 ${\displaystyle \{\lor ,\leftrightarrow ,\bot \}}$${\displaystyle \{\land ,\leftrightarrow ,\neg \}}$

アレクサンダー・V・クズネツォフが示したように、次の接続詞（最初のものは三項、2番目は五項）はどちらもそれ自体で機能的に完全であり、どちらも直観主義命題論理の唯一の十分な演算子の役割を果たすことができ、古典的な命題論理のシェファーストロークの類似物を形成します。^[7]

• ${\displaystyle {\big (}(P\lor Q)\land \neg R{\big )}\lor {\big (}\neg P\land (Q\leftrightarrow R){\big )}}$
• ${\displaystyle P\to {\big (}Q\land \neg R\land (S\lor T){\big )}}$

意味論は古典的な場合よりもかなり複雑です。モデル理論はヘイティング代数によって与えられますが、同等にクリプキ意味論によっても与えられます。2014年に、タルスキのようなモデル理論がボブ・コンスタブルによって完全であることが証明されましたが、完全性の概念は古典的とは異なります。^[8]

直観主義論理における証明されていない文には中間の真理値は与えられない（時々誤って主張されるが）。そのような文には第3の真理値はないと証明することができ、その結果は1928年のグリヴェンコに遡る。 ^[1]その代わりに、証明されるか反証されるまでは、それらの真理値は不明のままである。文は、矛盾を演繹することによって反証される。

この観点の帰結として、直観主義論理は、一般的な意味での二値論理、さらには有限値論理としての解釈もできない。直観主義論理は古典論理の自明な命題を保持しているが、命題式の各証明は有効な命題値とみなされるため、Heyting の命題を集合としてとらえると、命題式は (潜在的に非有限な) 証明の集合となる。 ${\displaystyle \{\top ,\bot \}}$

古典論理では、式が取り得る真理値についてよく議論します。値は通常、ブール代数のメンバーとして選択されます。ブール代数におけるmeet および join演算は、論理接続子 ∧ および ∨ と同一視されるため、形式A ∧ Bの式の値は、ブール代数におけるAの値とBの値の meet です。したがって、式が古典論理の有効な命題であるためには、その値がすべての値、つまり変数への値の割り当てに対して 1 になる必要があるという便利な定理が得られます。

対応する定理は直観主義論理にも当てはまりますが、各式にブール代数からの値を割り当てる代わりに、ブール代数が特別なケースであるヘイティング代数からの値を使用します。式は、任意のヘイティング代数上の任意の値の最上位要素の値を受け取る場合にのみ、直観主義論理で有効です。

有効な式を認識するには、実数直線Rの開集合を要素とする単一のヘイティング代数を考えるだけで十分であることが示される。^[9]この代数では、次の式が得られる。

${\displaystyle {\begin{aligned}{\text{Value}}[\bot ]&=\emptyset \\{\text{Value}}[\top ]&=\mathbf {R} \\{\text{Value}}[A\land B]&={\text{Value}}[A]\cap {\text{Value}}[B]\\{\text{Value}}[A\lor B]&={\text{Value}}[A]\cup {\text{Value}}[B]\\{\text{Value}}[A\to B]&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[B]\right)\end{aligned}}}$

ここでint( X )はXの内部であり、 X∁^はその補集合です。

A → Bに関する最後の恒等式により、 ¬ Aの値を計算できます。

${\displaystyle {\begin{aligned}{\text{Value}}[\neg A]&={\text{Value}}[A\to \bot ]\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[\bot ]\right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup \emptyset \right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\right)\end{aligned}}}$

これらの割り当てにより、直観的に有効な式は、まさに線全体の値が割り当てられている式になります。^[9]たとえば、式 ¬( A ∧ ¬ A ) は有効です。なぜなら、式Aの値としてどの集合Xが選択されても、 ¬( A ∧ ¬ A )の値は線全体であることが示されるためです。

${\displaystyle {\begin{aligned}{\text{Value}}[\neg (A\land \neg A)]&={\text{int}}\left({\text{Value}}[A\land \neg A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{Value}}[\neg A]\right)^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{int}}\left({\text{Value}}[A]^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\left(X\cap {\text{int}}\left(X^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\emptyset ^{\complement }\right)&&{\text{int}}\left(X^{\complement }\right)\subseteq X^{\complement }\\&={\text{int}}(\mathbf {R} )\\&=\mathbf {R} \end{aligned}}}$

したがって、この式の評価は真であり、実際に式は有効です。しかし、排中律A ∨ ¬ Aは、 Aの正の実数集合の特定の値を使用することで無効であることが示されます。

${\displaystyle {\begin{aligned}{\text{Value}}[A\lor \neg A]&={\text{Value}}[A]\cup {\text{Value}}[\neg A]\\&={\text{Value}}[A]\cup {\text{int}}\left({\text{Value}}[A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x>0\}^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x\leqslant 0\}\right)\\&=\{x>0\}\cup \{x<0\}\\&=\{x\neq 0\}\\&\neq \mathbf {R} \end{aligned}}}$

上で説明した無限ヘイティング代数における直観的に有効な式を解釈すると、代数のどの値が式の変数に割り当てられているかに関係なく、式の値として真を表す最上位要素が得られます。^[9]逆に、無効な式の場合、変数に値を割り当てると、最上位要素とは異なる値が生成されます。^{[10] [11]}有限ヘイティング代数は、これら2つの特性のうち2番目を持ちません。^[9]

ソール・クリプキは様相論理の意味論に関する研究を基に、直観主義論理のための別の意味論、すなわちクリプキ意味論または関係意味論を創案した。^{[12] [13] [5]}

直観主義論理のタルスキのような意味論は完全であると証明できないことが発見された。しかし、ロバート・コンスタブルは、タルスキのようなモデルの下では、より弱い完全性の概念が直観主義論理に依然として当てはまることを示した。この完全性の概念では、すべてのモデルに当てはまるすべてのステートメントではなく、すべてのモデルで同じように当てはまるステートメントに関心がある。つまり、モデルが式を真であると判断する単一の証明は、すべてのモデルに対して有効でなければならない。この場合、完全性の証明だけでなく、直観主義論理に従って有効な証明もある。^[8]

直観主義論理やその論理を使用する固定理論では、含意がメタ理論的には常に成り立つが、言語では成り立たないという状況が発生することがあります。たとえば、純粋な命題計算では、 が証明可能であれば、も証明可能です。別の例として、証明可能であることは、 も常に証明可能であることを意味します。システムはこれらの含意の下ではルールとして閉じており、ルールを採用できると言えます。 ${\displaystyle (\neg A)\to (B\lor C)}$ ${\displaystyle (\neg A\to B)\lor (\neg A\to C)}$${\displaystyle (A\to B)\to (A\lor C)}$${\displaystyle {\big (}(A\to B)\to A{\big )}\lor {\big (}(A\to B)\to C{\big )}}$

直観主義論理は、ブラジル論理、反直観主義論理、あるいは二重直観主義論理として知られる矛盾論理と双対性によって関連している。^[14]

FALSE (または NOT-2) 公理を取り除いた直観主義論理のサブシステムは最小論理として知られており、いくつかの違いは上で詳しく説明しました。

1932 年、クルト ゲーデルは古典論理と直観主義論理の中間の論理体系を定義しました。実際、ブール代数と同等でない有限 Heyting 代数は、(意味的に)中間論理を定義します。一方、純粋直観主義論理の式の妥当性は、個々の Heyting 代数に結び付けられるのではなく、同時にすべての Heyting 代数に関係します。

たとえば、否定を含まないスキーマの場合、古典的に有効な を考えます。これを直観主義論理よりも採用すると、ゲーデル・ダメット論理と呼ばれる中間論理が得られます。 ${\displaystyle (A\to B)\lor (B\to A)}$

古典論理のシステムは、次の公理のいずれかを追加することによって得られます。

• ${\displaystyle \phi \lor \neg \phi }$（排中律）
• ${\displaystyle \neg \neg \phi \to \phi }$（二重否定除去）
• ${\displaystyle (\neg \phi \to \phi )\to \phi }$( Consequentia mirabilis、パースの法則も参照)

様々な定式化、または2つの変数の図式としての定式化（例えば、パースの法則）も存在する。注目すべきものの1つは、（逆の）対置の法則である。

• ${\displaystyle (\neg \phi \to \neg \chi )\to (\chi \to \phi )}$

これらについては、中間ロジックの記事で詳しく説明します。

一般に、2 要素クリプキ フレーム では有効でない(つまり、スメタニッチの論理に含まれない) 古典的なトートロジーを追加の公理として採用することができます。 ${\displaystyle \circ {\longrightarrow }\circ }$

1932年にクルト・ゲーデルの多値論理に関する研究は、直観主義論理が有限値論理ではないことを示した。^{[15] （直観主義論理の}無限値論理解釈については、上記の「ヘイティング代数意味論」のセクションを参照）。

直観主義命題論理（IPC）の任意の式は、次のように通常の様相論理 S4の言語に翻訳できます。

${\displaystyle {\begin{aligned}\bot ^{*}&=\bot \\A^{*}&=\Box A&&{\text{if }}A{\text{ is prime (a positive literal)}}\\(A\wedge B)^{*}&=A^{*}\wedge B^{*}\\(A\vee B)^{*}&=A^{*}\vee B^{*}\\(A\to B)^{*}&=\Box \left(A^{*}\to B^{*}\right)\\(\neg A)^{*}&=\Box (\neg (A^{*}))&&\neg A:=A\to \bot \end{aligned}}}$

そして、翻訳された式が命題様相論理S4で有効であるのは、元の式がIPCで有効である場合に限ることが実証されている。^[16]上記の式のセットは、ゲーデル・マッキンゼー・タルスキー翻訳と呼ばれています。様相論理S4の直観主義バージョンである構成的様相論理CS4も存在します。^[17]

IPCと単純型ラムダ計算の間には拡張されたカリー・ハワード同型性が存在する。^[17]

• ヴァン・アッテン、マーク（2022年5月4日）。「直観主義論理の発展」。ザルタ、エドワード・N（編）『スタンフォード哲学百科事典』。

• McCarty, David Charles (2009)。「数学における直観主義」。Shapiro, Stewart (編)。オックスフォード数学・論理哲学ハンドブック。pp.  356– 386。doi :10.1093/ oxfordhb / 9780195325928.003.0010。ISBN 978-0-19-532592-8。

• モスコヴァキス、ジョアン（2022年12月16日）。「直観主義論理」。ザルタ、エドワードN.（編）スタンフォード哲学百科事典。

• 「S4 変換による直観主義論理のタブロー法」。グルノーブル情報科学研究所。命題式の直観主義的妥当性をテストする。