恒真式
恒真式（こうしんしき、トートロジー、英: tautology、ギリシャ語のταυτο「同じ」に由来）は、論理学の用語で「aであるならばaである（a → a）」「aである、または、aでない（a∨￢a）」のように、そこに含まれる命題変数の真理値、あるいは解釈に関わらず常に真となる論理式のことである。
恒真式の否定は、変数の値にかかわらず常に偽となる式、すなわち矛盾である。
命題論理
命題論理において、命題を記号化したものが論理式であるが、論理式を構成している、最も単純な文に相当する要素式の真偽値の取り方に関係なく常に真（恒真）となる論理式が存在し、それらはトートロジーもしくは恒真式と呼ばれる[1]。真にも偽にもなりうる論理式を整合式（英: consistent well-formed formula）、恒に偽になる論理式を恒偽式もしくは矛盾式（英: contradictory well-formed formula）という。
述語論理
述語論理においては、トートロジーを考える事はないが、同様な概念を考える事ができる。論理式が、全ての解釈にたいして真になるとき、この論理式は恒真 (validity) で、妥当式 (valid wff) になる。少なくとも一つの解釈で論理式が真になるとき、この論理式は充足可能 (en:Satisfiability) で、充足可能式 (satisfiable wff) になる。全ての解釈で論理式が偽になるとき、この論理式は充足不可能で、矛盾式 (contradictory wff) になる[2][3]。
定義と例
ここでは古典命題論理における恒真式の定義を述べる。
 | この項目は、数理論理学に関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています。 |
