最小限のロジック

暗黙の導入として、${\displaystyle C\to (B\to C)}$、 など${\displaystyle \bot \to (B\to \bot )}$考慮することによって${\displaystyle C=\bot }$つまり

$${\displaystyle \bot \to \neg B.}$$

同じく、

$${\displaystyle B\to \neg \neg B}$$

命題形式のモーダス・ポネンスから直接導き出せる${\displaystyle B\to ((B\to C)\to C)}$これを有効な対偶原理（下記参照）と組み合わせると、否定命題の安定性も導かれる。

$${\displaystyle \neg \neg \neg B\leftrightarrow \neg B.}$$

2 番目に同等のもの${\displaystyle \neg B}$フレーゲの定理から導かれる、

$${\displaystyle (B\to \neg B)\leftrightarrow \neg B.}$$

これはひいては、有効な弱い形のconsequentia mirabilisを意味する。${\displaystyle (\neg B\to \neg \neg B)\leftrightarrow \neg \neg B}$つまり、これは、ある命題の否定が、その命題を否定できないことを示唆する場合に限り、その命題を否定することはできない、ということを述べている。

二重否定導入には

$${\displaystyle {\big (}\neg \neg A\to B{\big )}\to {\big (}A\to B{\big )}}$$

そして、それはまた、その単なる特殊なケースとして、${\displaystyle B=\neg \neg A}$このセクションの残りの部分では、上記の最初の３つの定理を、それぞれ２つの命題変数を含む、より強力な妥当な定理の特殊な場合として再導出します。

まず、否定を含まない含意計算で採用された原理については、ヒルベルトシステムのページで、同一性の法則、含意導入、およびモーダス・ポネンスの変形の公理の命題形式を通して提示されています。${\displaystyle {\big (}B\to (A\to C){\big )}\leftrightarrow {\big (}A\to (B\to C){\big )}}$そこで証明されている。最初の導出では、${\displaystyle C=\bot }$ここではすぐにスキーマの結果が得られます

$${\displaystyle {\big (}B\to \neg A{\big )}\leftrightarrow {\big (}A\to \neg B{\big )}}$$

直観主義ヒルベルト体系では、導入しない場合${\displaystyle \bot }$定数として、これは2番目の否定特性公理としても解釈できます。（もう1つは爆発です。）${\displaystyle A}$として${\displaystyle \bot }$応答${\displaystyle \neg B}$上記は確かに爆発を示している${\displaystyle \bot \to \neg B}$応答${\displaystyle B\to \neg \neg B}$。

第二に、二重否定の導入も同様に、単なる特殊なケースから導かれる。${\displaystyle B=\neg A}$で

$${\displaystyle {\big (}\neg \neg A\to \neg B{\big )}\leftrightarrow {\big (}A\to \neg B{\big )}}$$

これは上記の2つの定理に近い。${\displaystyle {\big (}([A\to C]\to C)\to (B\to C){\big )}\leftrightarrow {\big (}A\to (B\to C){\big )}}$確かにその通りです。${\displaystyle {\big (}[(B\to C)\to C]\to C{\big )}\leftrightarrow (B\to C)}$これは否定文の安定性の一般化である。後者は、別の方法でも次のことから導かれる。${\displaystyle {\big (}[(B\to C)\to C]\to D{\big )}\to (B\to D)}$カリー・ハワード対応の下では、ここでの最後の定理はラムダ式によっても正当化される可能性がある。${\displaystyle \lambda f^{((B\to C)\to C)\to D}.\ \lambda b^{B}.\ f(\lambda g^{B\to C}.g(b))}$これは、ここで挙げた定理の1つについて、この方法を述べるためだけのものです。

第三に、含意導入の対偶から、

$${\displaystyle {\big (}\neg (A\to B){\big )}\to \neg B}$$

そして${\displaystyle A\to {\big (}B\leftrightarrow (A\to B){\big )}}$同様に、

$${\displaystyle {\big (}\neg \neg (A\to B){\big )}\to {\big (}A\to \neg \neg B{\big )}}$$

これから、二重否定の含意が導かれる。${\displaystyle B=A}$同様に。最後に、最小論理では対偶

$${\displaystyle (B\to A)\to (\neg A\to \neg B)}$$

証明できるかもしれない${\displaystyle (B\to A)\to ((A\to C)\to (B\to C))}$これから、任意の${\displaystyle B}$1つは${\displaystyle A\to (\neg A\to \neg B)}$したがって、これに関連して、否定の導入と同様に、${\displaystyle (A\land \neg A)\to \neg B}$これらからもまた、${\displaystyle \bot \to \neg B}$二重否定の含意は以下からも導かれる。${\displaystyle B=\neg A}$で${\displaystyle A\to (\neg A\to \neg B)}$弱いconsequentia mirabilisを使用します。

