命题语言
请注意，这个条目所介绍的术语没有标准称呼。仅仅是为了便于描述建立条目取了一个名字。
命题语言(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{ \land,\lor }[/math] 为左结合， [math]\displaystyle{ \rightarrow }[/math] 为右结合的形式省略括号。 [math]\displaystyle{ \leftrightarrow }[/math] 不规定结合性，不允许省略括号。
注：有些定义中不规定 [math]\displaystyle{ \rightarrow }[/math] 为右结合，必须使用括号明确结合性。且为了可读性， [math]\displaystyle{ \rightarrow }[/math] 的括号也往往不省略。
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)：对一个公式，不是其自身的子公式。
性质
- 递归可枚举性：命题语言的公式集是递归可枚举的。
- 唯一可读性：每个合式公式都有唯一的语法分析树。
语法与语义
以上是命题语言的语法，仅在符号串角度定义了符合语法约定的命题语言符号串，没有涉及其中符号的语义。这些符号串的语义需要通过指派、解释、满足等条目定义，通过真值表工具，最终用于重言蕴涵、等值/重言等价等场景。见对应条目。
变体
- 逻辑联结词部分仅使用某个函数完备集。
- 引入命题常量或真值常量。
- 模态命题语言：包含模态算子。