直観主義論理のソースを表示

'''直観主義論理'''（ちょっかんしゅぎろんり、{{lang-en-short|intuitionistic logic}}）または'''直観論理'''（ちょっかんろんり）、あるいは'''構成的論理'''（こうせいてきろんり、{{lang-en-short|constructive logic}}）とは、ある種の論理体系であり、伝統的な[[真理値]]の概念が[[構成的証明]]の概念に置き換わっている点で[[古典論理]]とは異なる。例えば古典論理では、全ての[[論理式 (数学)|論理式]]に真か偽の真理値 ( <math>\{\top,\bot\}</math> ) が割り当てられる。このときその真理値に対する直接的なエビデンスを持つか否かは問題にしない。これはどのような曖昧な命題においても「真か偽かが決定可能である」ということを意味する。対照的に、直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。<!-- 訳注：これはBHK解釈のような意味論を意図しているのだろう。しかしこれだとハイティング代数値意味論のように拡張された意味の真理値を考えるような意味論を排除してはいないか。(By Phio: Heyting代数は代数論なので、素朴な意味論からは離れている。そのため元々のBrowerの着想からは拡大されたものであるので問題は無い) -->
<!--
(We can also say, instead of the propositional formula being "true" due to direct evidence, that it is [[Inhabited set|inhabited]] by a proof in the [[Curry–Howard correspondence|Curry–Howard]] sense.) Operations in intuitionistic logic therefore preserve [[Theory of justification|justification]], with respect to evidence and provability, rather than truth-valuation.