含意のみの観点からの記述を超えて、これまで議論してきた原理は定理としても確立できる。否定の定義により、${\displaystyle \bot }$モーダス・ポネンスの声明は次の形式で${\displaystyle (A\land (A\to C))\to C}$それ自体は矛盾律に特化しており、${\displaystyle C=\bot }$否定が含意である場合、非矛盾のカレー形式は再び${\displaystyle A\to \neg \neg A}$さらに、前節で詳述した接続詞を用いた否定の導入は、単なる特殊なケースとして暗黙のうちに示されている。${\displaystyle {\big (}B\to (A\land (A\to C)){\big )}\to (B\to C)}$このように、最小論理は、否定除去（別名爆発）を除いた構成的論理として特徴づけることができる。

これにより、2 つの命題の結合を含む一般的な直観主義的含意のほとんども、カリー化同値性を含めて得ることができます。重要な同値性

$${\displaystyle {\big (}(A\lor B)\to C{\big )}\leftrightarrow {\big (}(A\to C)\land (B\to C){\big )}}$$

強調する価値がある。それは、両方とも同じことを言う2つの同等の言い方であることを表現している。${\displaystyle A}$そして${\displaystyle B}$暗示する${\displaystyle C}$そこから、よく知られているド・モルガンの法則のうち2つが得られる。

$${\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B).}$$

3つ目の有効なド・モルガンの法則も導き出すことができる。

排中命題の否定は、それ自身の妥当性を意味する。上記のコンセクエンティア・ミラビリスの弱い変形を参照すると、次のことが導かれる。

$${\displaystyle \neg \neg (B\lor \neg B)}$$

この結果は、${\displaystyle {\big (}(B\lor (B\to C))\to C{\big )}\to C}$これは以下から導かれる${\displaystyle ((A\lor B)\to C)\to (B\to C)}$検討する際に${\displaystyle B\to C}$のために${\displaystyle A}$。

もう1つ、もう少し具体的な特殊なケースとして、${\displaystyle {\big (}(A\lor \bot )\to A{\big )}\leftrightarrow (\bot \to A)}$すでに、素朴な選言法則が爆発とどのように結びついているかを示唆しており、このトピックについては後ほど詳しく説明します。

関連して、${\displaystyle A}$事例分析によると、${\displaystyle (B\lor A)\land (A\to B)}$単に${\displaystyle B}$。 特に、${\displaystyle (B\lor \neg B)\land (\neg B\to B)}$と同等${\displaystyle B}$同様に、${\displaystyle {\big (}B\lor (B\to C){\big )}\land {\big (}(B\to C)\to C{\big )}}$と同等${\displaystyle B\lor C}$そして特に、${\displaystyle (B\lor \neg B)\land \neg \neg B}$と同等${\displaystyle B\lor \bot }$しかし、それは一般的に単に${\displaystyle B}$そして今、同様に、最小限の論理で救済された含意は

$${\displaystyle {\big (}(B\lor \neg A)\land \neg \neg A{\big )}\to {\big (}(B\lor \neg B)\land \neg \neg B){\big )}}$$

これは、選言三段論法の完全な、直観主義的にのみ証明可能な命題表現と比較されるべきである。ここでも、爆発を伴う直観主義論理においてのみ、ここでの帰結は常に単にと証明可能的に同等である。${\displaystyle B}$許容される規則としての選言三段論法については、以下で論じる。

直観主義論理は証明しない${\displaystyle (A\to B)\to (\neg A\lor B)}$、そして${\displaystyle (A\land \neg A)\to B}$逆方向も証明することはできない。逆に、最小論理においては、分解規則のすべての形式が有効であるとは限らない。

多くの状況において、${\displaystyle \bot }$論理体系において独立した定数である必要はなく、その役割は任意の拒否された命題で置き換えることができる。例えば、次のように定義できる。${\displaystyle a=b}$どこ${\displaystyle a,b}$区別されるべきである。その命題は同じ記号で表すことができる。${\displaystyle \bot }$このような定義は、単純な構成論理よりも有益である可能性もある。

このような特徴付けの例${\displaystyle \bot }$は${\displaystyle 0=1}$自然数を含む理論において。${\displaystyle \bot }$ここでは、任意の2つの与えられた数が等しいことを証明できます。たとえば、${\displaystyle 1=0}$続く${\displaystyle 7=6+1=6+0=6}$この形式の証明は、論理公理である爆発がない場合でも可能である。したがって、算術は次のような場合に矛盾しているとみなされる。${\displaystyle 0=1}$導出できる。

この定義の文脈では、証明する${\displaystyle 3^{4}=8}$偽りである、つまり${\displaystyle \neg (3^{4}=8)}$証明する${\displaystyle (3^{4}=8)\to (0=1)}$表記法を導入する${\displaystyle 3^{4}\neq 8}$主張も捉えるために。そして実際、算術を使って、${\displaystyle {\tfrac {3^{4}-8}{73}}=1}$保持するが、${\displaystyle (3^{4}=8)}$また、${\displaystyle {\tfrac {3^{4}-8}{73}}=0}$つまり、これは${\displaystyle 1=0}$したがって、我々は次のものを得る。${\displaystyle \neg (3^{4}=8)}$証明終了。