哲学/逻辑导论/命题逻辑的更形式化方法

哲学导论 > 逻辑 > 命题逻辑的更形式化方法

我们的真值表分析揭示了关于逻辑联结词的一些有趣的事情。特别是，它们在某些方面像普通数字上的 + 和 . 一样。我们进入抽象世界的旅程已经带来了回报，所以现在我们将沿着抽象之路走得更远。

我们要做的是将命题演算定义为一种形式语言，就像一种计算机编程语言一样。我们将使用英语，以及一两个希腊字母，来定义和谈论命题演算的形式语言。因此，英语是元语言，而命题演算是目标语言。

合式公式

我们已经介绍了逻辑公式。一些逻辑符号串是有意义的，而另一些则没有；' p ∨ ' 是无意义的，因为它需要联结词后面有东西。那些有意义的被称为合式公式，简称wffs。我们可以引入一些规则来区分wffs和胡言乱语。

任何句子字母都是一个wff。

到目前为止，我们一直在使用 p、q 和 r 作为句子字母。实际上，它们有无限多个。我们可以写 p₁、p₂、p₃，等等，但我们将继续使用 p、q 和 r。

如果 φ 是一个wff，那么 ¬ φ 是一个wff。

如果 φ 和 ψ 是wffs，那么 (φ ∧ ψ)、(φ ∨ ψ)、(φ → ψ) 和 (φ ↔ ψ) 是wffs。

在我们的形式化处理中，我们总是写括号。

封闭子句：其他任何东西都不是wff。

这排除了无意义的字符串。请注意，虽然这些规则是为了区分可能是有意义的和没有意义的，但这些规则纯粹是句法上的。

需要注意的另一件事是，这些规则具有逆规则，这对决定已经写下的东西是否是一个wff很有用。我们只需应用这些逆规则，直到我们只剩下空值或卡住。因此，我们有一个生成 wffs 的有效程序，以及一个决定字符串是否为 wffs 的有效程序。

现在我们为命题演算引入一些推理规则。在某些方面，这些规则是不必要的，因为我们可以将真值表作为基本，并使用真值表来证明以下规则。然而，当我们谈到谓词演算时，我们将没有真值表来帮助我们，并且必须完全依靠推理规则。

推理规则

现在我们为命题演算引入一些推理规则。在某些方面，这些规则是不必要的，因为我们可以将真值表作为基本，并使用真值表来证明以下规则。然而，当我们谈到谓词演算时，我们将没有真值表来帮助我们，并且必须完全依靠推理规则。

双重否定消去：从 wff ¬ ¬ φ，我们可以推断出 φ。
合取引入：从任何 wff φ 和任何 wff ψ，我们可以推断出 ( φ ∧ ψ )。
合取消去：从任何 wff ( φ ∧ ψ )，我们可以推断出 φ 和 ψ
析取引入：从任何 wff φ，我们可以推断出 (φ ∨ ψ) 和 (ψ ∨ φ)，其中 ψ 是任何 wff。
析取消去：从形式为 ( φ ∨ ψ )、( φ → χ ) 和 ( ψ → χ ) 的 wffs，我们可以推断出 χ。
双条件引入：从形式为 ( φ → ψ ) 和 ( ψ → φ ) 的 wffs，我们可以推断出 ( φ ↔ ψ )。
双条件消去：从 wff ( φ ↔ ψ )，我们可以推断出 ( φ → ψ ) 和 ( ψ → φ )。
肯定前件：从形式为 φ 和 ( φ → ψ ) 的 wffs，我们可以推断出 ψ。
条件证明：如果可以在假设假设 φ 的情况下推导出 ψ，我们可以推断出 ( φ → ψ )。
归谬法：如果可以在假设假设 φ 的情况下推导出 ψ 和 ¬ ψ，我们可以推断出 ¬ φ。

算子的互定义性

可以用其他算子来定义一些逻辑算子。例如，公式 (φ → ψ) 的真值表等于 ¬(φ ∧ ¬ψ) 的真值表，因此我们可能想将 (φ → ψ) 仅仅视为 ¬(φ ∧ ¬ψ) 的简写符号。
这里有趣的是，命题演算中的所有逻辑算子都可以用 ¬ 和 ∧ 来表示。这一事实允许我们以非常简单的方式表达合式公式的规则。

如果 φ 是一个wff，那么 ¬ φ 是一个wff。
如果 φ 和 ψ 是 wffs，那么 (φ ∧ ψ) 是一个 wff。
其他任何东西都不是合式公式。

然后我们可以用这两个算子来定义其他算子。

(φ → ψ) 根据定义为 ¬(φ ∧ ¬ψ)。
(φ ↔ ψ) 根据定义为 (φ → ψ) ∧ (ψ → φ)。
(φ ∨ ψ) 根据定义为 ¬(¬φ ∧ ¬ψ)。

如果我们考虑这些定义（三个额外的规则），似乎我们并没有通过减少原始算子的数量而获得多少益处。然而，当将命题演算系统作为一个整体来考虑时（例如，当我们研究系统的性质时），用极少数规则来描述系统是有用的。在这种情况下，我们不关心特定的公式，因此可以删除定义其他算子的额外规则。
也可以证明所有逻辑算子都可以用 ¬ 和 ∨ 来定义。