Unproved statements in Intuitionistic logic are not given an intermediate truth value (as is sometimes mistakenly asserted). One can prove that such statements have no third truth value, a result dating back to [[Valery Glivenko|Glivenko]] in 1928.<ref>[http://plato.stanford.edu/entries/intuitionistic-logic-development/#4.3 Proof that intuitionistic logic has no third truth value, Glivenko 1928]</ref> Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them.

A consequence of this point of view is that intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions <math>\{\top, \bot\}</math> from classical logic, each ''proof'' of a propositional formula is considered a valid propositional value, thus by [[Brouwer-Heyting-Kolmogorov|Heyting's]] notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs.
-->

証明論的な視点から見ると、直観主義論理は古典論理の制限であって[[排中律]]や[[二重否定除去]]が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。

直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的な[[ブール代数値意味論]]を写しとったもので[[ブール代数]]の代わりに[[ハイティング代数]]を用いる。別の意味論では[[クリプキ・モデル]]を用いる。

直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって[[存在具体性]]を持つ証明が作られるからであり、これは直観主義論理が[[数学的構成主義]]のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。

形式化された直観主義論理は[[アレン・ハイティング]]によって[[ヤン・ブラウワー]]の[[直観主義 (数学の哲学)|直観主義]]プログラムの形式的な基礎として発展せられたものである。

==構文論と証明体系==
[[File:Rieger-Nishimura.svg|thumb|right|280px|Rieger–Nishimura束のハッセ図。これのノードは変数をひとつだけ持つ命題論理式の直観主義的な同値性による同値類で、その順序は直観主義的な含意から誘導されるものである。]]
直観主義論理の論理式の構文は古典[[命題論理]]や古典[[述語論理]]と類似である。しかしながら、直観主義的な[[論理結合子]]は、[[古典論理]]におけるように、他の論理結合子を用いて定義することはできない。（そのため <math>\{\to,\bot\}</math>, <math>\{\wedge,\neg\}</math>, <math>\{\vee,\neg\}</math> などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に<math>\to,\wedge,\vee,\bot</math> を基本的な結合子として採用する。ここで <math>\neg A</math> は <math>A \to \bot</math> の省略形として扱う。直観主義述語論理ではこれに量化記号 <math>\exists,\forall</math> を加える。

多くの古典論理の[[恒真式]]は直観主義的には証明できない。[[排中律]] <math>p\vee \neg p</math> だけでなく[[パースの法則]] <math>((p\to q)\to p)\to p</math> や[[二重否定除去]] <math>\neg\neg p \to p</math> などがその例である。古典論理において二重否定導入 <math>p \to \neg\neg p</math> と二重否定除去 はともに定理である。直観主義論理においては前者のみが定理である。すなわち二重否定を導入することはできるが、除去することはできない。ただし三重否定除去 <math>\neg\neg\neg p \to \neg p</math> は定理である。排中律 <math>p \vee \neg p</math> の拒絶は古典論理に親しい者には奇妙に思われるが、直観主義論理で命題論理式を証明するには、全ての可能な命題論理式に対して真または偽の証明が要求され、これは様々な理由によって不可能である。

多くの古典論理で妥当な恒真式は直観主義論理では定理でないが、全ての直観主義論理で妥当な定理は古典論理に於いても妥当であるから、直観主義論理は古典論理を弱めたものであるという見方ができる。ただし直観主義論理は古典論理にはない良い性質を多く持っている。

===シークエント計算===
{{Main|シークエント計算}}
[[ゲルハルト・ゲンツェン|ゲンツェン]]は彼の体系LK（古典論理のシークエント計算）の簡単な制限として直観主義論理の健全かつ完全な体系が得られることを見つけた。彼はこの体系をLJと呼んだ。LKにおいて任意個の論理式がシークエントの結論（右側）に来ることを許すが、LJにおいては高々ひとつの論理式だけを許す。この結果として例えば含意右の適用において直観主義的に許容できない推論が禁じられることから、直観主義論理の体系が得られるのである。（右辺が複数であることを許すと含意右を用いて α→α,⊥ から →α,￢α が得られ、排中律が導かれる。右辺を制限した結果として含意右が制限されて直観主義論理の体系が得られる。）

LKを制限して得られる直観主義論理の体系で結論が複数であることを許容するものもある。LJ'<ref>Proof Theory by G. Takeuti, ISBN 0-444-10492-5</ref>はその例である。

=== ヒルベルト流の計算 ===
直観主義論理は次のように[[ヒルベルト流の計算]]を用いても定義できる。これは古典命題論理の公理化（[[命題論理|Propositional calculus#Alternative calculus]]）に類似である。

命題論理では、推論規則として[[モーダスポネンス]]
* MP: <math>\phi</math> および <math>\phi \to \psi</math> から <math>\psi</math> を導く
を取り、公理図式として次のものを取る：
* THEN-1: <math>\phi \to (\chi \to \phi )</math>
* THEN-2: <math>(\phi \to (\chi \to \psi )) \to ((\phi \to \chi ) \to (\phi \to \psi ))</math>
* AND-1: <math>\phi \land \chi \to \phi </math>
* AND-2: <math>\phi \land \chi \to \chi </math>
* AND-3: <math>\phi \to (\chi \to (\phi \land \chi ))</math>
* OR-1: <math>\phi \to \phi \lor \chi </math>
* OR-2: <math>\chi \to \phi \lor \chi </math>
* OR-3: <math>(\phi \to \psi ) \to ((\chi \to \psi ) \to (\phi \lor \chi \to \psi ))</math>
* FALSE: <math>\bot \to \phi </math>
一階述語論理の体系を作るには次の推論規則を加える：
* <math>\forall </math>-GEN: <math>\psi \to \phi </math> から <math>\psi \to (\forall x \ \phi )</math> を導く；ただし固有変数条件「<math>x</math> は <math>\psi </math> に自由に現れない」を満たす
* <math>\exists </math>-GEN: <math>\phi \to \psi </math> から <math>(\exists x \ \phi ) \to \psi </math> を導く；ただし固有変数条件「<math>x</math> は <math>\psi </math> に自由に現れない」を満たす
また次のものを公理図式に加える：
* PRED-1: <math>(\forall x \ \phi (x)) \to \phi (t)</math> ただし項 ''t'' は <math>\phi</math> の中の ''x'' への代入について自由である (つまり ''t'' の中の変数記号は <math>\phi (t)</math> の中で束縛されていない)
* PRED-2: <math>\phi (t) \to (\exists x \ \phi (x))</math> ただしPRED-1と同様の条件を満たす

==== オプションの結合子 ====

===== 否定 =====
もし否定を表す結合子 <math>\lnot </math> を <math>\phi \to \bot </math> なる省略形の代わりに導入したいならば、次を公理に加えれば十分である：
* NOT-1': <math>(\phi \to \bot ) \to \lnot \phi </math>
* NOT-2': <math>\lnot \phi \to (\phi \to \bot )</math>

否定を導入した代わりに偽を表す命題定数 <math>\bot </math> を落としたいならば次のようにする。まず FALSE, NOT-1', NOT-2' を次の公理に置き換える：
* NOT-1: <math>(\phi \to \chi ) \to ((\phi \to \lnot \chi ) \to \lnot \phi )</math>
* NOT-2: <math>\phi \to (\lnot \phi \to \chi )</math>
NOT-1の代替としては <math>(\phi \to \lnot \chi ) \to (\chi \to \lnot \phi )</math> または <math>(\phi \to \lnot \phi ) \to \lnot \phi </math> などがある。

===== 同値 =====
同値を表す結合子 <math>\leftrightarrow </math> は <math>\phi \leftrightarrow \chi </math> standing for <math>(\phi \to \chi ) \land (\chi \to \phi )</math> の省略形として導入できる。代わりに次の公理を追加してもよい：

* IFF-1: <math>(\phi \leftrightarrow \chi ) \to (\phi \to \chi )</math>
* IFF-2: <math>(\phi \leftrightarrow \chi ) \to (\chi \to \phi )</math>
* IFF-3: <math>(\phi \to \chi ) \to ((\chi \to \phi ) \to (\phi \leftrightarrow \chi ))</math>

IFF-1とIFF-2は一つの公理 <math>(\phi \leftrightarrow \chi ) \to ((\phi \to \chi ) \land (\chi \to \phi ))</math> に結合できる。

==== 古典論理との関係 ====
古典論理の体系は次のどれかを公理に追加することによって得られる：

* <math>\phi \lor \lnot \phi </math> （排中律。これは <math>(\phi \to \chi ) \to ((\lnot \phi \to \chi ) \to \chi )</math> とも定式化できる。）
* <math>\lnot \lnot \phi \to \phi </math> （二重否定除去）
* <math>((\phi \to \chi ) \to \phi ) \to \phi </math> （パースの法則）

一般に、古典論理の恒真式で二元[[クリプキ・フレーム]] <math>\circ{\longrightarrow}\circ</math> で妥当でない公理を追加したもの（言い換えれば[[中間論理|Smetanich論理]]に含まれないもの）を考えれば、これは古典論理に等しい。Smetanich論理は古典論理よりも弱く直観主義論理より強い論理の中で極大なものだからである。

別の関係性としては[[ゲーデル＝ゲンツェン変換]]によるものがある。これは古典一階述語論理が直観主義一階述語論理に埋め込めることを示す。すなわち一階述語論理式が古典論理で証明可能であることと、それをゲーデル・ゲンツェン変換したものが直観主義論理で証明可能であることとが同値となる。また[[グリベンコの定理]]によれば、命題論理式が古典論理で証明可能であることと、それを二重否定したものが直観主義論理で証明可能であることとは同値である。したがって直観主義論理は古典論理を構成的意味論の観点から拡大したものと見做すことができる。

1932年に[[クルト・ゲーデル]]は古典論理と直観主義論理の間にあるゲーデル論理の体系を定義した。これは中間論理として知られる。

===結合子の定義不可能性===
古典命題論理において、[[論理積]]、[[論理和]]または[[実質含意]]を基本的なものとすれば、他は[[否定]]を用いて[[ウカシェヴィッチ]]の[[命題論理]]のようにして定義できる。またこれら4つを[[パースの矢印]]（NOR）や[[シェファーの棒]]（NAND）のようなただひとつの論理結合子を用いて定義することもできる。同様に、古典一階述語論理において、一方の量化子は他方と否定を用いて定義できる。

これらは全ての結合子は[[ブール関数]]であるという[[二値原理]]からの基本的な帰結である。二値原理は直観主義論理においては成り立たない。ただ[[無矛盾律]]だけが成り立つ。結果として、いかなる結合子も不要ではなく、上に述べたどの公理も必要であることが分かる。古典論理において成立する同値性は、直観主義論理においては、幾つかは成り立つけれども、多くは一方の含意だけが成り立つ。次のようなものがある：

論理積と論理和：
* <math>(\phi \wedge \psi) \to \neg (\neg \phi \vee \neg \psi)</math>
* <math>(\phi \vee \psi) \to \neg (\neg \phi \wedge \neg \psi)</math>
* <math>(\neg \phi \vee \neg \psi) \to \neg (\phi \wedge \psi)</math>
* <math>(\neg \phi \wedge \neg \psi) \leftrightarrow \neg (\phi \vee \psi)</math>
論理積と含意：
* <math>(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)</math>
* <math>(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)</math>
* <math>(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)</math>
* <math>(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi) </math>
論理和と含意：
* <math>(\phi \vee \psi) \to (\neg \phi \to \psi)</math>
* <math>(\neg \phi \vee \psi) \to (\phi \to \psi)</math>
全称量化と存在量化：
* <math>(\forall x \ \phi(x)) \to \neg (\exists x \ \neg \phi(x))</math>
* <math>(\exists x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))</math>
* <math>(\exists x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))</math>
* <math>(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exists x \ \phi(x))</math>

すると、例えば、 "a or b" は "if not a, then b" よりも強い主張となる。これは古典論理において同値であることと対照的である。他方で "not (a or b)" と "not a, and also not b" は同値となる。

同値を結合子のリストに入れるならば、いくつかの結合子は他から定義できる：
* <math>(\phi\leftrightarrow \psi) \leftrightarrow ((\phi \to \psi)\land(\psi\to\phi))</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\lor\psi) \leftrightarrow \psi)</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\land\psi) \leftrightarrow \phi)</math>
* <math>(\phi\land\psi) \leftrightarrow ((\phi\to\psi)\leftrightarrow\phi)</math>
* <math>(\phi\land\psi) \leftrightarrow (((\phi\lor\psi)\leftrightarrow\psi)\leftrightarrow\phi)</math>
とりわけ <math>\{\vee,\leftrightarrow\bot\}</math> と <math>\{\vee,\leftrightarrow\neg\}</math> は直観主義的結合子の完全な基底となる。

