直観主義論理

接続詞を含めたい場合は${\displaystyle \neg }$否定の略語として考えるのではなく、${\displaystyle \phi \to \bot }$付け加えるだけで十分だ。

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

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

• 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は、必要に応じて単一の公理に統合することができる。${\displaystyle (\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))}$接続詞を使って。

上記と同様に、次の形式のモーダス・ポネンスから${\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 }$常に有効です。

一般的に、${\displaystyle \neg \neg \psi \to \phi }$より強い${\displaystyle \psi \to \phi }$これはより強い${\displaystyle \neg \neg (\psi \to \phi )}$これは、それ自体が以下の3つの同等の記述を意味する。${\displaystyle \psi \to (\neg \neg \phi )}$、${\displaystyle (\neg \neg \psi )\to (\neg \neg \phi )}$そして${\displaystyle \neg \phi \to \neg \psi }$選言三段論法を用いると、前の4つは確かに同値である。これはまた、直観的に妥当な導出を与える。${\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つの否定を追加して命題を弱めることは、二重否定変換の中核的なステップでもある。これは、古典一階述語論理を直観主義論理に埋め込むことを意味する。一階述語論理式が古典論理で証明可能であるのは、そのゲーデル＝ゲンツェン変換が直観主義的に証明可能である場合に限る。例えば、次の形式の古典命題論理の定理は、 ${\displaystyle \psi \to \phi }$直観主義的証明からなる証明がある${\displaystyle \psi \to \neg \neg \phi }$続いて二重否定除去を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 )}}$

議論領域が空の場合、爆発原理により、存在命題は何でも含意する。領域が少なくとも１つの項を含む場合、排中律を仮定すると、${\displaystyle \forall x\,\phi (x)}$すると、上記の含意の逆もまた証明可能となり、つまり両辺が等価になる。この逆方向は、飲酒者のパラドックス（DP）と等価である。さらに、その存在論的かつ双対的な変種は、前提の独立性の原理（IP）によって与えられる。古典的には、上記の命題は、さらに後述するより選言的な形式と等価である。しかし、構成論的には、存在の主張は一般的に得にくい。

議論の領域が空ではなく、${\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))}$

実証済みの変換${\displaystyle (\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )}$さらに、以下の2つの意味合いを得ることができます。

${\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 )}}$

述語が${\displaystyle \psi }$すべてにおいて明らかに誤りである${\displaystyle x}$ならば、この等価性は自明である。${\displaystyle \psi }$すべてにおいて間違いなく真実である${\displaystyle x}$スキーマは、先に述べた等価性に単純に還元されます。クラスの言語では、${\displaystyle A=\{x\mid \phi (x)\}}$そして${\displaystyle B=\{x\mid \psi (x)\}}$偽とのこの等価性の特殊なケース${\displaystyle \varphi }$分離性の2つの特徴付けを等価とする${\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 )}$

第一の原則は覆すことはできない。${\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 )}$構成的解釈の非公式な例として、次のことを考えてみましょう。アリスとボブの両方がデートに現れたわけではないという決定的な証拠から、この人物が現れなかったという、どちらか一方に関連する決定的な証拠を導き出すことはできません。否定命題は、古典的に有効なド・モルガンの法則（単一の否定仮説から選言を与える）が構成的に自動的に成り立つわけではないため、比較的弱いと言えます。直観主義命題論理とその拡張の一部は、代わりに選言特性を示し、任意の選言の選言項の1つが個別に導出可能である必要があることを意味します。

これら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 )}$

逆は証明できない。なぜなら、それは弱い排中律を証明することになるからである。

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

一般的な等価性から、2つの異なる接続詞を用いて2つの述語の非互換性を表現するインポート・エクスポートも導かれる。

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

接続詞の対称性により、これは既に確立されたことを再び意味する。${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$否定された連言の同値式は、カリー化と非カリー化の特殊なケースとして理解できます。二重否定に関するさらに多くの考察が再び適用されます。そして、上記の非相互定義可能性の導入で言及した連言と含意に関する2つの非可逆定理は、この同値性から導かれます。1つは単純に証明された逆の変形であり、${\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 }$排中律と爆発法則は、ピアースの法則を必然的に導くことがわかっている。

直観主義論理では、以下の定理の変形が得られる。${\displaystyle \bot }$以下のように。まず、2つの異なる式があることに注意する。${\displaystyle \neg (\phi \land \psi )}$上記で述べたことは、${\displaystyle (\neg \phi \vee \neg \psi )\to (\phi \to \neg \psi )}$また、直接的な場合分け分析からも導かれ、否定が入れ替わった変種、例えば定理なども同様である。${\displaystyle (\neg \phi \lor \psi )\to (\phi \to \neg \neg \psi )}$または${\displaystyle (\phi \lor \psi )\to (\neg \phi \to \neg \neg \psi )}$後者は非相互定義可能性の序論で言及されている。これらは否定命題を含む選言三段論法の形式である。${\displaystyle \neg \psi }$強化された形式は直観主義論理では依然として有効である、例えば

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

一般的に、この含意を逆転させることはできない。なぜなら、逆転させると直ちに排中律を意味するからである。したがって、直観的に言えば、「${\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 {\big (}\neg \neg \phi \to (\bot \lor \psi ){\big )}}$ここでの最終的な結論は依然として${\displaystyle \neg \neg \psi }$しかし、すべての場合において、それをさらに単純化するために${\displaystyle \psi }$爆発を必要とする。

上記のリストには同値関係も含まれています。論理積と論理和を含む同値関係は、${\displaystyle (P\lor Q)\to R}$実際にはより強い${\displaystyle P\to R}$等価性の両辺は、独立した含意の連言として理解できる。上記は不条理である。${\displaystyle \bot }$用途${\displaystyle R}$機能的解釈では、if節構造に対応します。例えば「Not (${\displaystyle P}$または${\displaystyle Q}$)" は "Not${\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 \{\lor ,\leftrightarrow ,\neg \}}$例えば、直観主義的結合子の完全な基底である。

Alexander V. Kuznetsovが示したように、次の結合子のいずれか (最初のものは三項結合子、2 番目のものは五項結合子) はそれ自体で機能的に完全です。どちらも直観主義命題論理の唯一の十分演算子の役割を果たすことができ、古典命題論理のSheffer ストロークの類似物を形成します。 ^{[ 6 ]}

• ${\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 )}}$

直観主義論理は、ブラジル論理、反直観主義論理、または双対直観主義論理として知られる矛盾のない論理と双対性によって関連している。^{[ 13 ]}

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

1932年、クルト・ゲーデルは古典論理と直観主義論理の中間に位置する論理体系を定義した。実際、ブール代数と等価でない任意の有限ハイティング代数は、（意味論的に）中間的な論理を定義する。一方、純粋直観主義論理における論理式の妥当性は、個々のハイティング代数に縛られることなく、あらゆるハイティング代数に同時に関係する。

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

古典論理体系は、以下の公理のいずれか1つを追加することによって得られる。

• ${\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年に直観主義論理が有限値論理ではないことを示した。^{[ 14 ]} （直観主義論理の無限値論理解釈については、上記の「ハイティング代数意味論」の項を参照のこと。）

直観主義命題論理（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で有効である場合に限ることが実証されている。^{[ 15 ]}上記の式のセットは、ゲーデル・マッキンゼー・タルスキー翻訳と呼ばれている。また、直観主義的な様相論理S4のバージョンとして、構成的様相論理CS4と呼ばれるものもある。^{[ 16 ]}