最小論理

最小論理（さいしょうろんり、テンプレート:Lang-en-short、最小計算とも）は、もともとテンプレート:仮リンクによって「テンプレート:Lang」という名称で開発された記号論理学の体系であるテンプレート:Sfn。これは直観主義論理よりも弱い矛盾許容論理であり、任意の命題が矛盾から証明できるとする爆発律（ex falso quodlibet）、および排中律の双方を退ける。これに対して、直観主義論理は他のほとんどの構成的論理と同様、排中律のみを退ける。

したがって、最小論理においては、任意の命題$A$と$B$について、以下の2つの導出はいずれも成り立たない。

$⊢(B\vee \mathrm{\neg }B)$,

$(A\wedge \mathrm{\neg }A)⊢B$.

古典論理では、ex falso律 $(A\wedge \mathrm{\neg }A)\to B$（あるいは同値な $\mathrm{\neg }A\to (A\to B)$）も成り立つ。これらは最小論理では自動的には成り立たない。

「最小論理」という名称は、連結記号の数を制限した論理体系を指すために用いられることもある。

構文と公理化

最小論理は通常、含意 $\to$、連言 $\wedge$、選言 $\vee$、そして矛盾または不条理 $\mathrm{\perp }$ を基本の論理結合子とする、直観主義命題論理と同じ構文を用いて定式化されるのが通例であり、¬Aは(A → ⊥)の略記として扱われる。この構文を用いると、最小論理は、$\mathrm{\perp }$に固有に言及する公理を持たない、直観主義論理の正のフラグメントと同じ公理化を持つ。

¬を基本の結合子とする最小論理の代替的な定式化も、爆発が避けられている限り可能である。そのような公理化には否定に関する直接の公理が必要であり、それは以下で与えられる。常に望まれる性質は、次に論じる否定導入律である。

定理

否定導入

否定に関する妥当な規則をざっと分析するだけでも、完全な爆発を欠くこの論理が何を証明でき、何を証明できないかについてよい見通しが得られる。 最小論理のような否定を含む言語における自然な命題の一つは、例えば否定導入の原理であり、これはある命題を仮定してそこから矛盾を導出することによって、その命題の否定を証明するというものである。最小論理においては、この原理は次の式と同値である。

$$(B\to (A\wedge \mathrm{\neg }A))\to \mathrm{\neg }B,$$

これは任意の2つの命題について成り立つ。$B$を矛盾それ自体 $A\wedge \mathrm{\neg }A$ とすると、これは無矛盾律

$$\mathrm{\neg }(A\wedge \mathrm{\neg }A).$$

を確立する。任意の$C$を仮定すると、実質条件法の導入規則は$B\to C$を与える。これは$B$と$C$が関連性を持つわけではない場合にも成り立つ。これと含意除去を用いると、上記の導入原理は

$$(A\wedge \mathrm{\neg }A)\to \mathrm{\neg }B,$$

を含意する。すなわち、何らかの矛盾を仮定すると、あらゆる命題を否定できるということである。この論理において否定導入が可能であることから、任意の矛盾はあらゆる二重否定を証明する。逆に、ある$C$について$\mathrm{\neg }C$が証明可能であれば、さらに常に$C\to \mathrm{\neg }\mathrm{\neg }B$も成り立つ。爆発律があれば帰結における二重否定を除去できるが、この原理は最小論理では採用されない。

これにより、$C\to B$という形の多くの命題は、最小論理において爆発律と同値であることがわかる。一例を挙げるならば、$\mathrm{\neg }(A\vee \mathrm{\neg }A)\to B$である。

不条理を介した公理化

正の計算を最小論理へと拡張する一つの方法は、$\mathrm{\neg }B$を含意として扱うことであり、この場合、論理の構成的な含意命題計算から得られる定理が否定に関する命題にも引き継がれる。このために、$\mathrm{\perp }$が、体系が無矛盾でない限り証明不可能な命題として導入され、否定$\mathrm{\neg }B$は$B\to \mathrm{\perp }$の略記として扱われる。構成的には、$\mathrm{\perp }$はそれを信じる理由がありえない命題を表す。

