公式well-formed formula

项与公式 / 语句（Formula, Sentence）

def.formula · 定义 · 逻辑 · 公式 · 自由变元 · 语句

又称合式公式·well-formed formula·wff·命题

陈述

（在给定的一阶语言 L\mathcal{L} 里）公式就是按语法规则 3 生成的表达式，即

φ::=R(t1,…,tn)  ∣  ¬φ  ∣  (φ∧ψ)  ∣  (φ∨ψ)  ∣  (φ→ψ)  ∣  ∀viφ  ∣  ∃viφ\varphi ::= R(t_{1}, \ldots, t_{n}) \;\mid\; \neg \varphi \;\mid\; (\varphi \wedge \psi) \;\mid\; (\varphi \vee \psi) \;\mid\; (\varphi \to \psi) \;\mid\; \forall v_{i} \varphi \;\mid\; \exists v_{i} \varphi

其中 RR 遍历 L\mathcal{L} 的关系符号，tjt_{j} 遍历项（严格说这是一条归纳定义：公式全体是「含全部原子公式、并对上述运算封闭」的最小集合）。

变元在 ∀vi\forall v_{i}、∃vi\exists v_{i} 的辖域内出现叫约束出现，否则叫自由出现；没有自由变元的公式叫语句（闭公式）。

公式的复杂度（连接词与量词的个数）可以做归纳 —— 这是「对公式作归纳」的依据。

说明

⭐ 「φ(x,p)\varphi (x, p)」这种写法在说什么：它表示 φ\varphi 是一个公式，且其中的自由变元都在 {x,p}\{ x, p \} 里（未必都用上）。分离公理模式里写的「对每个公式 φ\varphi（BB 不出现）」说的就是这种约定 —— 公式是元数学概念，不是 ZFC 的对象，所以「不出现」才是一句关于符号串的话。

⭐ 归纳定义 = 最小集合：这句话背后用的是 N\mathbb{N} 上的归纳（见「归纳原理与递推定义」）。同时它也是「公式的复杂度可以做归纳」的原因 —— 两者是同一件事的两面。

⚠ 只留一部分原始符号：∃\exists 是 ¬∀¬\neg \forall \neg 的缩写，∨\vee、→\to 也可由 ¬,∧\neg, \wedge 定义。原始符号越少，语法规则和后续的证明就越短，代价是写公式时多几层括号。

⚠ 「变元换成项」的操作是代入，它有个必须小心的坑（变元捕获），单独一个节点。

它指向谁（出边）

定义引用 4

谁指向它（入边）

定义引用 1

参考

同一星团的其他概念 4 个

继续

在星图里打开「公式」　·　 全部 709 个概念　·　 Markdown 原文　·　 English entry　·　读图指南与记号表