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

[[分类:命题逻辑]][[分类:形式语言实例]]
{{非标准称呼}}
命题语言('''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>C_0</math> 并入 <math>C</math>。

=== 规则 ===

记 <math>\mathcal{L}_0</math> 的公式集为 <math>F</math> ，其中仅包含以下几类元素：
* <math>p</math>，<math>p\in P</math>；
* <math>\lnot\phi</math>，<math>\phi \in F</math>；
* <math>(\phi\odot\psi)</math>，<math>\phi,\psi \in F, \odot \in C_2</math>。
且：
* 最外层的括号可省略；
* 可以按照 <math>\lnot, \land, \lor, \rightarrow, \leftrightarrow</math> 的结合顺序省略括号。

注：有的定义也包括真和假。

==== BNF 定义 ====

<syntaxhighlight lang="bnf">
<formula> ::= <atom> | "¬" <formula> | "(" <formula> <op> <formula> ")"
<op> ::= "∧" | "∨" | "→" | "↔"
</syntaxhighlight>
其中 <syntaxhighlight inline lang="bnf"><atom></syntaxhighlight> 是终结符，替换为任意命题变元 <math>p\in P</math>。
且也按上述方式省略括号。