$(A\to C)\to (A\to B)$という形の任意の含意は、単に$C\to B$と同値である。もし不条理が論理において原始的なものであれば、（上記で$C=\mathrm{\perp }$とした形の）完全な爆発律もまた同様に$\mathrm{\perp }\to B$として表せる。

以下は、最小論理においてなお成り立つ定理を示す簡潔な議論であり、しばしば妥当なカリー化規則と演繹定理を暗黙のうちに用いる。

含意と否定

含意導入により$C\to (B\to C)$が成り立ち、したがって$C=\mathrm{\perp }$とすることで$\mathrm{\perp }\to (B\to \mathrm{\perp })$、すなわち

$$\mathrm{\perp }\to \mathrm{\neg }B.$$

が成り立つ。同様に、

$$B\to \mathrm{\neg }\mathrm{\neg }B$$

は、命題形$B\to ((B\to C)\to C)$におけるモーダスポネンスから直接導出できる。 これを、（下記の）妥当な対偶原理と組み合わせると、否定命題の安定性も導かれる。

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

$\mathrm{\neg }B$と同値な第2の式は、フレーゲの定理から従う。

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

これはさらに、コンセクエンティア・ミラビリスの弱い妥当な形、$(\mathrm{\neg }B\to \mathrm{\neg }\mathrm{\neg }B)\leftrightarrow \mathrm{\neg }\mathrm{\neg }B$を含意する。言葉で言えば、これはある命題が斥けられえないのは、まさにその命題の否定が「その命題は斥けられえない」ことを含意するとき、ということを述べている。

二重否定導入は

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

を含意し、逆に、$B=\mathrm{\neg }\mathrm{\neg }A$とした特殊な場合として、これによっても含意される。 本節の残りでは、上記の最初の3つの定理を、それぞれ2つの命題変数を含む、いくつかのより強い妥当な定理の特殊な場合として再導出する。

まず、否定を含まない含意計算における採用済みの原理については、ヒルベルト系のページで、同一律・含意導入・モーダスポネンスの一変種の命題形を通じて提示されている。そこでは同値式$(B\to (A\to C))\leftrightarrow (A\to (B\to C))$が証明されている。最初の導出として、ここで$C=\mathrm{\perp }$とすると、直ちに次の図式が得られる。

$$(B\to \mathrm{\neg }A)\leftrightarrow (A\to \mathrm{\neg }B)$$

「直観主義的」ヒルベルト系において、$\mathrm{\perp }$を定数として導入しない場合、これは否定を特徴づける第2の公理としても採用しうる（もう一方は爆発律である）。 ここで$A$をそれぞれ$\mathrm{\perp }$および$\mathrm{\neg }B$とすると、上式はそれぞれ$\mathrm{\perp }\to \mathrm{\neg }B$および$B\to \mathrm{\neg }\mathrm{\neg }B$という形の爆発律を実際に示す。

第二に、二重否定導入は同様に、次の式の特殊な場合$B=\mathrm{\neg }A$からも従う。

$$(\mathrm{\neg }\mathrm{\neg }A\to \mathrm{\neg }B)\leftrightarrow (A\to \mathrm{\neg }B)$$

これは上の両定理に近い。一般に$(([A\to C]\to C)\to (B\to C))\leftrightarrow (A\to (B\to C))$が成り立つ。特殊な場合$([(B\to C)\to C]\to C)\leftrightarrow (B\to C)$は、それ自体が否定命題の安定性の一般化である。後者は$([(B\to C)\to C]\to D)\to (B\to D)$からも別途導かれる。カリー＝ハワード同型対応のもとでは、ここでの最後の定理は、ラムダ式$\lambda f^{((B\to C)\to C)\to D}.\lambda b^B.f(\lambda g^{B\to C}.g(b))$によっても正当化できる。ここではこの手法をこの定理の一つについて示すにとどめる。

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

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

が得られる。また$A\to (B\leftrightarrow (A\to B))$は同様に

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

を含意する。ここから、$B=A$として二重否定含意も従う。 最後に、最小論理において対偶

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

