論理学や数学において、真理値(論理値とも呼ばれる)は、命題と真理の関係を示す値であり、古典論理では真理には2つの可能な値(真または偽)しかありません。[ 1 ] [ 2 ]真理値は、コンピューティングだけでなく、さまざまな種類の論理でも使用されます。
プログラミング言語によっては、ブール型を期待するコンテキストで任意の式を評価できます。通常(プログラミング言語によって異なりますが)、数値のゼロ、空文字列、空のリスト、nullなどの式は false として扱われ、内容のある文字列(「abc」など)、その他の数値、オブジェクトは true として評価されます。これらの式のクラスは、偽値と真値と呼ばれることがあります。たとえば、Lispでは、空のリストである nilは false として扱われ、その他の値はすべて true として扱われます。C では、数値の 0 または 0.0 は false であり、その他の値はすべて true として扱われます。
JavaScriptでは、空文字列 ( "")、null、undefined、NaN、+0および[ 3 ]−0は、厳密に型チェックされたブール値と強制されたブール値を区別するために、偽値(その補数は真値)と呼ばれることがあります ( JavaScript 構文#型変換も参照)。[ 4 ] Python とは異なり、空のコンテナ (配列、マップ、セット) は真値とみなされます。PHP などの言語もこのアプローチを使用しています。false
古典論理では、その意図された意味論において、真理値は真(1またはverum⊤ で表される)と偽( 0またはfalsum⊥で表される)の2つです。つまり、古典論理は2値論理です。この2つの値の集合はブール領域とも呼ばれます。論理結合子の対応する意味論は真理関数であり、その値は真理表の形で表現されます。論理双条件は等号二項関係になり、否定は真と偽を入れ替える全単射になります。連言と選言は否定に関して双対であり、否定はド・モルガンの法則で表現されます。
命題変数はブール領域の変数となる。命題変数に値を割り当てることを評価と呼ぶ。
古典論理では真理値がブール代数を形成するのに対し、直観主義論理、そしてより一般的には構成的数学では、真理値はハイティング代数を形成する。このような真理値は、局所性、時間性、計算内容など、妥当性の様々な側面を表現することができる。
例えば、位相空間の開集合を 直観主義的な真理値として用いる場合、論理式の真理値は、論理式が成り立つかどうかではなく、その論理式が成り立つ場所を表すことになる。
実現可能性の真理値はプログラムの集合であり、これは公式の妥当性を示す計算上の証拠として理解できます。例えば、「すべての数にはそれより大きい素数が存在する」という命題の真理値は、数nを入力として受け取り、 nより大きい素数を出力するすべてのプログラムの集合です。
圏論において、真理値は部分対象分類子の要素として現れる。特に、基本トポスにおいては、高階論理のすべての論理式に部分対象分類子における真理値を割り当てることができる。
ハイティング代数には多くの要素が含まれる可能性があるが、これは真でも偽でもない真理値が存在することを意味するものではない。なぜなら、直観主義論理では¬( p ≠ ⊤ ∧ p ≠ ¬⊥) (「 pが真でも偽でもないということはない」) が証明されるからである。[ 5 ]
直観主義型理論において、カリー=ハワード対応は命題と型の等価性を示しており、それによれば妥当性は型への居住と等価である。
直観主義的真理値に関するその他の概念については、Brouwer–Heyting–Kolmogorov 解釈および直観主義論理 § 意味論を参照してください。
多値論理(ファジー論理や関連性論理など)は、2つ以上の真理値を許容し、内部構造を持つ場合がある。例えば、単位区間[ 0, 1 ]では、そのような構造は全順序であり、これはさまざまな真理値の存在として表現できる。
すべての論理体系が、論理結合子を真理関数として解釈できるという意味で真理値評価的であるとは限りません。例えば、直観主義論理は、その意味論であるブロウワー・ヘイティング・コルモゴロフ解釈が、論理式の必然的な真理値ではなく、証明可能性条件によって規定されているため、完全な真理値セットを持ちません。
しかし、真偽値を持たない論理体系でも、代数的意味論のように論理式に値を関連付けることができる。直観主義論理の代数的意味論は、古典的な命題論理のブール代数意味論と比較して、ハイティング代数の観点から説明される。