公式 (数理逻辑)

公式
技术术语
上级分类	word、​数学公式
话题方面	邏輯學
研究学科	邏輯學、​逻辑代数

在数理逻辑中，公式（英語：well-formed formula，缩写WFF或wff，常读作「woof」或「wiff」）是根据形式语言的语法规则构造的有限符号序列。公式是语法对象，通过解释被赋予语义含义。对公式的两个关键应用是在命题逻辑和谓词逻辑中：在命题演算中，公式由命题变量和逻辑联结词构成；在一阶谓词演算中，公式还包括量词、谓词符号和函数符号。

公式的精确定义依赖于所涉及的形式逻辑，但对一阶逻辑而言，有以下经典定义：公式是相对于特定语言定义的，即一组常量符号、函数符号和关系符号，其中的每个函数和关系符号都带有一个元数（arity）来指示它所接受的参数的数目。

命题演算公式

在命题演算中，公式通过归纳定义构造。首先选定一组命题变量（如p、q、r等）。公式的集合是满足以下条件的最小表达式集合：

1. 每个命题变量本身是一个公式。
2. 若$\varphi$是公式，则$\neg \varphi$是公式。
3. 若$\varphi$和$\psi$是公式，则$(\varphi \land \psi )$、$(\varphi \lor \psi )$、$(\varphi \to \psi )$和$(\varphi \leftrightarrow \psi )$都是公式。

该定义可用BNF表示如下（假设变量集合有限）：

<form> ::= p | q | r | ... | ¬<form> | (<form>∧<form>) | (<form>∨<form>) | (<form>→<form>) | (<form>↔<form>)

为减少括号数量，逻辑联结词通常规定优先级：¬（最高）→ → → ∧ → ∨（最低）。在此约定下，公式$((p\to q)\land (r\to s))\lor (\neg q\land \neg s)$可简写为$p\to q\land r\to s\lor \neg q\land \neg s$。

谓词逻辑公式

在一阶逻辑中，公式的定义依赖于签名（signature），即常量符号、谓词符号和函数符号的集合。

项

项（term）表示论域中的对象，递归定义如下：

1. 任何变量都是项。
2. 任何常量符号都是项。
3. 若$f$是$n$元函数符号，$t_{1},\ldots ,t_{n}$是项，则$f(t_{1},\ldots ,t_{n})$是项。

原子公式

1. 若$t_{1}$和$t_{2}$是项，则$t_{1}=t_{2}$是原子公式。
2. 若$R$是$n$元谓词符号，$t_{1},\ldots ,t_{n}$是项，则$R(t_{1},\ldots ,t_{n})$是原子公式。

公式的递归定义

公式的集合是包含所有原子公式且满足以下条件的最小集合：

1. 若$\varphi$是公式，则$\neg \varphi$是公式。
2. 若$\varphi$和$\psi$是公式，则$(\varphi \land \psi )$和$(\varphi \lor \psi )$是公式。
3. 若$\varphi$是公式，$x$是变量，则$\exists x\,\varphi$和$\forall x\,\varphi$是公式。

不含任何量词的公式称为无量词公式（quantifier-free formula）。不以量词开头的公式称为开放公式（open formula）。

原子公式与开放公式

主条目：原子公式

原子公式是不包含逻辑联结词和量词的公式。在命题逻辑中原子公式就是命题变量；在谓词逻辑中，原子公式是谓词符号或等词作用于项的结果。开放公式是含有自由变量的公式（即至少有一个变量不受量词约束）。没有自由变量的公式称为封闭公式（closed formula）或句子（sentence）。若公式$\mathbf {A}$中有自由变量$v_{1},\ldots ,v_{n}$，则对$\mathbf {A}$全部自由变量的全称量化$\forall v_{1}\cdots \forall v_{n}\,\mathbf {A}$称为$\mathbf {A}$的全称闭包（universal closure）。

公式的性质

设$\mathbf {A}$是语言${\mathcal {Q}}$中的公式：

• 有效性：若$\mathbf {A}$在${\mathcal {Q}}$的所有解释下都为真，则$\mathbf {A}$是有效的（valid）。
• 可满足性：若$\mathbf {A}$在${\mathcal {Q}}$的某个解释下为真，则$\mathbf {A}$是可满足的（satisfiable）。
• 可判定性：若存在一种有效方法，对$\mathbf {A}$的自由变量的任何代入都能判定代入后实例的真假，则$\mathbf {A}$是可判定的（decidable）。

术语使用

在数理逻辑的早期著作中（如邱奇、希尔伯特和阿克曼），「公式」一词曾泛指任何符号串，而「合式公式」（well-formed formula）特指符合构造规则的公式。现代用法（尤其是计算机科学领域）倾向于仅保留公式的代数概念，将具体的符号表示（如联结词的选择、括号约定、波兰记法或中缀记法）视为纯粹的记法问题。

WFF的发音在英语中有多种变体，最常见的是「woof」（与「roof」押韵），此外也有「wiff」、「weff」和「whiff」等变体。这一缩写还进入了流行文化——耶鲁大学的Layman Allen开发的逻辑教学游戏「WFF 'N PROOF」的名称即是对「whiffenpoof」（耶鲁大学的传统欢呼用语）的双关借用。

参见

• 合式公式
• T-模式
• 原子公式
• 句子 (数理逻辑)
• 形式语言