は、$(B\to A)\to ((A\to C)\to (B\to C))$から証明できる。 ここから、任意の$B$について$A\to (\mathrm{\neg }A\to \mathrm{\neg }B)$が成り立つことがわかる。したがってこれは、否定導入と同様に、$(A\wedge \mathrm{\neg }A)\to \mathrm{\neg }B$も証明する。これらから、再び$\mathrm{\perp }\to \mathrm{\neg }B$も得られる。二重否定含意はまた、弱いコンセクエンティア・ミラビリスを用いて、$A\to (\mathrm{\neg }A\to \mathrm{\neg }B)$における$B=\mathrm{\neg }A$からも従う。

連言と選言

含意のみによる命題を超えて、これまで論じてきた原理は定理としても確立できる。$\mathrm{\perp }$による否定の定義を用いると、$(A\wedge (A\to C))\to C$という形のモーダスポネンス命題自体が、$C=\mathrm{\perp }$を考えることで「無矛盾原理」に特化する。否定が含意であるとき、無矛盾のカリー化された形は再び$A\to \mathrm{\neg }\mathrm{\neg }A$である。 さらに、前節で詳述した連言を伴う形での否定「導入」は、$(B\to (A\wedge (A\to C)))\to (B\to C)$の単なる特殊な場合として含意される。 このように、最小論理は否定「除去」（すなわち爆発律）だけを欠いた構成的論理として特徴づけることができる。

これにより、2つの命題の連言に関わるほとんどの一般的な直観主義的含意も、カリー化の同値式を含めて得られる。次の重要な同値式

$$((A\vee B)\to C)\leftrightarrow ((A\to C)\wedge (B\to C))$$

は強調に値する。これは、$A$と$B$の双方が$C$を含意すると言うことの、2つの同値な表現であることを示している。ここから、おなじみのド・モルガンの法則のうち2つが得られる。

$$\mathrm{\neg }(A\vee B)\leftrightarrow (\mathrm{\neg }A\wedge \mathrm{\neg }B).$$

3つ目の妥当なド・モルガンの法則も導出できる。

排中律命題の否定は、それ自体の妥当性を含意する。上記の弱いコンセクエンティア・ミラビリスの変種を踏まえると、次のことが従う。

$$\mathrm{\neg }\mathrm{\neg }(B\vee \mathrm{\neg }B)$$

この結果は、$((B\vee (B\to C))\to C)\to C$の特殊な場合とも見なせる。これは、$A$に$B\to C$を考えることで$((A\vee B)\to C)\to (B\to C)$から従う。

もう一つ、やや具体的な特殊な場合として、$((A\vee \mathrm{\perp })\to A)\leftrightarrow (\mathrm{\perp }\to A)$があり、これは素朴な選言律が爆発律とどのように結びついているかを既に示唆している。この話題は後段で詳しく論じる。

同様に、任意の$A$について、場合分けによって$(B\vee A)\wedge (A\to B)$が単に$B$と同値であることが示せる。特に$(B\vee \mathrm{\neg }B)\wedge (\mathrm{\neg }B\to B)$は$B$と同値である。同様に、$(B\vee (B\to C))\wedge ((B\to C)\to C)$は$B\vee C$と同値である。そして特に、$(B\vee \mathrm{\neg }B)\wedge \mathrm{\neg }\mathrm{\neg }B$は$B\vee \mathrm{\perp }$と同値であるが、これは一般には単に$B$と同値ではない。そして同様に、最小論理において救い出されるのは次の含意である。

$$((B\vee \mathrm{\neg }A)\wedge \mathrm{\neg }\mathrm{\neg }A)\to ((B\vee \mathrm{\neg }B)\wedge \mathrm{\neg }\mathrm{\neg }B))$$

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

直観主義論理は$(A\to B)\to (\mathrm{\neg }A\vee B)$を証明せず、また$(A\wedge \mathrm{\neg }A)\to B$なしには逆方向も証明できない。したがって、導出規則（resolution rule）のすべての形が最小論理において妥当なわけではない。

代替原理による公理化

上記の原理はすべて、正の計算からの定理と定数$\mathrm{\perp }$を組み合わせることで得られる。この定数を用いた定式化の代わりに、対偶原理$(B\to A)\to (\mathrm{\neg }A\to \mathrm{\neg }B)$と、二重否定原理$B\to \mathrm{\neg }\mathrm{\neg }B$を公理として採用することもできる。これにより、直観主義論理の正のフラグメントの上に、最小論理の代替的な公理化が与えられる。

