永真式（Tautology）是逻辑学中的一个重要概念，又称为重言式。它指的是 在任何解释或模型下，其真值都为真的命题公式。换句话说，无论对命题公式中的变量进行何种指派，该公式的真值始终为真（True）。永真式包括由逻辑联结词∨、∧、→和¬等构成的复合命题，以及这些联结词的重言式组合。
例如，命题公式 （P ∧ Q） → （P ∨ Q） 是一个永真式，因为无论P和Q的真值如何，该公式的真值始终为真。可以通过真值表或逻辑推理来验证这一点。
永真式在逻辑学和数学中有着广泛的应用，例如在证明理论、程序验证、形式语言和自动推理等领域。