永真式

永真式在每个命题赋值下都为真，因此其有效性完全来自逻辑形式，而非变量代表的具体事实；把任意具体命题代入也不会变假。它与可满足公式公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。不同：可满足只需要一个成功赋值，永真则要求没有反例。公式 $\phi$ 永真等价于 $\mathrm{\neg }\phi$ 不可满足。

$p\vee \mathrm{\neg }p$、$(p\wedge (p\to q))\to q$ 都是永真式；$p\to q$ 是偶然式。$p\vee q$ 在某个赋值为真，因此可满足，但不是永真，说明可满足只需一个模型而永真要求全部模型。自然语言中“显然为真”的经验命题不是逻辑永真式，除非其真由形式结构保证。

分配律可写成永真式

它在全部八种赋值下都为真，因此可作为任意具体命题的合法替换规则。相比之下，$P\vee Q$ 只需在某些赋值下为真，属于可满足公式而非永真式。经验上总是真的陈述也不自动成为逻辑永真式；永真性只由公式结构和联结词语义决定。

永真式表达有效推理模式、布尔恒等式和组合电路规范。真值表公理库真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。可决定有限命题公式是否永真，命题可靠性与完备性公理库命题逻辑可靠性与完备性定理Soundness and completeness of propositional logic命题演算中的可证性与对所有赋值成立的语义蕴涵恰好一致。保证永真式恰为可证明公式；检查 $\phi \leftrightarrow \psi$ 是否永真即可判定逻辑等价。电路等价检查、程序条件验证与逻辑化简，也都把目标归结为永真性或其否定的不可满足性。