古典論理との関係

$\mathrm{\neg }A$を$A\to C$へと一般化する手法は、二重否定を含むすべての古典的に妥当な命題を証明するためには機能しない。とりわけ、驚くには当たらないことだが、二重否定除去 $\mathrm{\neg }\mathrm{\neg }B\to B$の素朴な一般化は、この方法では証明できない。実際、$A$がどのようなものであっても、$(A\to C)\to B$という統語形式のいかなる図式も強すぎる。$C$として任意の真である命題を考えると、これは単に$B$と同値になってしまうからである。

命題$\mathrm{\neg }\mathrm{\neg }(B\vee \mathrm{\neg }B)$は最小論理の定理であり、$(A\wedge \mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }B$も同様である。したがって、最小論理において完全な二重否定原理$\mathrm{\neg }\mathrm{\neg }B\to B$を採用すると、実際には爆発律も証明されてしまい、その結果、計算はすべての中間論理を飛び越えて古典論理へと戻ってしまう。

上で見たように、任意の命題についての二重否定された排中律は、最小論理においてすでに証明可能である。しかし強調すべきは、述語計算においては、より強い直観主義論理の法則をもってしても、排中律命題の無限連言の二重否定を証明することはできないという点である。実際、

$$⊬\mathrm{\neg }\mathrm{\neg }\mathrm{\forall }(n\in \mathbb{N}).Q(n)\vee \mathrm{\neg }Q(n)$$

同様に、二重否定シフト図式（DNS）も妥当ではない。すなわち

$$⊬(\mathrm{\forall }(n\in \mathbb{N}).\mathrm{\neg }\mathrm{\neg }P(n))\to \mathrm{\neg }\mathrm{\neg }\mathrm{\forall }(n\in \mathbb{N}).P(n)$$

算術を超えて、この証明不可能性は非古典的理論の公理化を可能にする。

矛盾許容論理との関係

排中律は矛盾許容論理においてはしばしば妥当であるが、最小論理ではそうではない。最小論理においては、これはコンセクエンティア・ミラビリスと同値であることが示せる。

最小論理が証明するのは、排中律の二重否定と、上記で用いられ、その項目自体で示されているコンセクエンティア・ミラビリスの弱い変種のみである。

適切さの論理との関係

最小論理は弱化律を証明する。すなわち、命題形$C\to (B\to C)$における含意導入を認める。 この原理は演繹定理の導出において役割を果たす。

同一律$A\to A$は非常に弱い論理においても成り立つ。これを用いると、最小論理では弱化律をさらに用いて$B\to (A\to A)$を証明できる。

例えば弱化律を証明する点で、最小論理は関連性論理とは異なる。したがって当然ながら、ここで論じている論理は形式的な意味での「最小」ではない。

直観主義論理との関係

$\wedge ,\vee ,\to$のみを用いる任意の論理式は、直観主義論理において証明可能な場合に限り、最小論理においても証明可能である。 しかし、最小論理では証明不可能でありながら、直観主義的には成り立つ命題論理の命題も存在する。

爆発律は直観主義論理において妥当であり、あらゆる命題を導出するには、何らかの不条理を導出しさえすればよいことを表す。最小論理では、この原理は任意の命題について公理的には成り立たない。最小論理は直観主義論理の正のフラグメントのみを表すため、それは直観主義論理の部分体系であり、厳密により弱い。両方の論理とも選言性を持つ。

否定された命題についての爆発律があれば、完全な爆発律はその特殊な場合$((\mathrm{\neg }B)\wedge \mathrm{\neg }(\mathrm{\neg }B))\to B$と同値である。後者は、斥けられた命題についての二重否定除去、$\mathrm{\neg }B\to (\mathrm{\neg }\mathrm{\neg }B\to B)$として言い換えられる。簡潔に言えば、直観主義論理における爆発律は、最小論理が持たない二重否定除去原理の特定の場合をまさに与えるものである。 この含意はまた、次節で見る完全な選言三段論法も直ちに含意する。

選言三段論法

