计算机科学家逻辑/命题逻辑/语法

语法

为了定义语法，我们必须假设一组原子公式，作为归纳定义的起点。借助三个连接词和括号作为标点符号，我们归纳定义了更复杂的公式。

定义 1（命题逻辑的语法）

假设一个

• 可数的原子公式集 $P_{i}$，其中 $i=1,2,3,\cdots$，
• 连接词 $\land ,\lor$ 和 $\lnot$，
• 标点符号 $($ 和 $)$。

命题公式集由以下归纳定义

• 原子公式是公式。
• 如果 $F$ 和 $G$ 是公式，则 $(F\land G)$ 和 $(F\lor G)$ 是公式。
• 如果 $F$ 是一个公式，则 $\lnot F$ 是一个公式

不同类型的公式被称为合取、析取和否定。注意，这仅仅是对措辞的一种约定，到目前为止，我们没有对这些连接词给出任何语义，以证明这些名称是合理的。

这个公式集的定义也以一种非常自然的方式引入了一个偏序，如果我们考虑子公式的概念。

定义 2（子公式）

公式的子公式是一个子串，它本身也是一个公式。

注意，关系“是子公式”确实是一个偏序。

公式集与子公式关系是一个良基关系。

为了简化符号，我们引入以下缩写

$A,B,C$ 代替 $P_{1},P_{2},P_{3}$

$(F_{1}\to F_{2})$ 代替 $(\lnot F_{1}\lor F_{2})$

$(F_{1}\leftrightarrow F_{2})$ 而不是 $((F_{1}\land F_{2})\lor (\lnot F_{1}\land \lnot F_{2}))$

$\bigvee _{i=1}^{n}~F_{i}$ 而不是 $(\cdots ((F_{1}\lor F_{2})\lor F_{3})\lor \cdots \lor F_{n})$

$\bigwedge _{i=1}^{n}~F_{i}$ 而不是 $(\cdots ((F_{1}\land F_{2})\land F_{3})\land \cdots \land F_{n})$

这些符号（除了第一个）只是简单的缩写；当这些箭头符号或索引连接词出现在公式中时，相应的子公式可以根据此定义进行替换。

回到我们之前的例子，您可以看到

$\lnot (ab(or1))\to high(or1,o)\leftrightarrow (high(or1,i1)\lor high(or1,i2))$

可以根据上述定义通过引入括号写成公式

$(\lnot (ab(or1))\to (high(or1,o)\leftrightarrow (high(or1,i1)\lor high(or1,i2))))$

引入括号是为了避免任何歧义。为了提高可读性，只要有可能，我们将省略它们。如果我们另外应用上述缩写规则，我们将得到以下公式
$(\lnot \lnot (ab(or1))\lor$

$(high(or1,o)\land ((high(or1,i1)\lor high(or1,i2))\lor$

$(\lnot high(or1,o)\lor \lnot (high(or1,i1)\lor high(or1,i2))))))$