<!--
As shown by Alexander Kuznetsov, either of the following connectives – the first one ternary, the second one quinary – is by itself [[functionally complete]]: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the [[Sheffer stroke]] from classical propositional logic:<ref>Alexander Chagrov, Michael Zakharyaschev, ''Modal Logic'', vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59. ISBN 0-19-853779-4.</ref>
* <math>((p\lor q)\land\neg r)\lor(\neg p\land(q\leftrightarrow r)),</math>
* <math>p\to(q\land\neg r\land(s\lor t)).</math>
-->

==意味論==
直観主義論理の意味論は古典論理のそれよりも複雑である。直観主義論理のモデル論は[[ハイティング代数]]や[[クリプキ意味論]]として与えられている。最近では[[タルスキ流のモデル論]]の完全性が[[Robert Lee Constable|Bob Constable]]によって証明せられた。ただしこの完全性は通常の意味のそれとは異なる。

===ハイティング代数意味論===
古典論理において、我々はしばしば論理式の取る[[真理値]]について議論する。この値は普通は[[ブール代数]]の元から選ぶ。ブール代数の交わりと結びは論理結合子の <math>\wedge</math> と <math>\vee</math> に同一視される。そして <math>A\wedge B</math> の真理値は <math>A</math> と <math>B</math> の真理値のブール代数における交わりとする。このとき論理式が古典論理において妥当であることと、任意のブール代数とその上で値を取る真理値割り当てに対して論理式の真理値が <math>\top</math> であることとが同値となる。