実践的には、直観主義的な文脈において、爆発律の原理は次のような単一の命題の形で選言三段論法を証明することを可能にする。 $$((A\vee B)\wedge \mathrm{\neg }A)\to B.$$ これは以下のように読める。$A\vee B$の構成的な証明と、$A$の構成的な拒絶が与えられれば、無条件に$B$という肯定的な場合の選択が許される。ここではその二重否定だけではない。 このように、三段論法は選言に対する展開原理である。これは爆発律の形式的な帰結と見なすことができ、同時にそれを含意もする。なぜなら、もし$A\vee B$が$B$を証明することによって証明されたのであれば、$B$は既に証明されており、一方もし$A\vee B$が$A$を証明することによって証明されたのであれば、直観主義的な体系は爆発律を許すため、$B$もまた従うからである。

例えば、コイン投げの結果が表か裏のいずれか（$A$または$B$）であったという構成的な論証と、その結果が実際には表ではなかったという構成的な論証が与えられれば、この三段論法を表す命題は、これがすでに裏が出たという論証を構成することを表している。

もし直観主義論理の体系がメタ論理的に無矛盾であると仮定されるならば、この三段論法は、$B$を示す他の非論理的公理が存在しない場合、$A\vee B$と$\mathrm{\neg }A$の構成的な論証が実際には$B$の論証を含んでいる、と読むことができる。

ヨハンソンは自身の論文の中で、たとえ$((A\vee B)\wedge \mathrm{\neg }A)\to B$が最小論理の定理でなくとも、$(A\vee B)\wedge \mathrm{\neg }A$の証明可能性から$B$の証明可能性が従うことを証明している。したがってこの段階は、いわゆる推論の許容規則である。彼の証明は、直観主義論理のためのゲンツェンのシークエント計算を用いている。

爆発律の弱い形は選言三段論法を証明し、逆方向にも、$A=\mathrm{\neg }B$とした三段論法の事例は$((B\vee \mathrm{\neg }B)\wedge \mathrm{\neg }\mathrm{\neg }B)\to B$と読め、排中律が成り立つ命題についての二重否定除去と同値である。 $$(B\vee \mathrm{\neg }B)\to (\mathrm{\neg }\mathrm{\neg }B\to B).$$ 実質条件法が証明された命題について二重否定除去を与えるように、これもまた斥けられた命題についての二重否定除去と同値である。

最後に、爆発律があれば、直観主義論理では$A\vee (\mathrm{\perp }\to P)$が任意の$A$について自明に成り立つ。例えば、この選言は$A=\mathrm{\perp }$という偽の選言肢（それ自体は古典論理においてすら証明可能ではない）についても直観主義的に証明可能である。最小論理では一般に、2つの選言肢のどちらも証明されない。

理論における使用の直観主義的な例

次のヘイティング算術の定理は、爆発律の原理なしには、この一般的な結果によっては証明できない存在主張の証明を可能にする。この結果は本質的に、計算可能な述語を束縛する$\mathrm{\exists }$命題についての、単純な二重否定除去の主張の族である。

$P$を任意の量化子を含まない述語とし、したがってすべての数$n$について決定可能であるとすると、排中律が成り立つ。

$$P(n)\vee \mathrm{\neg }P(n).$$ すると$m$についての帰納法により、

$$\mathrm{\forall }m.\mathrm{\neg }(\mathrm{\forall }(n<m).\mathrm{\neg }P(n))\to \mathrm{\exists }(b<m).P(b)$$ 言葉で言えば、$m$までの有限範囲内の数$n$について、どの場合も成り立たないということが排除できる場合、すなわち、すべての数、例えば$n=a$について、対応する命題$P(a)$が常に反証可能であるということが排除できるならば、それはこれらの$n$の中に$P(b)$が証明可能であるような$n=b$が存在することを含意する、ということである。

