直観主義論理
直観主義論理(ちょっかんしゅぎろんり、英: intuitionistic logic)または直観論理(ちょっかんろんり)、あるいは構成的論理(こうせいてきろんり、英: constructive logic)とは、ある種の論理体系であり、伝統的な真理値の概念が構成的証明の概念に置き換わっている点で古典論理とは異なる。例えば古典論理では、全ての論理式に真か偽の真理値 ( { ⊤ , ⊥ } {\displaystyle \{\top ,\bot \}} ) が割り当てられる。このときその真理値に対する直接的なエビデンスを持つか否かは問題にしない。これはどのような曖昧な命題においても「真か偽かが決定可能である」ということを意味する。対照的に直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。
同値
同値を表す結合子 ↔ {\displaystyle \leftrightarrow } は φ ↔ χ {\displaystyle \phi \leftrightarrow \chi } standing for ( φ → χ ) ∧ ( χ → φ ) {\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 ))} に結合できる。
例えば矛盾律 ¬ ( A ∧ ¬ A ) {\displaystyle \neg (A\wedge \neg A)} は妥当である。なぜなら開集合 X {\displaystyle X} を A {\displaystyle A} の付値としてどのように選んでも ¬ ( A ∧ ¬ A ) {\displaystyle \neg (A\wedge \neg A)} の値は次のように直線全体となるからである:
v a l ( ¬ ( A ∧ ¬ A ) ) = i n t ( ( X ∧ i n t ( X c ) ) c ) {\displaystyle \mathrm {val} (\neg (A\wedge \neg A))=\mathrm {int} ((X\wedge \mathrm {int} (X^{c}))^{c})}
位相空間論によれば i n t ( X c ) {\displaystyle \mathrm {int} (X^{c})} は X c {\displaystyle X^{c}} の部分集合であり、 X {\displaystyle X} との共通部分は空であるから、
i n t ( ∅ c ) = i n t ( R ) = R {\displaystyle \mathrm {int} (\varnothing ^{c})=\mathrm {int} (\mathbb {R} )=\mathbb {R} }