直観主義論理においても同様の完全性定理が成立するが、論理式の真理値はブール代数の代わりにハイティング代数の元を用いる。ブール代数はハイティング代数の特別な場合である。このとき論理式が直観主義論理で妥当であることと、任意のハイティング代数とその上で値を取る真理値割り当てに対して論理式の真理値が <math>\top</math> であることは同値である。<!-- 訳注: このとき有限ハイティング代数だけを考えればよいことが分かる。直観主義論理で証明できない論理式に対しては有限ハイティング代数で反駁を構成できる。これを直観主義論理の有限モデル特性という。 -->

論理式が妥当であることを確かめる為には、ひとつのハイティング代数の上で調べれば十分であることが証明できる。そのハイティング代数は数直線 <math>\mathbb{R}</math> の開部分集合からなるハイティング代数である。<ref name="S-U">{{cite book | title = Lectures on the Curry-Howard Isomorphism | last = Sørensen | first = Morten Heine B |author2=Paweł Urzyczyn | year = 2006 | publisher = [[Elsevier]] | isbn = 0-444-52077-5 | series = Studies in Logic and the Foundations of Mathematics | page = 42 }}</ref> この代数系において、<math>\wedge</math> と <math>\vee</math> は集合の交わりと結びである。また <math>A\to B</math> は <math>\mathrm{int}(A^c \cup B)</math> すなわち <math>A</math> の補集合と <math>B</math> との和集合の[[開核作用素|内部]]である。（これは古典論理における含意の演算の結果を開集合になるように調整したものである。様相論理の観点から見るとこれは必然性を外側に付けているのと同じことになる。）<math>\bot</math> は空集合 <math>\varnothing</math> であり、<math>\top</math> は全体集合 <math>\mathbb{R}</math> である。否定 <math>\neg A</math> は <math>A \to \bot</math> と定義されるが、これは <math>A</math> の補集合の開核すなわち[[外部]]と一致する。この対応付けによって直観主義的に妥当な論理式はちょうど空間全体が割り当てられるものと一致する。<ref name="S-U"/>

