命题语言

请注意，这个条目所介绍的术语没有标准称呼。仅仅是为了便于描述建立条目取了一个名字。

命题语言(propositional language)，或命题逻辑的语言(language of propositional logic)，指研究命题逻辑的形式语言。 它包括命题变元和逻辑联结词，是构建命题公式的形式系统。 在数理逻辑中，命题语言通常记作 [math]\displaystyle{ \mathcal{L}_0 }[/math] ，表示最基础层次的逻辑语言。

命题语言为命题逻辑提供了严格的语法框架，使得命题的逻辑结构能够被精确地形式化和分析。

形式语言定义

命题语言 [math]\displaystyle{ \mathcal{L}_0 }[/math] 的字母表和规则如下：

字母表

[math]\displaystyle{ \mathcal{L}_0 }[/math] 的字母表是以下不相交集合的并集：

• 命题变元的集合： [math]\displaystyle{ P = \{p_0, p_1, \dots \} }[/math] ；
• 逻辑联结词的集合： [math]\displaystyle{ C = C_1 \cup C_2 }[/math] ：
  • 一元逻辑联结词的集合： [math]\displaystyle{ C_1 = \{\lnot\} }[/math] ；
  • 二元逻辑联结词的集合： [math]\displaystyle{ C_2 = \{\land, \lor, \rightarrow, \leftrightarrow\} }[/math] ；
• 辅助符号的集合，包括左右括号： [math]\displaystyle{ \{ (, ) \} }[/math] 。

注：不同文献对命题语言的定义可能有所差异。

• 有些定义中包括命题常量的集合，与命题变元集合并列。
• 有些定义中将命题常量归入命题变元集合的一部分。
• 有些定义中包括真值常量真和假构成的集合 [math]\displaystyle{ \{\mathrm{T},\mathrm{F}\} }[/math] 。
• 有的定义中包括真和假构成的零元逻辑联结词的集合 [math]\displaystyle{ C_0=\{\top,\bot\} }[/math] ，并认为 [math]\displaystyle{ C = C_0 \cup C_1 \cup C_2 }[/math] 。
• 有些定义可能包括一些非常用联结词。
• 有些定义可能使用不同的符号表示。

注：为避免基数过大引入不必要的问题，一般要求命题变元的集合是可数无限集。虽然形式上也允许使用任意集合，但并没有必要。理论上，选择 [math]\displaystyle{ P }[/math] 的核心是不与其他集合相交且符号充足的符号集。 在绝大多数文献和实际应用中，其元素采用诸如 [math]\displaystyle{ p, q, r, \dots }[/math] 或带下标的 [math]\displaystyle{ p_0, p_1, p_2, \dots }[/math] 等形式。

规则

命题语言 [math]\displaystyle{ \mathcal{L}_0 }[/math] 的公式集 [math]\displaystyle{ \mathrm{Form}(\mathcal{L}_0) }[/math] ，是通过以下规则递归定义的最小集合：

• [math]\displaystyle{ p }[/math] ，其中 [math]\displaystyle{ p\in P }[/math] 。是递归终止条件，称为 [math]\displaystyle{ \mathcal{L}_0 }[/math]-原子公式；
• [math]\displaystyle{ \lnot\phi }[/math] ，其中 [math]\displaystyle{ \phi \in \mathrm{Form}(\mathcal{L}_0) }[/math] ；
• [math]\displaystyle{ (\phi\odot\psi) }[/math]，其中 [math]\displaystyle{ \phi,\psi \in \mathrm{Form}(\mathcal{L}_0), \odot \in C_2 }[/math] 。

括号省略约定

为简化书写，采用以下括号省略规则：

• 最外层的括号可省略；
• 结合性（优先级）从高到低顺序为 [math]\displaystyle{ \lnot, \land, \lor, \rightarrow, \leftrightarrow }[/math] ，可按照这一顺序省略括号。（[math]\displaystyle{ \land,\lor }[/math] 之间推荐不省略）
• 一元运算符 [math]\displaystyle{ \lnot }[/math] 连续出现时，不会出现歧义，因此可以省略之间的括号。
• 相同符号的二元联结词按照 [math]\displaystyle{ \land,\lor }[/math] 为左结合， [math]\displaystyle{ \rightarrow }[/math] 为右结合的形式省略括号。 [math]\displaystyle{ \leftrightarrow }[/math] 不规定结合性，不允许省略括号。

注：有些定义中不规定 [math]\displaystyle{ \rightarrow }[/math] 为右结合，必须使用括号明确结合性。且为了可读性， [math]\displaystyle{ \rightarrow }[/math] 的括号也往往不省略。

BNF 定义

命题语言是一种上下文无关语言，可以通过 BNF 定义。

<formula> ::= <atomic>
            | "¬" <formula>
            | "(" <formula> "∧" <formula> ")"
            | "(" <formula> "∨" <formula> ")"
            | "(" <formula> "→" <formula> ")"
            | "(" <formula> "↔" <formula> ")"

<atomic> ::= "p" | "p₀" | "p₁" | "p₂" | ...

其中 <atomic> 是 [math]\displaystyle{ \mathcal{L}_0 }[/math]-原子公式，表示任意命题变元，在实际应用中通常用具体的符号代替。

相关术语

• 主联结词：递归定义中，若一个公式不是原子公式，则形式上最后使用的联结词称为这一公式的主联结词。即 [math]\displaystyle{ \lnot\varphi }[/math] 中的 [math]\displaystyle{ \lnot }[/math] 以及 [math]\displaystyle{ \varphi\odot\psi }[/math] 中的 [math]\displaystyle{ \odot\in C_2 }[/math] 。
• 直接子公式(direct subformula)：递归定义中，若一个公式不是原子公式，则直接递归的公式称为这一公式的直接子公式。即 [math]\displaystyle{ \lnot\varphi }[/math] 中的 [math]\displaystyle{ \varphi }[/math] 以及 [math]\displaystyle{ \varphi\odot\psi }[/math] 中的 [math]\displaystyle{ \varphi }[/math] 和 [math]\displaystyle{ \psi }[/math] 。
• 子公式(subformula)：对一个公式，进行递归定义。若其是原子公式，只有其本身是其子公式；若其是非原子公式，其本身及其直接子公式的任意子公式，均是其子公式。
• 真子公式(proper subformula)：对一个公式，不是其自身的子公式。

性质

• 递归可枚举性：命题语言的公式集是递归可枚举的。
• 唯一可读性：每个合式公式都有唯一的语法分析树。

语法与语义

以上是命题语言的语法，仅在符号串角度定义了符合语法约定的命题语言符号串，没有涉及其中符号的语义。这些符号串的语义需要通过指派、解释、满足等条目定义，通过真值表工具，最终用于重言蕴涵、等值/重言等价等场景。见对应条目。

变体

• 逻辑联结词部分仅使用某个函数完备集。
• 引入命题常量或真值常量。
• 模态命题语言：包含模态算子。

命题逻辑/零阶逻辑
基本概念	命题	命题、命题变元、命题常量
	真值	真 [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]
	范式	析取范式、合取范式（主析取范式、主合取范式）