查看“︁命题语言”︁的源代码

[[分类:命题逻辑]]
[[分类:形式语言实例]]{{DEFAULTSORT:ming4ti2yu3yan2}}
{{#seo:
|keywords=命题语言, 命题逻辑的形式语言, 形式语言, 命题逻辑
|description=本文介绍命题语言的定义、性质与语法规则，包括命题语言作为命题逻辑的形式语言的概念，其字母表和公式构造规则，及其在逻辑学中的基础地位。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2024-04-05
}}
{{非标准称呼}}
命题语言('''propositional language''')，或命题逻辑的语言(language of propositional logic)，指研究[[:分类:命题逻辑|命题逻辑]]的[[形式语言]]。
它包括[[命题|命题变元]]和[[逻辑联结词]]，是构建[[命题公式]]的形式系统。
在数理逻辑中，命题语言通常记作 <math>\mathcal{L}_0</math> ，表示最基础层次的逻辑语言。

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

== 形式语言定义 ==

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

=== 字母表 ===

<math>\mathcal{L}_0</math> 的字母表是以下不相交集合的并集：
* [[命题|命题变元]]的集合： <math>P = \{p_0, p_1, \dots \}</math> ；
* [[逻辑联结词]]的集合： <math>C = C_1 \cup C_2</math> ：
** 一元逻辑联结词的集合： <math>C_1 = \{\lnot\}</math> ；
** 二元逻辑联结词的集合： <math>C_2 = \{\land, \lor, \rightarrow, \leftrightarrow\}</math> ；
* 辅助符号的集合，包括左右括号： <math>\{ (, ) \}</math> 。

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

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

=== 规则 ===

命题语言 <math>\mathcal{L}_0</math> 的公式集 <math>\mathrm{Form}(\mathcal{L}_0)</math> ，是通过以下规则递归定义的最小集合：
* <math>p</math> ，其中 <math>p\in P</math> 。是递归终止条件，称为 <math>\mathcal{L}_0</math>-原子公式；
* <math>\lnot\phi</math> ，其中 <math>\phi \in \mathrm{Form}(\mathcal{L}_0)</math> ；
* <math>(\phi\odot\psi)</math>，其中 <math>\phi,\psi \in \mathrm{Form}(\mathcal{L}_0), \odot \in C_2</math> 。

==== 括号省略约定 ====

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

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

== BNF 定义 ==

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

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

<atomic> ::= "p" | "p₀" | "p₁" | "p₂" | ...
</syntaxhighlight>
其中 <syntaxhighlight inline lang="bnf"><atomic></syntaxhighlight> 是 <math>\mathcal{L}_0</math>-原子公式，表示任意命题变元，在实际应用中通常用具体的符号代替。

== 相关术语 ==

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

== 性质 ==

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

== 语法与语义 ==

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

== 变体 ==

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


{{命题逻辑}}