例えば矛盾律 <math>\neg (A\wedge \neg A)</math> は妥当である。なぜなら開集合 <math>X</math> を <math>A</math> の付値としてどのように選んでも <math>\neg (A\wedge \neg A)</math> の値は次のように直線全体となるからである：

<math>\mathrm{val}(\neg (A\wedge \neg A)) = \mathrm{int}((X \wedge \mathrm{int}(X^c))^c)</math>

[[位相空間論]]によれば <math>\mathrm{int}(X^c)</math> は <math>X^c</math> の部分集合であり、<math>X</math> との共通部分は空であるから、

: <math>\mathrm{int}(\varnothing^c) = \mathrm{int}(\mathbb{R}) = \mathbb{R}</math>

したがってこの論理式の付値は真であり、妥当であることが従う。

しかし排中律 <math>A\vee\neg A</math> は非妥当である。それには <math>A</math> に <math>(0,\infty)</math> を割り当てるとよい。すると <math>\neg A</math> の付値は <math>(-\infty, 0 ]</math> の内部、すなわち <math>(-\infty,0)</math> であり、目的の論理式の付値は <math>(0,\infty)</math> および <math>(-\infty,0)</math> の和集合、すなわち <math>\mathbb{R}\setminus\{0\}</math> となる。これは空間全体に一致しない。