これまでに論じた例と同様に、この証明には、否定を含まない命題を得るために、前提側での爆発律が必要となる。 命題が$m=0$から始まるものとして定式化される場合、この最初の場合はすでに、空虚な節からの爆発律の一形態を与える。 $$\mathrm{\perp }\to \mathrm{\exists }(b<0).P(b).$$ 次の場合$m=1$は、決定可能な述語についての二重否定除去を述べる。 $$\mathrm{\neg }\mathrm{\neg }P(0)\to P(0).$$ $m=2$の場合は次のようになる。 $$\mathrm{\neg }(\mathrm{\neg }P(0)\wedge \mathrm{\neg }P(1))\to (P(0)\vee P(1)),$$ これはすでに述べたように、次と同値である。 $$\mathrm{\neg }\mathrm{\neg }(P(0)\vee P(1))\to (P(0)\vee P(1)).$$ $m=0$と$m=1$のいずれも、再び決定可能な述語についての二重否定除去の事例である。 もちろん、固定された$m$と$P$についての命題$\mathrm{\exists }(b<m).P(b)$は、最小論理の原理を用いて他の手段で証明可能な場合もある。

余談だが、一般の決定可能な述語についての非有界な図式は、直観主義的にすら証明可能ではない。マルコフの原理を参照。

型理論との関係

単純型

本節では、最小論理を含意のみに制限した体系について述べる。関数型プログラミングの計算体系は、真っ先に含意結合子に依存する。例えば述語論理の枠組みとしての構成の計算を参照。

この体系は次のシークエント規則によって定義できるテンプレート:Sfnテンプレート:Sfn。 $$\frac{}{\mathrm{\Gamma }\cup \{A\}⊢A}\text{ axiom}$$         $\frac{\mathrm{\Gamma }\cup \{A\}⊢B}{\mathrm{\Gamma }⊢A\to B}\text{ intro}$         $\frac{\mathrm{\Gamma }⊢A\to B\mathrm{\Delta }⊢A}{\mathrm{\Gamma }\cup \mathrm{\Delta }⊢B}\text{ elim.}$

この制限された最小論理の各論理式は、単純型付きラムダ計算における型に対応する（カリー＝ハワード同型対応を参照）。最小論理のこの含意的フラグメントは、直観主義論理の正の含意的フラグメントと同一であり、型理論の文脈では、しばしばそれ自体がすでに「最小論理」と呼ばれるテンプレート:Sfn。

否定の使用

不条理$\mathrm{\perp }$は、自然演繹においてだけでなく、カリー＝ハワード対応のもとでの型理論的な定式化においても用いられる。 型体系においては、$\mathrm{\perp }$はしばしば空型としても導入される。その命題についての証明の存在は、それ自体が矛盾を構成することになる。

算術

多くの文脈において、$\mathrm{\perp }$は論理における独立した定数である必要はなく、その役割は任意の斥けられた命題によって代替できる。例えばそれは、$a,b$が異なるはずであるような$a=b$として定義できる。その命題は、同じ記号$\mathrm{\perp }$によって表記されうる。このような定義は、素朴な構成的論理の上でも有益でありうる。

そのような$\mathrm{\perp }$の一例となる特徴づけは、自然数を含む理論における$0=1$である。ここで$\mathrm{\perp }$を仮定すると、任意の2つの与えられた数が等しいことが証明できる。例えば、$1=0$から$7=6+1=6+0=6$が従う。この形の証明は、論理的公理である爆発律がなくても可能である。ゆえに、$0=1$が導出できる算術は無矛盾でないと呼ばれる。

この定義を用いる文脈では、$3^4=8$が偽であること、すなわち$\mathrm{\neg }(3^4=8)$を証明することは、単に$(3^4=8)\to (0=1)$を証明することを意味する。この主張を捉えるために、$3^4\ne 8$という記法を導入してもよい。 そして実際、算術を用いると$\frac{3^4-8}{73}=1$が成り立つが、$(3^4=8)$はまた$\frac{3^4-8}{73}=0$も含意する。したがってこれは$1=0$を含意することになり、それゆえ$\mathrm{\neg }(3^4=8)$が得られる。証明終わり。

意味論

最小論理には、直観主義論理のフレーム意味論を反映する意味論が存在する。詳しくは矛盾許容論理における意味論の議論を参照のこと。ここでは、命題に真理値を割り当てる評価関数がより少ない制約に従うことができる。

関連項目

• 直観主義論理
• 矛盾許容論理
• 含意命題計算
• 論理学における公理系の一覧

出典

• テンプレート:Cite book
• テンプレート:Cite book
• テンプレート:Cite journal
• テンプレート:Cite web
• テンプレート:Cite book
• テンプレート:Cite book