恒真式
恒真式（こうしんしき、トートロジー、英: tautology、ギリシャ語のταυτο「同じ」に由来）とは論理学の用語で、「aならば aである（a → a）」「aである、または、aでない（a ∨ ￢a）」のように、そこに含まれる命題変数の真理値、あるいは解釈に関わらず常に真となる論理式である。
定義と例
ここでは古典命題論理における恒真式の定義を述べる。[math] \mathrm{Val}[/math] を命題変数の全体とする。[math] f:\mathrm{Val}\to\{\top,\bot\} [/math] なる写像、すなわち命題変数への真理値割り当てを考える。[math]\top[/math]は恒真、[math]\bot[/math]は矛盾。次のようにして [math]f[/math] の始域を論理式の全体 [math]\mathrm{Fml}[/math] に拡張する（右辺の [math]\wedge\vee\neg\to[/math] は論理記号ではなく [math]\{\top,\bot\}[/math] 上の 演算である）：
- [math] f(\alpha \wedge \beta) := f(\alpha) \wedge f(\beta) [/math]
- [math] f(\alpha \vee \beta) := f(\alpha) \vee f(\beta) [/math]
- [math] f(\neg \alpha) := \neg f(\alpha) [/math]
- [math] f(\alpha \to \beta) := f(\alpha) \to f(\beta) [/math]
このようにして得られる写像 [math]f:\mathrm{Fml}\to \{\top,\bot\}[/math] を付値という。任意の付値 [math]f[/math] に対して [math]f(\alpha)=\top[/math] となるとき、[math]\alpha[/math] を恒真式という。
古典論理の上で、次の論理式は恒真式である。
- [math] \neg(\alpha\wedge\neg\alpha) [/math]
- [math] \alpha\vee\neg\alpha[/math]
- [math] (\alpha\to \beta)\Leftrightarrow(\neg \beta\to \neg \alpha)[/math]
- [math] \neg\neg\alpha\Leftrightarrow\alpha [/math]
- [math] \neg(\alpha\wedge \beta)\Leftrightarrow(\neg \alpha\vee\neg \beta)[/math]
- [math] ((\alpha\to \beta)\wedge(\beta\to \gamma))\to(\alpha\to \gamma)[/math]
恒真式である確認
ある式が恒真式であるかどうかを確認することは命題論理の基本である。命題変数がn個存在する場合2n通りのケースを調べればよい。 例えば [math]\alpha \to (\beta \to \alpha)[/math] であれば4通りのケースを調べれば良い。
| [math]\alpha[/math] | [math]\beta[/math] | [math]\beta\to\alpha[/math] | [math]\alpha \to (\beta \to \alpha)[/math] |
| T | T | T | T |
| T | F | T | T |
| F | T | F | T |
| F | F | T | T |
次のようにして、代数的な式変形によっても確認できる。
[math] \alpha\to(\beta\to\alpha) = \neg\alpha\vee(\neg\beta\vee\alpha) = (\alpha\vee\neg\alpha)\vee\neg\beta = \top \vee \neg\beta = \top [/math]