命题公式

命题公式
术语名称	命题公式
英语名称	propositional formula
别名	命题合式公式, propositional well-formed formula, 合式公式, well-formed formula, WFF, 公式, formula

命题公式(propositional formula)是命题语言中的合式公式， 由命题变元、逻辑联结词和括号按照特定语法规则构成的符号串。

命题公式是命题逻辑研究的基本对象，通过指派可以确定其真值。

定义

命题语言公式集 [math]\displaystyle{ \mathrm{Form}(\mathcal{L}_0) }[/math] 中的元素称为命题合式公式(propositional well-formed formula)，简称合式公式(well-formed formula，缩写为WFF)或命题公式(propositional formula)，有时也简称公式(formula)，是通过以下规则递归定义的符号串：

1. 原子公式：任意命题变元（和命题常量）是命题公式；
2. 复合公式：
   • 若 [math]\displaystyle{ \varphi }[/math] 是命题公式，则 [math]\displaystyle{ \lnot\varphi }[/math] 是命题公式；
   • 若 [math]\displaystyle{ \varphi }[/math] 、 [math]\displaystyle{ \psi }[/math] 是命题公式，则 [math]\displaystyle{ (\varphi \land \psi) }[/math] 、 [math]\displaystyle{ (\varphi \lor \psi) }[/math] 、 [math]\displaystyle{ (\varphi \rightarrow \psi) }[/math] 、 [math]\displaystyle{ (\varphi \leftrightarrow \psi) }[/math] 是命题公式。
3. 只有有限次应用规则 1 和 2 所得到的符号串是命题公式。

为简化书写，通常省略最外层括号，并规定逻辑联结词的优先级从高到低为 [math]\displaystyle{ \lnot, \land, \lor, \rightarrow, \leftrightarrow }[/math] ，其中 [math]\displaystyle{ \land,\lor }[/math] 左结合。

注：

• 有些定义不提及命题常量。
• 有些定义中命题常量被归入命题变元。
• 有些定义包含真值常量真和假。
• 有些定义将真值常量视为零元联结词。

注意：命题公式中由于含有命题变元，通常不能确认其真值，因此命题公式不是命题。只有命题公式的指派才是命题。

命题公式的分类

主条目：命题公式分类

根据在所有可能指派下的行为，命题公式可分为重言式、矛盾式、偶然式。

命题逻辑/零阶逻辑
基本概念	命题	命题、命题变元、命题常量
	真值	真 [math]\displaystyle{ \mathrm{T} }[/math]/[math]\displaystyle{ 1 }[/math]/[math]\displaystyle{ \top }[/math] 、假 [math]\displaystyle{ \mathrm{F} }[/math]/[math]\displaystyle{ 0 }[/math]/[math]\displaystyle{ \bot }[/math]
命题结构	命题结构	原子命题、复合命题
	逻辑联结词	否定（非） [math]\displaystyle{ \lnot }[/math] 、合取（且/与） [math]\displaystyle{ \land }[/math] 、析取（或） [math]\displaystyle{ \lor }[/math]
		蕴涵（推出） [math]\displaystyle{ \rightarrow }[/math] 、等价（当且仅当） [math]\displaystyle{ \leftrightarrow }[/math]
命题公式	形式定义	命题语言 [math]\displaystyle{ \mathcal{L}_0 }[/math] 、命题公式
	逻辑语义	指派、 Tarski 真理定义、解释、真值表、满足
	语义分类	重言式/永真式、偶然式/仅可满足式/可真可假式、矛盾式/永假式/不可满足式
	语义关系	重言等价/等值/等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、重言蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	析取范式、合取范式（主析取范式、主合取范式）