数直線からハイティング代数を作る上のやり方は任意の位相空間に対しても適用できる。位相空間論では閉包の開核がもとと一致する集合を[[正則開集合]]という。これはこのハイティング代数における二重否定で不変な集合と同じものである。正則開集合の全体は（完備）ブール代数を成す。これは古典論理が二重否定によって直観主義論理に埋め込めるという[[グリベンコの定理]]に対応している。
<!--
The [[interpretation (logic)|interpretation]] of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula.<ref name="S-U"/> Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element.<ref>Alfred Tarski, ''Der Aussagenkalkül und die Topologie'', Fundamenta Mathematicae 31 (1938), 103–134. [http://matwbn.icm.edu.pl/tresc.php?wyd=1&tom=31]</ref><ref name="R-S">{{cite book | title = The Mathematics of Metamathematics | last = Rasiowa | first = Helena |author2=Roman Sikorski | year = 1963 | publisher = Państwowe Wydawn. Naukowe | isbn = | location = Warsaw |series =  Monografie matematyczne | pages = 385–386 }}</ref> No finite Heyting algebra has both these properties.<ref name="S-U"/>
-->

===クリプキ意味論===
{{Main|クリプキ意味論}}
<!--
Building upon his work on semantics of [[modal logic]], [[Saul Kripke]] created another semantics for intuitionistic logic, known as '''Kripke semantics''' or '''relational semantics'''.<ref name=Mosch-IntLog>[http://plato.stanford.edu/entries/logic-intuitionistic/ Intuitionistic Logic]. Written by [http://www.math.ucla.edu/~joan/ Joan Moschovakis]. Published in Stanford Encyclopedia of Philosophy.</ref>
-->

===タルスキ流のモデル論===
<!--
It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, [[Robert Lee Constable|Robert Constable]] has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true ''in the same way'' in every model. That is, a single proof that the model judges a formula to be true must be valid for every model. In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic.<ref>{{cite journal | last1 = Constable | first1 = R. | last2 = Bickford | first2 = M. | year = | title = Intuitionistic completeness of first-order logic | journal = Annals of Pure and Applied Logic | volume = | issue = | page = | doi = 10.1016/j.apal.2013.07.009 | arxiv=1110.1614 }}</ref>
-->

=== 他の論理との関係 ===
直観主義論理の双対<ref group="注">ここでの双対はシークエント計算においての双対である。</ref>は双対直観論理（{{Lang-en-short|dual-intuitionistic logic}}）である<ref>{{Cite journal |last=Urbas |first=Igor |date=1996-07-01 |title=Dual-Intuitionistic Logic |url=https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-37/issue-3/Dual-Intuitionistic-Logic/10.1305/ndjfl/1039886520.full |journal=Notre Dame Journal of Formal Logic |volume=37 |issue=3 |doi=10.1305/ndjfl/1039886520 |issn=0029-4527}}</ref>。双対直観論理は[[矛盾許容論理]]の一種であり、ブラジリアン論理（{{Lang-en-short|Brazilian logic}}）、反直観主義論理（{{Lang-en-short|anti-intuitionistic logic}}）などと呼ばれる論理と対応している<ref>{{Cite journal |author=Aoyama, Hiroshi |year=2004 |title=LK, LJ, Dual Intuitionistic Logic, and Quantum Logic |journal=Notre Dame Journal of Formal Logic |volume=45 |issue=4 |pages=193–213 |doi=10.1305/ndjfl/1099238445}}</ref>。

直観主義論理から{{仮リンク|爆発律|en|Principle of explosion|label=爆発原理}}の公理を取り除いたものは{{仮リンク|最小論理|en|Minimal logic}}として知られる。

==== 多値論理との関係 ====
[[クルト・ゲーデル]]は1932年に直観主義論理が[[多値論理]]ではないことを証明した。（[[#ハイティング代数意味論]]は直観主義論理の"無限多値論理"としての解釈の一種と見られる。）

==== 中間論理との関係 ====
任意の有限ハイティング代数でブール代数でないものは（意味論的に）[[中間論理]]を定める。他方で、純粋な直観主義論理における論理式の妥当性は、特定のハイティング代数に結びついたものではなく、あらゆるハイティング代数に関係している。

==== 様相論理との関係 ====
直観主義命題論理の論理式は次のように[[様相論理|様相命題論理S4]]の論理式に翻訳できる：

{|
|-
| <math>\bot^*</math>
| =
| &nbsp;&nbsp;<math>\ \bot</math>
|-
| <math>A^*</math> 
| =
| &nbsp;&nbsp;<math>\ \Box A \qquad \hbox{if } A \hbox{ is prime (a positive literal)}</math>
|-
| <math>(A \wedge B)^*</math>
| =
| &nbsp;&nbsp;<math>\ A^* \wedge B^*</math>
|-
| <math>(A \vee B)^*</math>
| =
| &nbsp;&nbsp;<math>\ A^* \vee B^*</math>
|-
| <math>(A \rightarrow B)^*</math>
| =
| &nbsp;&nbsp;<math>\ \Box(A^* \rightarrow B^*)</math>
|-
| <math> (\neg A)^*</math>
| =
| &nbsp;&nbsp;<math>\ \Box(\neg (A^*)) \qquad \hbox{since } \neg A := A \rightarrow \bot</math>
|}
またこれにより直観主義論理を模倣できる<ref>{{Cite web |url=http://teachinglogic.liglab.fr/INT1/S4Lint.pdf |title=Logique modale propositionnelle S4 et logique intuitioniste propositionnelle |access-date=2015年5月8日 |last=Lévy |first=Michel |date=2011-04-29 |format=PDF |pages=4–5}}</ref>。すなわち翻訳された論理式が様相命題論理S4で妥当であることと、翻訳前の論理式が直観主義命題論理IPCで妥当であることは同値である。上のような変換は[[ゲーデル＝マッキンゼー＝タルスキ変換]]と呼ばれる。

様相論理S4の直観主義版は構成的様相論理CS4と呼ばれる<ref name="categorical">{{Cite web |url=http://www.cs.nott.ac.uk/~nza/papers/Alechina++:01a.pdf |title=Categorical and Kripke Semantics for Constructive S4 Modal Logic |access-date=2015年5月8日 |author=Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter |format=PDF}}</ref>。

===ラムダ計算===
[[カリー＝ハワード対応]]はIPCと直和と直積を持つ[[単純型付きラムダ計算]]との間に拡張できる。<ref name=categorical />

==関連項目==
* {{仮リンク|BHK解釈|en|BHK interpretation}}
* {{仮リンク|直観主義的型理論|en|Intuitionistic type theory}}
* [[直観主義 (数学の哲学)]]
* [[中間論理]]
* [[線形論理]]
* {{仮リンク|構成的証明|en|Constructive proof}}
* [[カリー＝ハワード対応]]
* {{仮リンク|計算可能性論理|en|Computability logic}}
* [[ゲーム意味論]]
* {{仮リンク|Smooth infinitesimal analysis|en|Smooth infinitesimal analysis}}
{{colend}}

== 脚注 ==
{{脚注ヘルプ}}

=== 注釈 ===
{{Notelist2}}

=== 出典 ===
{{Reflist}}

==参考文献==
{{refbegin}}
*[[前原昭二]]『[[数学基礎論]]』財団法人放送大学教育振興会
* [[Dirk van Dalen|van Dalen, Dirk]], 2001, "Intuitionistic Logic", in Goble, Lou, ed., ''The Blackwell Guide to Philosophical Logic''. Blackwell.
* Morten H. Sørensen, Paweł Urzyczyn, 2006, ''Lectures on the Curry-Howard Isomorphism'' (chapter 2: "Intuitionistic Logic").  Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier.
*W. A. Carnielli (with A. B.M. Brunner).[https://doi.org/10.1016/j.jal.2004.07.016 "Anti-intuitionism and paraconsistency"].  Journal of Applied Logic Volume 3, Issue 1, March 2005, pages 161-184.

==外部リンク==
* [[Stanford Encyclopedia of Philosophy]]:  "[http://plato.stanford.edu/entries/logic-intuitionistic/ Intuitionistic Logic]"—by  Joan Moschovakis.
* [http://www.cs.le.ac.uk/people/nb118/Publications/ESSLLI'05.pdf Intuitionistic Logic] by Nick Bezhanishvili and Dick de Jongh (from the Institute for Logic, Language and Computation at the [[University of Amsterdam]])
* [https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf Semantical Analysis of Intuitionistic Logic I] by Saul A. Kripke from ''Harvard University, Cambridge, Mass., USA''
* [http://www.phil.uu.nl/~dvdalen/articles/Blackwell(Dalen).pdf Intuitionistic Logic] by ''[[Dirk van Dalen]]''
* [http://www.illc.uva.nl/j50/contribs/troelstra/troelstra.pdf The discovery of E.W. Beth's semantics for intuitionistic logic] by A.S. Troelstra and P. van Ulsen
* [ftp://ftp.cs.toronto.edu/pub/bonner/papers/hypotheticals/naclp89.ps Expressing Database Queries with Intuitionistic Logic] (''FTP one-click download'') by Anthony J. Bonner. L. Thorne McCarty. Kumar Vadaparty. Rutgers University, Department of Computer Science.
* [http://teachinglogic.liglab.fr/INT1/index.php Tableaux'method for intuitionistic logic through S4-translation] tests the intuitionistic validity of propositional formulae; provided by the Laboratoire d'Informatique de [[Grenoble]].
* [http://www.playmycode.com/play/game/torusglider/validity-tester-for-ipc Validity tester for IPC] (based on [http://www.playmycode.com/play/game/torusglider/mezhirovs-game-for-ipc Mezhirov's game for IPC]) at ''playmycode.com''
{{refend}}

{{Normdaten}}
{{DEFAULTSORT:ちよつかんしゆきろんり}}
[[Category:直観主義]]
[[Category:非古典論理]]
[[Category:形式論理体系]]
[[Category:数学に関する記事]]

[[de:Intuitionismus (Logik und Mathematik)]]