命题逻辑
命题逻辑试图捕捉自然语言的某些逻辑特征。特别是,它涵盖了句子的真值函数连接。它的形式语言专门识别命题连接
- 并非_____
- _____ 和 _____
- _____ 或 _____
- _____ 或 _____ (或两者)
- 如果 _____, 则 _____
- _____ 当且仅当 _____
空白处应填入可以为真或假的语句。例如,“今天正在下雨”或“明天会下雪”。最终的句子是否为真,完全取决于填入的语句是否为真。例如,如果今天正在下雨,但明天不会下雪,那么说“今天正在下雨或者明天会下雪”是正确的。另一方面,说“今天正在下雨并且明天会下雪”是错误的,因为明天不会下雪。
“一个语句是否为真”在逻辑学行话中被称为真值。因此,“今天正在下雨或者今天没有下雨”的真值为真,而“今天正在下雨并且今天没有下雨”的真值为假。
请注意,上面列出的命题连接并不包括所有可能的真值组合。例如,没有一个连接在两个子语句都为真,两个子语句都为假,或第一个子语句为真而另一个子语句为假时为真,而在其他情况下为假。但是,您可以将上面的连接组合在一起,以构建任何数量的子语句的任何真值组合。
我们已经默认地采取了持续争论中的一个立场。上面看似简单的开头已经提出了一些问题,列举如下。
- 我们是否应该只承认真或假的句子进入我们的逻辑?多值逻辑允许更大范围的句子。
- 上面列出的连接真的是真值函数吗?我们是否应该承认非真值函数句子进入我们的逻辑?
- 逻辑应该以什么作为它的真值承担者(为真或假的事物)?今天领先的两个竞争者是句子和命题。
- 句子。它们由一系列单词和可能的标点符号组成。句子“猫在垫子上”包含六个元素:“the”、“cat”、“is”、“on”、“the”和“mat”。
- 命题。它们是句子的意思。它们是句子表达的内容,或者某人在说句子时表达的内容。命题猫在垫子上包含三个元素:一只猫、一个垫子和“在”关系。
- 在维基教科书和维基百科的别处,您将看到“命题逻辑”(或更确切地说是“命题演算”,见下文)的名称,以及对命题的处理比看到“命题逻辑”的名称和对句子的处理更为常见。我们在这里的选择代表了贡献者的观点,即哪种立场在当代逻辑学家中更流行,以及您在该主题的标准教科书中最有可能看到什么。关于流行观点是否真正正确的考虑因素在这里没有讨论。
- 一些作者会使用“语句”来代替“句子”。您可能遇到的多数(但并非全部)此类作者将语句视为句子的一个子集,即那些要么为真要么为假的句子。这种“语句”的用法并不代表争议中的第三个立场,而是将这些作者置于句子阵营。(然而,其他——特别是较老的——“语句”的用法可能将它们的作者置于第三个阵营。)
有时您会看到“演算”而不是“逻辑”,例如“命题演算”或“命题演算”,而不是“命题逻辑”或“命题逻辑”。虽然“命题”和“命题”之间的选择是实质性的和哲学性的,但“逻辑”和“演算”之间的选择仅仅是风格上的。
本页非正式地描述了我们的命题语言,我们将其命名为
。将在形式语法和形式语义学中给出更正式的描述。
中的句子
表示为句子字母,它们是单个字母,例如
等等。有些文本将它们限制为小写字母,另一些文本将它们限制为大写字母。我们将使用大写字母。
直观地,我们可以将语句字母视为英语句子,它们要么为真,要么为假。因此,
可以翻译为“地球是一颗行星”(这是真的),或者“月亮是由绿色奶酪制成的”(这是假的)。但
不能翻译为“伟大的想法疯狂地沉睡着”,因为这样的句子既不是真的也不是假的。英语和
之间的翻译效果最好是限制在永恒的真假现在时句子,以陈述语气表达。你会在下面的翻译部分看到,我们并不总是遵循该建议,其中我们展示了一些句子,其真假并非永恒的。
语句连接词是命题逻辑中表示真值函数关系的特殊符号。它们用来从较小的句子构建较大的句子。然后,可以根据较小句子的真假来计算较大的句子的真假。
- 翻译成英语为“和”。
被称为合取式,而
和
是它的合取项。
为真,当且仅当
和
都为真,否则为假。
- 一些作者使用&(和号)、•(实心圆点)或并置。在最后一种情况下,作者会写

- 而不是我们的

- 翻译成英语为“或”。
被称为析取式,而
和
是它的析取项。
为真,当且仅当
或
中至少有一个为真;否则为假。
- 有些作者可能会使用竖线:|。然而,这来自于计算机语言,而不是逻辑学家们的用法。逻辑学家通常将竖线保留用于与非(替代否定)。当用作与非时,它被称为 Sheffer 竖线。
- 翻译成英文为 'it is not the case that',但通常读作 'not'。
被称为否定。
为真,当且仅当
为假;否则为假。
- 有些作者使用~(波浪号)或−。有些作者使用上划线,例如写

- 而不是

- 翻译成英文为 'if...then',但通常读作 'arrow'。
被称为条件句。它的前件是
,它的后件是
.
为假,如果
为真,而
为假——否则为真。
- 根据定义,
等效于 
- 有些作者使用 ⊃(钩号)。
- 翻译成英文是“当且仅当”。
被称为*双条件式*。
为真,如果
和
都为真或都为假——否则为假。
- 根据定义,
等效于更冗长的
。它也等效于
,两个条件式的合取,其中第二个条件式的先行式和后件式与第一个条件式相反。
- 有些作者使用 ≡。
圆括号
和
用于分组。因此


是两个不同且独立的句子。每个否定、合取、析取、条件和双条件都只有一个括号对。
(1) 一个原子句是一个仅包含单个句子字母的句子。一个分子句是一个至少包含一个句子连接词的句子。主连接词是指控制整个句子的连接词。原子句当然没有主连接词。
(2) 条件和双条件的⊃ 和≡ 符号在历史上更为古老,也许更传统,在维基教科书 和 维基百科 上比我们箭头和双箭头更常见。它们起源于阿尔弗雷德·诺思·怀特黑德 和 伯特兰·罗素 在《数学原理》 中。我们箭头和双箭头似乎起源于 阿尔弗雷德·塔尔斯基,并且可能比怀特黑德和罗素的⊃ 和≡ 今天更流行。
(3) 有时你会看到人们将我们的箭头读作蕴含。这在维基教科书 和 维基百科 中相当常见。但是,大多数逻辑学家更喜欢将“蕴含”保留用于元语言使用。他们会说
- 如果 P 那么 Q
或者甚至
- P 箭头 Q
他们赞成
- 'P' 蕴含 'Q'
但会反对
- P 蕴含 Q
考虑以下英语句子
- 如果下雨而且琼斯出去散步,那么琼斯带了雨伞。
- 如果是星期二或者星期三,那么琼斯出去散步。
为了在
中表达这些,我们首先为一些句子字母指定适当的英语翻译。
下雨了。
琼斯出去散步。
琼斯带了雨伞。
今天是星期二。
今天是星期三。
我们现在可以将我们的例子部分翻译为


然后通过添加句子连接词和括号完成翻译


对于英语表达式,我们遵循使用单引号的逻辑传统。这使我们能够使用' 'It is raining' '作为'It is raining'的引用。
对于
中的表达式,将它们视为自引用的更方便,因此引号是隐式的。因此,我们说上述示例将
(注意缺少引号)翻译成'If it is Tuesday, then It is raining'。
在命题语言中,我们非正式地描述了我们的命题语言。在这里,我们给出它的形式语法或文法。我们将我们的语言称为
。
- 句子字母:大写字母'A' – 'Z',每个都有 (1) 上标 '0' 和 (2) 自然数下标。(自然数是正整数和零的集合。)因此,句子字母是



句子字母上的上标在我们进入谓词逻辑之前并不重要,所以我们在这里不必担心它们。句子字母上的下标是为了确保无限供应的句子字母。在下一页,我们将省略大多数上标和下标。
来自
词汇的任何字符字符串都是
的一个表达式。一些表达式在语法上是正确的。有些在
中与“Over talks David Mary the”在英语中的错误一样。在
中,还有其他表达式与“jmr.ovn asgj as;lnre”在英语中的错误一样糟糕。
我们称
的语法上正确的表达式为良构式公式。当我们进入谓词逻辑时,我们会发现只有部分良构式公式是句子。不过,目前,我们认为所有良构式公式都是句子。
的表达式被称为
的良构式公式,如果它是根据以下规则构造的。
该表达式包含单个句子字母
该表达式由其他良构式公式
和
以以下方式之一构成





一般来说,我们将使用“公式”作为“良构公式”的简写。由于在
中的所有公式都是句子,我们将交替使用“公式”和“句子”。
我们将认为
的表达式是自引用的,因此将

看作包括隐含的引号。然而,像

需要特别考虑。它本身不是
的表达,因为
和
不在
的词汇中。相反,它们在英语中用作变量,这些变量在
的表达式范围内变化。这样的变量被称为 *元变量*,而使用
和元变量的词汇的表达式被称为 *元逻辑表达式*。假设我们让
为
并且
为
那么 (1) 变成
'
'
'
'
'
'
这与我们想要的并不一样。相反,我们将 (1) 解释为(使用明确的引号)
- 由 '
' 后跟
后跟 '
' 后跟
后跟 '
' 组成。
遵循这种约定的显式引号被称为 *Quine 引号* 或 *角引号*。我们的角引号将是隐式的。
我们介绍(或在某些情况下重复)一些有用的句法术语。
- 我们区分表达式(或公式)和表达式的 *出现*(或公式)。公式

无论写多少次都是同一个公式。然而,它包含句子字母
的三个出现和句子连接词
的两个出现。
是
的一个 子公式 当且仅当
和
都是公式,并且
包含
的一个出现。
是
的一个 真子公式 当且仅当 (i)
是
的子公式,并且 (ii)
与
不是同一个公式。
- 一个 原子公式 或者 原子句子 仅仅包含一个句子字母。或者换句话说,它是一个没有句子连接词的公式。一个 分子公式 或者 分子句子 包含至少一个句子连接词的出现。
- 一个分子公式的 主连接词 是在根据上述规则构建公式时添加的最后一个连接词的出现。
- 一个 否定 是一个形如
的公式,其中
是一个公式。
- 合取式是指形如
的公式,其中
和
都是公式。在这种情况下,
和
都是合取项。
- 析取式是指形如
的公式,其中
和
都是公式。在这种情况下,
和
都是析取项。
- 条件句 是一种形式为
的公式,其中
和
都是公式。在这种情况下,
是前件,而
是后件。
的逆命题 是
。
的逆否命题 是
.
- 双条件句 是一种形式为
的公式,其中
和
都是公式。

根据规则 (i),所有句子字母,包括

都是公式。然后,根据规则 (ii-a),否定

也是一个公式。然后根据规则 (ii-c) 和 (ii-b),我们得到析取和合取

作为公式。再次应用规则 (ii-a),我们得到否定

作为公式。最后,规则 (ii-c) 生成 (1) 的条件句,所以它也是一个公式。

这似乎是由规则 (ii-c) 从

其中第二个是根据规则 (i) 的公式。但第一个呢?它必须由规则 (ii-b) 从

但

不能通过规则 (ii-a) 生成。所以 (2) 不是公式。
在 命题语言 中,我们对命题语言给出了一个非正式的描述,即
。我们也已经给出了
的 形式语法。我们正式的语法生成大量的括号。这使得形式定义和其他规范更容易编写,但也使语言使用起来相当笨拙。此外,所有下标和上标很快就会变得不必要地繁琐。最终结果是一种丑陋且难以阅读的语言。
我们将在指定形式时继续使用正式语法。但是,我们将非正式地使用一个不太笨拙的变体用于其他目的。以下转换规则将
的正式公式转换为我们的非正式变体。
我们按照以下方式创建正式
公式的非正式变体。这些示例是累积的。
- 正式语法要求句子字母带有上标“0”。在上标逻辑出现之前,上标并不是必需的,甚至没有用,所以我们将在非正式变体中始终省略它们。例如,我们将写
而不是
。
- 如果下标是“0”,我们将省略它。因此,我们将写
而不是
。但是,我们不能省略所有下标;我们仍然需要写,例如,
。

- 而不是

- 我们将让一系列相同的二元连接符在右侧关联。例如,我们可以将正式的

- 转换为非正式的

- 但是,对于以下情况,我们能做的最好的就是

- 是

- 我们将使用优先级排序,尽可能省略内部括号。例如,我们将认为
的优先级(范围)低于
。这使我们能够写成

- 而不是

- 但是,我们无法从

- 中删除内部括号。我们对这个公式的非正式变体是

- 完整的优先级排序如下所示。
优先级排序表示我们评估命题连接词的顺序。
的优先级高于
。因此,在计算

的真值时,我们首先评估

首先。作用域是指由连接词支配的表达式的长度。在(1)中,
的作用域比
的作用域更广。因此,(1)中
支配整个句子,而(1)中
仅支配(1)中(2)的出现。
从最高优先级(最窄作用域)到最低优先级(最广作用域)的完整排序如下所示:
|
 |
|
最高优先级(最窄作用域) |
|
 |
|
|
|
 |
|
|
|
 |
|
|
|
 |
|
最低优先级(最广作用域) |
让我们看一些例子。首先:

可以非正式地写成

其次:

可以非正式地写成

有些额外的括号可能对理解有帮助。在上例中,非正式的变体可能更容易阅读,如

以及

注意非正式公式

恢复为官方形式

相反,非正式公式

恢复为官方形式

对于“狗叫”,英语语法指定它由一个复数名词后跟一个不及物动词组成。英语语义学对“狗叫”的含义进行指定,即狗叫。
在命题语言中,我们对
给出了一个非正式的描述。我们还给出了形式语法。然而,在这一点上,我们的语言只是一个玩具,一个我们可以像串珠一样串起来的符号集合。我们确实有关于这些符号如何排序的规则。但在这一点上,这些规则也可能只是美学规则。良好格式的公式和格式错误的表达之间的区别,还没有比漂亮和丑陋的项链之间的区别更重要。为了使我们的语言具有任何意义,能够用于表达事物,我们需要一个形式语义。
任何给定的形式语言都可以与许多相互竞争的语义规则集中的任何一个配对。我们在这里定义的语义是现代逻辑的常用语义。然而,人们已经提出了替代的语义规则集。
的替代语义规则集包括(但当然不限于)直觉逻辑、相关逻辑、非单调逻辑和多值逻辑。
像
这样的形式语言的形式语义分为两部分。
- 指定解释的规则。一个解释将语义值赋予形式语法的非逻辑符号。形式语言的语义将指定可以将哪些范围的值赋予哪些类别的非逻辑符号。
只有一类非逻辑符号,因此这里的规则特别简单。命题语言的解释是赋值,即对句子字母的真值赋值。在谓词逻辑中,我们将遇到除了赋值之外还包含其他元素的解释。
- 将语义值赋予语言中较大的表达式的规则。对于命题逻辑,这些规则根据赋予较小公式的真值来赋予较大公式的真值。对于更复杂的语法(例如,用于谓词逻辑),以更复杂的方式赋值。
一个扩展赋值根据赋值将真值赋予
(或类似的命题语言)的分子公式。句子字母的赋值通过一组规则扩展以涵盖所有公式。
我们可以给出一个(部分)赋值
作为




(请记住,我们省略了上标来缩写句子字母。)
通常,我们只对几个句子字母的真值感兴趣。赋予其他句子字母的真值可以是随机的。
给定这个赋值,我们说
![{\displaystyle {\mathfrak {v}}[\mathrm {P_{0}} ]\ =\ {\mbox{True}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ebced4e093fec5549c19e71009bbfe61150bcb32)
![{\displaystyle {\mathfrak {v}}[\mathrm {P_{1}} ]\ =\ {\mbox{False}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a3abfe7bf710089ee4a80f78e285d70c5e2ac288)
![{\displaystyle {\mathfrak {v}}[\mathrm {P_{2}} ]\ =\ {\mbox{False}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/421c4ef2a1afc19e7f41c997a4c24a8d16ae5df1)
![{\displaystyle {\mathfrak {v}}[\mathrm {P_{3}} ]\ =\ {\mbox{False}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d825606df7242317bd0a3a3ded2cde67c2c0e41b)
实际上,我们可以将赋值定义为一个函数,其参数是句子字母,值是真值(因此称为“真值”)。需要注意的是,
对于句子字母没有固定的解释或赋值。相反,我们为临时使用指定解释。
扩展解释根据给定的解释生成较长句子的真值。对于命题逻辑,解释是赋值,因此扩展解释是扩展赋值。我们定义赋值的扩展
如下。
对于所有句子字母
![{\displaystyle {\mbox{ii.}}\quad {\overline {\mathfrak {v}}}[\lnot \varphi ]\ =\ {\begin{cases}{\mbox{True}}&{\mbox{if}}\ {\overline {\mathfrak {v}}}[\varphi ]={\mbox{False}};\\{\mbox{False}}&{\mbox{otherwise (i.e., if}}\ {\overline {\mathfrak {v}}}[\varphi ]={\mbox{True).}}\end{cases}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d273839318730f629b864f7ee2b347b77a3d6d18)
![{\displaystyle {\mbox{iii.}}\quad {\overline {\mathfrak {v}}}[(\varphi \land \psi )]\ =\ {\begin{cases}{\mbox{True}}&{\mbox{if}}\ {\overline {\mathfrak {v}}}[\varphi ]={\overline {\mathfrak {v}}}[\psi ]={\mbox{True}};\\{\mbox{False}}&{\mbox{otherwise}}.\end{cases}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/beee36cb5bd2db11eba8ff28102b09ab55455d54)
![{\displaystyle {\mbox{iv.}}\quad {\overline {\mathfrak {v}}}[(\varphi \lor \psi )]\ =\ {\begin{cases}{\mbox{True}}&{\mbox{if}}\ {\overline {\mathfrak {v}}}[\varphi ]={\mbox{True}}\ {\mbox{or}}\ {\overline {\mathfrak {v}}}[\psi ]={\mbox{True}}\ {\mbox{(or both)}};\\{\mbox{False}}&{\mbox{otherwise}}.\end{cases}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f77ad1978590950a29bfe27fb9eb4961336aba1e)
![{\displaystyle {\mbox{v.}}\quad {\overline {\mathfrak {v}}}[(\varphi \rightarrow \psi )]\ =\ {\begin{cases}{\mbox{True}}&{\mbox{if}}\ {\overline {\mathfrak {v}}}[\varphi ]={\mbox{False}}\ \ {\mbox{or}}\ \ {\overline {\mathfrak {v}}}[\psi ]={\mbox{True}}\ \ {\mbox{(or both)}};\\{\mbox{False}}&{\mbox{otherwise.}}\end{cases}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/58609bb31fc2cf95154d2548c4186fc7b32222a83)
![{\displaystyle {\mbox{vi.}}\quad {\overline {\mathfrak {v}}}[(\varphi \leftrightarrow \psi )]\ =\ {\begin{cases}{\mbox{True}}&{\mbox{if}}\ {\overline {\mathfrak {v}}}[\varphi ]={\overline {\mathfrak {v}}}[\psi ];\\{\mbox{False}}&{\mbox{otherwise}}.\end{cases}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c7992cb4fd370092b7de8c79b88af3968e0ec08)
我们将确定给定两种赋值后此示例句子的真值。

首先,考虑以下赋值



(2) 根据条款 (i)
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {P} ]\ =\ {\mbox{True}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78cdb69761b884faa72b30db3cff8fc4a327856f)
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {Q} ]\ =\ {\mbox{True}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6d0efa7a915fac7ef962d0f2f6ccb28929c35307)
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {R} ]\ =\ {\mbox{False}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ec51568f30e8f378d378aff08b4e904288acc51c)
(3) 根据 (1) 和条款 (iii),
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {P} \land \mathrm {Q} ]\ =\ {\mbox{True}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/11cae0180cab0f6442791354b034e77a9fb6aebb)
(4) 根据 (1) 和条款 (iv),
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {Q} \lor \mathrm {R} ]\ =\ {\mbox{True}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a210367b901f58d46e5dc0bfa02614aed0e4a5cf)
(5) 根据 (4) 和条款 (v),
![{\displaystyle {\overline {\mathfrak {v}}}[\lnot (\mathrm {Q} \lor \mathrm {R} )]\ =\ {\mbox{False}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/16c3679ea35b0aaa6a8d6f46967b89f9d120ef0b)
(6) 根据 (3)、(5) 和条款 (v),
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {P} \land \mathrm {Q} \rightarrow \lnot (\mathrm {Q} \lor \mathrm {R} )]\ =\ {\mbox{False}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/254c7028855c2601b10b61357fa0c82fb832fae6)
因此,在我们的解释中 (1) 是假的。
接下来,尝试评估



(7) 根据条款 (i)
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {P} ]\ =\ {\mbox{True}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78cdb69761b884faa72b30db3cff8fc4a327856f)
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {Q} ]\ =\ {\mbox{False}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fcb1a4a71fc929b4b5978178306540fac36eefe8)
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {R} ]\ =\ {\mbox{True}}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d1abbcf46ce1162c387f473031daa2f15c5f4be6)
(8) 根据 (7) 和条款 (iii),
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {P} \land \mathrm {Q} ]\ =\ {\mbox{False}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c7537741c53cf4db9db28ae3f3938c7dae033f2e)
(9) 根据 (7) 和条款 (iv),
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {Q} \lor \mathrm {R} ]\ =\ {\mbox{True}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a210367b901f58d46e5dc0bfa02614aed0e4a5cf)
(10) 根据 (9) 和条款 (v),
![{\displaystyle {\overline {\mathfrak {v}}}[\lnot (\mathrm {Q} \lor \mathrm {R} )]\ =\ {\mbox{False}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/16c3679ea35b0aaa6a8d6f46967b89f9d120ef0b)
(11) 根据 (8)、(10) 和条款 (v),
![{\displaystyle {\overline {\mathfrak {v}}}[\mathrm {P} \land \mathrm {Q} \rightarrow \lnot (\mathrm {Q} \lor \mathrm {R} )]\ =\ {\mbox{True}}.\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eb0856841a0bf2fec31c009819a0109c99900644)
因此,(1) 在这种第二个解释中是真的。请注意,我们这次做了一些比必要的工作更多。根据条款 (v),(8) 足以证明 (1) 的真值。
在形式语法中,我们之前给出了命题逻辑的形式语义。真值表是一种使用这种形式语法来计算给定解释(对句子字母分配真值)的更大公式的真值的设备。真值表也可以帮助澄清来自形式语法的材料。
我们从否定的真值表开始。它对应于我们对扩展评估的定义的条款 (ii)。
|
|
|
T |
F |
F |
T |
|
T 和 F 分别代表真和假。每行代表一种解释。第一列显示解释对句子字母
赋予的真值。在第一行,解释对
赋予了真值。在第二行,解释对
赋予了假值。
第二列显示
在给定行解释下的值。在第一行解释下,
的值为假。在第二行解释下,
的值为真。
我们可以更正式地说明。上面真值表的第一行表明,当
= 真时,
= 假。第二行表明,当
= 假时,
= 真。我们也可以更简单地说:否定句的真值与其被否定部分的真值相反。
合取的真值表对应于我们对扩展赋值的定义中的第三条。
|
|
|
|
T |
T |
T |
T |
F |
F |
F |
T |
F |
F |
F |
F |
|
这里我们有两个句子字母,因此有四种可能的解释,每种解释都用一行表示。前两列显示了四种解释对
和
的赋值。第一行表示的解释将两个句子字母都赋值为真,依此类推。最后一列显示了对
的赋值。你可以看到,当两个合取式都为真时,合取式为真——否则合取式为假,即当至少有一个合取式为假时。
析取的真值表对应于我们对扩展赋值的定义中的第 (iv) 条。
|
|
|
|
T |
T |
T |
T |
F |
T |
F |
T |
T |
F |
F |
F |
|
在这里我们看到,当至少一个析取式为真时,析取式为真——否则析取式为假,即当两个析取式都为假时。
条件句的真值表对应于我们对扩展赋值的定义中的第 (v) 条。
|
|
|
|
T |
T |
T |
T |
F |
F |
F |
T |
T |
F |
F |
T |
|
当条件句的前件为假或后件为真(或两者都为真)时,条件句为真。否则为假,即当条件句的前件为真而条件句的后件为假时。
双条件句的真值表对应于我们对扩展赋值的定义中的第 (vi) 条。
|
|
|
|
T |
T |
T |
T |
F |
F |
F |
T |
F |
F |
F |
T |
|
当双条件句的两部分具有相同的真值时,双条件句为真。当双条件句的两部分具有相反的真值时,双条件句为假。
我们将使用来自 形式语义 的相同示例句子。

我们按如下方式构建其真值表。
|
|
|
|
|
|
|
|
T |
T |
T |
T |
T |
F |
F |
T |
T |
F |
T |
T |
F |
F |
T |
F |
T |
F |
T |
F |
T |
T |
F |
F |
F |
F |
T |
T |
F |
T |
T |
F |
T |
F |
T |
F |
T |
F |
F |
T |
F |
T |
F |
F |
T |
F |
T |
F |
T |
F |
F |
F |
F |
F |
T |
T |
|
当有三个命题字母时,我们需要八个赋值(以及真值表中的八行)来覆盖所有情况。该表分部分构建示例语句。
列是基于
和
列构建的。
列是基于
和
列构建的。反过来,这也是其在下一列中否定之基础。最后,最后一列是基于
和
列构建的。
从该真值表中,我们看到当
和
都为真时,示例语句为假;其他情况下为真。
该表可以以更压缩的格式编写,如下所示。
|
|
|
|
|
(1)
|
|
(4)
|
(3)
|
|
(2)
|
|
T |
T |
T |
|
T |
|
F |
F |
|
T |
|
T |
T |
F |
|
T |
|
F |
F |
|
T |
|
T |
F |
T |
|
F |
|
T |
F |
|
T |
|
T |
F |
F |
|
F |
|
T |
T |
|
F |
|
F |
T |
T |
|
F |
|
T |
F |
|
T |
|
F |
T |
F |
|
F |
|
T |
F |
|
T |
|
F |
F |
T |
|
F |
|
T |
F |
|
T |
|
F |
F |
F |
|
F |
|
T |
T |
|
F |
|
|
连接词上方的数字不是真值表的一部分,而是显示了列的填充顺序。
在命题逻辑中,一个公式为真的解释被称为满足该公式。在谓词逻辑中,满足的概念稍微复杂一些。一个公式是可满足的 当且仅当它在至少一个解释下为真(也就是说,当且仅当至少一个解释满足该公式)。真值表 的示例真值表显示了以下语句是可满足的。

为了更简单的说明,公式
是可满足的,因为它在任何将
赋值为 True 的解释下都是真的。
我们用符号
来表示解释
满足
。如果
不满足
则我们写成
。
满足的概念也可以扩展到公式集。一个公式集是可满足的,当且仅当存在一个解释,使得该集中的每个公式在该解释下都是真的(即,该解释满足该集中的每个公式)。
一个公式是 *不可满足的*,当且仅当不存在一个解释,使得该公式在该解释下为真。一个简单的例子是

你可以通过真值表轻松验证,无论解释对
赋值什么真值,该公式都是假的。我们称不可满足的公式为 *逻辑假* 。可以认为命题逻辑中(但不包括谓词逻辑)不可满足的公式是 *重言式假* 。
一个公式是 *有效的*,当且仅当它在每个解释下都为真。例如,

是有效的。你可以通过真值表轻松验证,无论解释对
赋值什么,该公式都是真的。我们称有效的句子为 *逻辑真* 。我们称命题逻辑中(但不包括谓词逻辑)有效的公式为 *重言式* 。
我们使用符号
来表示
是有效的,并且使用
表示
是无效的。
当且仅当两个公式在完全相同的解释下为真时,它们才是等价的。您可以通过真值表轻松地确认任何满足
的解释也满足
。此外,任何满足
的解释也满足
。因此它们是等价的。
我们可以使用以下方便的符号来表示
和
是等价的。

当且仅当以下成立时为真

一个论证是指一组被指定为前提的公式,以及被指定为结论的单个句子。直观地说,我们希望这些前提共同构成相信结论的理由。就我们而言,一个论证是任何前提集加上任何结论。对于某些特别荒谬的论证来说,这可能有点人为,但论证的逻辑属性并不取决于它是否荒谬,或者是否有人实际上确实或可能认为这些前提是相信结论的理由。我们认为论证好像有人确实或可能认为这些前提是结论的理由,而不管是否有人实际确实或可能这样做。即使是空的前提集加上一个结论,也算是一个论证。
以下示例显示了使用多种符号表示的相同论证。
- 符号 1


- 因此

- 符号 2


- ∴

- 符号 3



- 符号 4
∴ 
一个论证是有效的当且仅当所有满足所有前提的解释也满足结论。一个有效论证的结论是其前提的 *逻辑结果*。我们可以用
作为其前提集,
作为其结论来表达论证的有效性(或无效性),使用以下符号。
- (1)

- (2)

例如,我们有

论证的有效性,或逻辑结果,是我们构建逻辑直觉的中心概念。我们想知道我们的论证是否是有力的论证,也就是说,它们是否代表了良好的推理。我们想知道一个论证的前提是否构成了相信结论的充分理由。有效性是良好论证的一个重要特征。它不是唯一的必要特征。至少有一个错误前提的有效论证是无用的。有效性是真值保持特征。它不告诉我们结论是正确的,只告诉我们论证的逻辑特征是,如果前提是正确的,那么结论就是正确的。具有正确前提的有效论证是 *健全的*。
一个好的论证还需要一些不太正式的特征。仅仅因为前提是正确的,并不意味着它们是可信的,我们有理由相信它们,或者我们可以收集证据来支持它们。还应该注意的是,有效性只适用于某些类型的论证,特别是 *演绎* 论证。演绎论证旨在有效。演绎论证的典型例子是数学证明。归纳论证,以科学论证为典型例子,并不旨在有效。前提的真实性并不旨在保证结论的真实性。相反,前提的真实性旨在使结论的真实性高度可能或有可能。在科学中,我们并不打算提供数学证明。相反,我们收集证据。
对于每个有效的公式,都存在一个相应的有效论证,其结论是有效的公式,前提集为空集。因此

当且仅当

对于每个具有有限多个前提的有效论证,都存在一个相应的有效公式。考虑一个具有
作为结论,其前提为
的有效论证。然后

那么,就有对应的有效公式

对于有效的论证
∴ 
有以下有效的公式

您可能会看到一些文字将我们的箭头
理解为 “蕴涵”,并使用 “蕴涵” 作为 “条件句” 的替代词。这通常被视为用词不当。在日常英语中,以下句子被认为是语法正确的
- (3) '有烟就意味着有火'。
- (4) '有烟' 蕴涵 '有火'。
在 (3) 中,我们有一个事实或命题或其他东西(哲学家们现在似乎最喜欢的是命题),它蕴涵了同类的另一个事实或命题。在 (4) 中,我们有一个句子蕴涵了另一个句子。
但是以下句子被认为是不正确的
- 有烟蕴涵有火。
这里,与 (3) 相比,没有引号。没有主体在进行蕴涵,也没有客体被蕴涵。相反,我们正在用较小的句子构成一个更大的句子,就像 “蕴涵” 是一个语法连词,例如 “当且仅当”。
因此,逻辑学家倾向于避免使用 “蕴涵” 来表示 条件句。相反,他们使用 “蕴涵” 来表示 具有逻辑结果,并使用 “蕴涵” 来表示 有效的论证。这样做时,他们遵循的是 (4) 的模型,而不是 (3) 的模型。特别是,他们将 (1) 和 (2) 理解为 '
蕴涵(或不蕴涵)
。
一个包含 n 个句子字母的公式,其 真值表 中需要
行。对于一个包含 m 行的真值表,有
种可能的公式。因此,对于一个包含 n 个字母的句子,
,可能的公式数量为
。
例如,一个句子字母有四种可能的公式(需要一个两行真值表),而两个句子字母有 16 种可能的公式(需要一个四行真值表)。我们用以下表格来说明这一点。编号列代表主连接符列的不同可能性。
|
|
(i) |
(ii) |
(iii) |
(iv) |
T |
T |
T |
F |
F |
F |
T |
F |
T |
F |
|
列 (iii) 是之前介绍的否定公式 earlier。
|
|
|
(i) |
(ii) |
(iii) |
(iv) |
(v) |
(vi) |
(vii) |
(viii) |
(ix) |
(x) |
(xi) |
(xii) |
(xiii) |
(xiv) |
(xv) |
(xvi) |
T |
T |
T |
T |
T |
T |
T |
T |
T |
T |
F |
F |
F |
F |
F |
F |
F |
F |
T |
F |
T |
T |
T |
T |
F |
F |
F |
F |
T |
T |
T |
T |
F |
F |
F |
F |
F |
T |
T |
T |
F |
F |
T |
T |
F |
F |
T |
T |
F |
F |
T |
T |
F |
F |
F |
F |
T |
F |
T |
F |
T |
F |
T |
F |
T |
F |
T |
F |
T |
F |
T |
F |
|
列 (ii) 代表析取公式,列 (v) 代表条件句,列 (vii) 代表双条件句,列 (viii) 代表合取。
我们现在开始讨论一个问题:是否拥有足够的连接词来表达任意数量的句子字母的所有公式。请记住,每一行代表一个赋值。我们可以通过将赋值为真值的那个句子字母进行合取,并将赋值为假值的句子字母进行否定,然后将这些结果进行合取来表达这个赋值。上面第二个表格中的四个赋值可以表达为:




现在,我们可以通过对公式值为真的赋值进行析取来表达任意公式。例如,我们可以用以下公式来表达第 (x) 列:
- (1)

你可以通过完成真值表来确认这个公式是否产生了预期的结果。当 (a)
为真且
为假,或 (b)
为假且
为真时,这个公式为真。有一个更简单的表达方法:
。想出一个简单的表达任意公式的方法可能需要一些洞察力,但至少我们有一种自动机制可以找到某种方法来表达它。
现在让我们考虑第二个例子。我们想表达一个由
,
和
组成的公式,并且我们希望这个公式只在以下三个赋值下为真值。
|
|
|
(i) |
|
(ii) |
|
(iii) |
|
|
|
真 |
|
假 |
|
假 |
|
|
|
真 |
|
真 |
|
假 |
|
|
|
假 |
|
假 |
|
真 |
我们可以将产生真值的三个条件表达为



现在我们需要说第一个条件成立,或者第二个条件成立,或者第三个条件成立。
- (2)

你可以通过真值表验证它是否产生了想要的结果,即该公式仅在上文的解释中为真。
这种表达任意公式的技术不适用于在所有解释中都为假的公式。我们至少需要一个解释结果为真,才能开始这个公式。然而,我们可以使用任何永假的公式来表达这些公式。
就足够了。
范式提供了一个标准化的表达规则,任何公式都等效于符合该规则的公式。在下文中,将定义文字为句子字母或其否定(例如
和
以及
和
)。
我们说一个公式处于析取范式,如果它是一个文字的合取的析取。例如
。为了这个定义的目的,我们允许所谓的退化的析取和合取,它们只包含一个析取项或合取项。因此,我们将
视为处于析取范式,因为它是一个退化的(单值)析取,它包含一个退化的(单值)合取。可以通过将其转换为等效公式
来消除退化。为了这个定义的目的,我们还允许多值的析取和合取,例如
。上面显示了一种找到任意公式的析取范式的方法。
在命题逻辑中,另一种常见的范式是合取范式。如果一个公式是文字的析取的合取,那么它就处于合取范式。例如
。同样地,我们可以用合取范式表达任意公式。首先,取公式求值为 False 的那些赋值。对于每个这样的赋值,形成一个析取,这个析取包含赋值为 False 的句子字母以及赋值为 True 的句子字母的否定。对于赋值
: False
: True
: False
我们形成析取

任意公式的合取范式表达式是所有与公式求值为 False 的解释相匹配的这些析取的合取。上面 (1) 的合取范式等价形式是

上面 (2) 的合取范式等价形式是

否定和合取足以表达其他三个连接词,以及任何任意公式。



否定和析取足以表达其他三个连接词,实际上可以表达任何任意公式。



否定和条件足以表达其他三个连接词,实际上可以表达任何任意的公式。



否定和双条件不足以表达其他三个连接词。
我们已经看到,三对连接词中的每一对都可以共同表达任意公式。由此引出一个问题:是否可以用一个连接词来表达任意公式?答案是肯定的,但不能用我们现有的任何连接词。如果在
中添加以下两个二元连接词中的任何一个,那么它将足以表达任意公式。
选择否定,有时被称为NAND。这个连接词通常用谢弗竖线符号表示,写成
(一些作者使用 ↑)。在
中临时添加符号
,并令
在
或
中至少有一个为假时为真。它的真值表如下:
|
|
|
|
T |
T |
F |
T |
F |
T |
F |
T |
T |
F |
F |
T |
|
现在我们有以下等价关系。





联合否定,有时称为NOR。暂时将符号
添加到
中,并令
在
和
都为假时为真。它的真值表如下
|
|
|
|
T |
T |
F |
T |
F |
F |
F |
T |
F |
F |
F |
T |
|
现在我们有以下等价关系。





这里列出了一些比较有名的、历史重要的或有用的等价和同义反复。这些等价和同义反复可以添加到连接词的相互定义中列出的等价和同义反复。我们可以在这里继续列出很多,但会尽量使列表保持简洁。请记住,对于
和
的每个等价,都存在一个相关的同义反复
.
每个公式只有一个真值。
排中律
矛盾律
算术中的一些熟悉定律在命题逻辑中也有类似的定律。
条件和双条件(但不是合取和析取)是自反的。


合取、析取和双条件(但不是条件)是可交换的。



合取、析取和双条件式(但非条件式)都是结合的。



我们列出了十条分配律。其中,最重要的可能是合取和析取互相分配,以及条件式自身分配。










合取、条件和双条件(但不包括析取)是传递的。



这些重言式和等价式主要与条件句相关。



条件加法
条件加法
逆否命题
导出规则
这些重言式和等价关系大多与双条件语句有关。
双条件加法
双条件加法


我们重复可表达性部分的可表达性中的德摩根定律,并添加两种附加形式。我们还列出了一些额外的重言式和等价式。
幂等对于合取
幂等对于析取
析取加法
析取加法

德摩根定律
德摩根定律
德摩根定律
德摩根定律
双重否定律
以下两个原则将在后面的页面中用于构建我们的推导系统。它们很容易被证明,但由于它们既不是重言式也不是等价式,所以仅仅用真值表不足以做到这一点。我们在这里不会尝试证明。
令
和
都是公式,令
是一组公式。

令
和
都是公式,令
是一组公式。


本页将使用在 Formal Logic/Sentential Logic/Formal Syntax 的“Additional terminology” 部分介绍的 occurrence 和 subformula 概念。这些概念自那时起很少使用,因此您可能需要回顾一下。
我们已经介绍了一些重言式,例如
- (1)

使用元变量
和
替换 (1) 中的
和
。这产生了形式
- (2)

事实证明,任何匹配此形式的公式都是重言式。因此,例如,令
和
。那么,
- (3)

是一个重言式。此过程可以推广到所有重言式:对于任何重言式,通过用不同的元变量(如(2)中所示,用希腊字母表示)替换每个句子字母来找到其显式形式。我们可以将其称为 *重言式形式*,它是元逻辑表达式而不是公式。此重言式形式的任何实例都是重言式。
前面说明了如何通过重言式形式从旧重言式生成新重言式。在这里,我们将展示如何不借助重言式形式来生成重言式。为此,我们定义了公式的替换实例。任何重言式的替换实例也是重言式。
首先,我们定义了公式对句子字母的简单替换实例。令
和
是公式,而
是句子字母。*简单替换实例*
是将
中 *所有* 出现的
替换为
所得到的结果。*公式对句子字母的替换实例* 是简单替换实例链的结果。特别是,从
开始的零个简单替换实例链是替换实例,实际上就是
本身。因此,任何公式都是其自身的替换实例。
事实证明,如果
是重言式,则任何简单替换实例
也是重言式。如果我们从重言式开始并生成简单替换实例链,那么链中的每个公式也是重言式。因此,重言式的任何(不一定是简单的)替换实例也是重言式。
再次考虑 (1)。我们将
替换为 (1) 中所有出现的
。这给了我们 (1) 的以下简单替换实例
- (4)

在这里,我们将
代替
。这样我们就得到了 (3) 作为 (4) 的一个简单的替换实例。由于 (3) 是两个简单替换实例链的结果,因此它是 (1) 的一个 (非简单) 替换实例。由于 (1) 是一个重言式,所以 (3) 也是一个重言式。我们可以将替换链表示为
![{\displaystyle \mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )[\mathrm {Q} /\mathrm {R} \land \mathrm {S} ][\mathrm {P} /\mathrm {P} \lor \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/81271051059723595e8d452d27da89f1af994693)
再举一个例子,同样从 (1) 开始。我们想要得到
- (5)

我们的第一次尝试可能是用
代替
,
- (6)

这确实是一个重言式,但它不是我们想要的那个。相反,我们在 (1) 中用
代替
,得到

现在用
代替
,得到

最后,将
代入
得到我们想要的结果,即 (5)。由于 (1) 是重言式,所以 (5) 也是重言式。我们可以将替换链表示为
![{\displaystyle \mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )[\mathrm {P} /\mathrm {R} ][\mathrm {Q} /\mathrm {P} ][\mathrm {R} /\mathrm {Q} ]\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3a6dac03fc4768317ce9e57ee664b4a38cd4dfcf)
我们可以将一系列简单替换压缩成单个复杂替换。设
、
、
、... 为公式;设
、
、... 为句子字母。我们定义一个*公式对句子字母的同步替换实例*
为从
开始,同时将
替换为
、
替换为
、.... 我们可以重新生成我们的示例。
之前生成的公式 (3) 是
![{\displaystyle \mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )[\mathrm {P} /\mathrm {P} \lor \mathrm {Q} ,\mathrm {Q} /\mathrm {R} \land \mathrm {S} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/86e6d375945f1499a1f619e0362ac3cb4bec2b09)
类似地,(5) 是
![{\displaystyle \mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )[\mathrm {P} /\mathrm {Q} ,\ \mathrm {Q} /\mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e422947c6c27eebd07aa0cf66ed74321e18f1561)
最后 (6) 是
![{\displaystyle \mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )[\mathrm {Q} /\mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dfca8b9e7c07ffb3fd96e9180eda01663234be6f)
当我们进入谓词逻辑时,不会有同时替换实例可用。这就是我们通过引用一系列简单替换实例而不是同时替换实例来定义 *替换实例* 的原因。
我们之前在 命题连接词的性质 中看到了以下等价关系
- (7)

然后您可能会期望以下等价关系

这个预期是正确的;这两个公式是等价的。令
和
为等价公式。令
为一个公式,其中
作为子公式出现。最后,令
为在
中至少替换一个(不一定是全部)
为
所得的结果。那么
和
是等价的。这种替换被称为交换。
另一个例子,假设我们想要生成等价关系
- (8)

我们注意到以下等价关系
- (9)

这两个公式可以通过真值表来验证,或者更简单地,将 (7) 中的两个公式中的
替换为
来确认。
这种替换确实将 (9) 确立为一个等价关系。我们已经注意到,
和
等价当且仅当
是一个重言式。根据 (7),我们得到重言式

然后我们的替换得到

这也是一个重言式。那么相应的等价关系就是 (9)。
根据 (9),我们现在可以将
的后件替换为其等价关系。这将产生我们想要的等价关系,即 (8)。
每个与重言式等价的公式也是重言式。因此,在重言式中交换等价的子公式将得到一个重言式。例如,我们可以使用 (7) 的替换实例

以及我们之前在 命题联结词性质 中看到的重言式

得到

作为一个新的重言式。
作为示例,我们将使用 联结词的可互定义性 来用条件语句和否定来表达
- (10)

。
基于

我们得到了替换实例

这反过来又允许我们替换 (10) 中的相应子公式,得到
- (11)

等价关系

以及适当的替换,给了我们
- (12)

与 (11) 等价。
最后,应用

以及适当的替换,得到我们的最终结果

本页提出了两个论点。
- 给定一个公式,将子公式替换为等价公式的结果是与给定公式等价的公式。
这些断言并非微不足道的观察或简单的真值表的结论。它们是需要证明的实质性断言。证明可以在许多标准的元逻辑教科书中找到,但此处不予展示。
页面 命题语言 简要介绍了英语和
之间的翻译。我们将在本文中更详细地探讨这一问题。
在下文中,我们假设将以下英语句子分配给
的命题字母
2 是一个质数。
2 是一个偶数。
3 是一个偶数。
将
翻译成英语的规范方法是“并非”。根据上述分配,
- (1)

翻译成
- 并非 2 是一个质数。
但我们通常用“不是”或在词尾加“不”来表示英语中的否定。因此,(1) 也可以翻译成以下两种方式:
- 2 不是一个质数。
- 2 不是一个质数。
将
翻译成英语的规范方法是“如果……那么……”。因此
- (2)

翻译成英语为
- (3) 如果 2 是一个质数,那么 2 是一个偶数。
人们对规范翻译提出了一些异议,我们的例子可能说明了这个问题。将 (3) 视为真似乎很奇怪;然而,我们的语义规则确实将 (2) 视为真(因为
和
都是真的)。我们可能希望,如果一个条件语句及其前件为真,那么后件也是真的,因为前件为真。也许我们希望有一个通用的规则
- (4) 如果 x 是一个质数,那么 x 是一个偶数
为真——但这条规则显然是假的。无论如何,我们通常希望前件的真值(如果它确实是真)与结论的真值(如果它确实是真)在某种程度上是相关的。(2) 是一个例外,因为一个数字是质数与这个数字是偶数之间通常不存在相关性。
的条件式
被称为实质条件,以区别于严格条件或反事实条件。 关联逻辑试图定义一个符合这些反对意见的条件式。 另请参阅斯坦福哲学百科全书关于关联逻辑的条目。
如今人们普遍认为,并非表达的语言使用的所有方面都属于其语言意义的一部分。 有人认为,将“if”解读为实质条件式的反对意见是基于会话含义,而不是基于“if”的意义。 有关更多信息,请参阅斯坦福哲学百科全书关于会话含义的条目。 尽管这更像是一个简化假设,但我们将采用这种观点。 我们也可以在我们的辩护中指出,翻译不需要完全准确才能有用。 即使我们的简化假设是错误的,
仍然是
中最接近“if”的表达方式。 还应该注意的是,在数学陈述和证明中,数学家始终将“if”用作实质条件式。 他们接受 (2) 和 (3) 作为彼此的翻译,并且不觉得将 (3) 视为真有什么奇怪。
“If”可以出现在条件式的开头或中间。 “Then”可以省略。 因此,以下两者(以及 (3))都翻译成 (2)。
- 如果 2 是一个素数,那么 2 是一个偶数。
- 2 是一个偶数,如果 2 是一个素数。
我们不将“implies”翻译成
。 特别地,我们拒绝
- 2 是一个素数,蕴含 2 是一个偶数。
因为它是语法上不正确的,因此不能翻译成 (2)。 有关更多详细信息,请参阅蕴含部分的有效性。
英文
- (5) 2 是一个素数,当且仅当 2 是一个偶数
等同于英文
- 如果 2 不是一个偶数,那么 2 不是一个素数。
这反过来翻译成
为
- (6)

我们在条件式部分的命题连接词的性质中看到,(6) 等同于
- (7)

许多逻辑书籍将此作为 (5) 翻译成
的首选翻译。 这允许使用方便的规则“if”始终引入一个前件,而“only if”始终引入一个后件。
与“if”一样,“only if”也可以出现在条件式的第一个位置或中间位置。 (5) 等同于
- 当且仅当 2 是一个偶数,2 才是一个素数。
“如果”——以及类似的表达,例如“假设”和“如果”——可以与“if”等效地使用。 因此,以下每个都翻译成
为 (2)。
- 2 是一个偶数,如果 2 是一个素数。
- 2 是一个偶数,假设 2 是一个素数。
- 如果 2 是素数,那么 2 是偶数。
在 "provided that" 前面加上 "only" 与在 "if" 前面加上 "only" 意义相同。因此以下每个句子都可翻译为
,如 (6) 或 (7)。
- 只有当 2 是偶数时,2 才是素数。
- 只有假设 2 是偶数时,2 才是素数。
- 只有当 2 是偶数时,2 才是素数。
将
翻译成英文是 "[either] ... or ..."(其中 "either" 可选)。因此
- (8)

翻译成英语为
- (9) 2 是素数或 2 是偶数
或者
- 2 是素数或 2 是偶数。
我们在 可表达性的连接词互定 部分看到 (8) 等价于

正如将 "if" 理解为
会引发争议,将 "or" 理解为
也存在类似的争议。我们将再次做出简化的假设,忽略这些争议。
英文中的 "or" 既有包含性也有——有点争议——排他性用法。当至少有一个析取式为真时,包含性或 为真;当恰好有一个析取式为真时,排他性或 为真。
运算符与包含性用法相匹配。包含性用法在否定中尤为明显。如果布什总统承诺不入侵伊朗或朝鲜,即使是最优秀的共和党说客也不会声称他可以通过入侵两国来履行诺言。对 (9) 的排他性解读翻译成
如下所示:

或者更简单地(不太直观)为

在英文中,可以使用 "or" 进行缩略。因此,(8) 翻译为
- 2 是素数或偶数。
同样地,

翻译为
- 2 或 3 是偶数。
"Unless" 与 "if not" 含义相同。因此
- (10)

翻译为
- (11) 2 是素数,除非 2 是偶数。
以及
- (12) 除非 2 是偶数,否则 2 是素数。
我们在连接词的可互定义性部分的表达能力中看到 (10) 等价于 (8)。许多逻辑书籍将 (8) 作为 (11) 或 (12) 翻译成
的首选翻译。
在联合否定部分的表达能力中,我们暂时将
添加到
作为联合否定的连接词。如果我们仍然可以使用该连接词,我们可以翻译
- 2 不是素数,也不是偶数。
为
.
然而,由于
实际上并不在
的词汇表中,我们需要进行改写。以下任一方法都可行
- (13)
.
- (14)
.
与“或”一样,也适用于相同的望远镜。
- 2 既不是素数,也不是偶数。
翻译成
为 (13) 或 (14)。同样地,
- 2 和 3 都不为偶数。
翻译为以下任一:
.
.
将
翻译成英文的典型形式是“‘[both] … and …’” (其中“both” 可选)。因此
- (15)

翻译成英语为
- 2 是素数,并且 2 是偶数。
或者
- 2 是素数,并且 2 是偶数。
我们将“and” 翻译成
的做法并不特别有争议。但是,“and” 有时用于表达时间顺序。以下两个句子
- 她结婚了,然后怀孕了。
- 她怀孕了,然后结婚了。
通常听起来有很大不同。
“And” 与“or” 一样,具有相同的望远镜效果。
- 2 既是素数,又是偶数。
翻译成
,如 (15)
- 2 和 3 都是偶数。
翻译成
.
到英文的标准翻译是 "... if and only if ...". 因此
- (16)

翻译成英语为
- 2 是一个质数当且仅当 2 是一个偶数。
英文句子
- (17) 2 是一个质数当且仅当 2 是一个偶数
是
- 2 是一个质数如果 2 是一个偶数,并且 2 是一个质数只有当 2 是一个偶数
的简化形式,翻译成

或更简洁地表示为等效公式
- (18)
.
我们在 连接词的可互定义性 部分看到了, (18) 等价于 (16)。关于 'if' 的物质解释和非物质解释的问题也适用于 'if and only if'。
数学家和有时其他人使用 'iff' 作为 'if and only if' 的简写形式。所以
- 2 是一个质数当且仅当 2 是一个偶数
是 (17) 的简写形式,并翻译成 (16)。
在 有效性 中,我们引入了公式和论证的有效性概念。在命题逻辑中,有效的公式是重言式。到目前为止,我们可以通过以下方式显示公式
是有效的(重言式)。
- 为
制作真值表。
- 获得
作为已知有效的公式的替换实例。
- 通过将等价交换应用于已知有效的公式来获得
。
然而,这些方法在谓词逻辑中失效,因为谓词没有真值表。如果没有替代方法,我们就无法使用第二种和第三种方法,因为它们依赖于知道其他公式的有效性。显示公式有效的另一种方法——不使用真值表——是使用推导。本页和后面的页面介绍了这种技术。注意,声称推导显示论证有效假设了一个健全的推导系统,参见下面的健全性。
推导是一系列编号的行,每行包含一个带有注释的公式。注释提供了将该行添加到推导中的理由。推导是数学证明的高度形式化的模拟——或者可能是模型。
典型的推导系统将允许以下类型的行
- 一行可以是公理。推导系统可以指定一组公式作为公理。这些公理被接受为任何推导的真值。对于命题逻辑,公理集是所有重言式的固定子集。
- 一行可以是假设。推导可以包含几种类型的假设。以下内容涵盖了标准情况。
- 前提。在试图证明论证的有效性时,可以假设该论证的前提。
- 用于子推导的临时假设。这种假设旨在仅在推导的一部分中生效,并且必须在推导被认为完成之前被解除(变为无效)。子推导将在后面的页面中介绍。
- 一行可以是将推理规则应用于先前行的结果。推理是先前行的语法转换,用于生成新行。推理必须遵循推导系统定义的固定模式之一。这些模式是系统的推理规则。其思想是,任何符合推理规则的推理都应该是有效的论证。
我们在形式语义学中注意到,像
这样的形式语言可以通过几种替代甚至相互竞争的语义规则集来解释。对于给定的语法语义对,也可以定义多个推导系统。包含形式语法、形式语义和推导系统的三元组是一个逻辑系统。
推导旨在证明论证的有效性。零前提论证的推导旨在证明其结论是有效的公式——在命题逻辑中,这意味着证明它是重言式。对于给定的逻辑系统,如果推导系统实现了这些目标,则称该推导系统为健全。也就是说,一个推导系统是健全(具有健全性属性)的,如果其推导系统中可推导的每个公式(和论证)都是有效的(给定语法和语义)。
推导系统另一个理想的特性是完备性。对于给定的逻辑系统,如果其推导系统可以推导出所有有效的公式,则称该推导系统为完备。但是,对于某些逻辑,不存在任何推导系统是或可以是完备的。
健全性和完备性是重要的结果。它们的证明在此不予给出,但可以在许多标准的元逻辑教科书中找到。
符号有时被称为转置符号,特别是语义转置符号。我们之前介绍了该符号的以下三种用法。
|
(1)
|
|
|
|
满足 . |
|
(2)
|
|
|
|
是有效的。 |
|
(3)
|
|
|
|
蕴含(作为逻辑结果) . |
其中
是一个赋值,而
是一组前提,如有效性中所介绍的。
推导有语义转置符号的对应物,即语法转置符号。上面的项目 (1) 没有语法对应物。但是,上面的 (2) 和 (3) 有以下对应物。
|
(4)
|
|
|
|
是可证的。 |
|
(5)
|
|
|
|
证明(具有推导结果) . |
项目(4)的情况当且仅当存在
从无前提的正确推导。同样地,(5)的情况当且仅当存在
的正确推导,它将
的成员作为前提。
上面(4)和(5)的否定是
|
(6)
|
|
|
|
(7)
|
|
|
现在我们可以定义健全性和完备性如下


推理规则将以以下示例的格式显示。
- 条件消去 (CE)



这个推理规则的名称是“条件消去”,缩写为“CE”。如果在线上方的公式形式作为推导中的活动行出现,则可以应用此规则。这些称为此推理的前件行。应用此规则将添加一个具有在线下方的形式的公式。这称为此推理的后件行。新推导的行文本的注释是前件行的行号和缩写“CE”。
注意。您可能会看到前提行和结论行来代替前件行和后件行。您也可能会看到其他术语,因为大多数教科书在这里避免给出任何特殊的术语。
每个命题连接词将有两个推理规则,分别对应以下类型。
- 一个引入规则。给定连接词的引入规则允许我们推导出一个以给定连接词作为主连接词的公式。
- 一个消去规则。给定连接词的消去规则允许我们使用已经出现在推导中的公式,该公式以给定连接词作为主连接词。
三个规则(否定引入、否定消去和条件引入)将推迟到下一页。这些是所谓的放电规则,将在我们讨论子推导时解释。
三个规则(合取消去、析取引入和双条件消去)将分别有两个形式。我们任意地将这两种模式视为同一规则的形式,而不是独立的规则。
本页上推理的有效性可以通过真值表来证明。
否定引入 (NI)
- 推迟到下一页。
否定消去 (NE)
- 推迟到下一页。
合取引入 (KI)



合取引入传统上被称为并置或合取。
合取消去,形式一 (KE)


合取消去,形式二 (KE)


合取消去传统上被称为简化。
析取引入,形式一 (DI)


析取引入,形式二 (DI)


析取引入传统上被称为加法。
析取消去 (DE)




析取消去传统上被称为案例分离。
条件句引入 (CI)
- 推迟到下一页。
条件消去 (CE)



条件句消去传统上被称为拉丁语名称肯定前件或不太常使用地被称为肯定前件。
双条件句引入 (BI)



双条件句消去,形式一 (BE)



双条件句消去,形式二 (BE)



推理规则很容易应用。从以下两行
- (1)

以及
- (2)

我们可以使用条件消去来添加
- (3)

到推导中。
注释将是 (1) 和 (2) 的行号以及条件消去的缩写,即“1, 2, CE”。前件行的顺序并不重要;无论 (1) 出现于 (2) 之前还是之后,该推理都是允许的。
必须记住,推理规则是严格的句法规则。语义上明显的变体是不允许的。例如,不允许从 (1) 和
- (4)

推导出 (3)。然而,你可以通过首先推导出
- (5)

以及
- (6)

使用合取消去 (KE) 从 (1) 和 (4) 中得到 (3)。然后,你可以通过合取引入 (KI) 推导出 (2),最后像以前一样通过条件消去 (CE) 从 (1) 和 (2) 中推导出 (3)。一些推导系统有一个规则,通常称为重言式蕴涵,允许你推导出先前行中的任何重言式结论。然而,这应该被视为一种(诚然有用)的缩写。在后面的页面中,我们将实现这种缩写的限制版本。
通常情况下,通过使用消去规则来分解前提、其他假设(将在后面的页面中介绍)——然后继续分解结果,这样做是很有用的。假设这就是为什么我们对 (1) 和 (2) 应用 CE,那么推导出
- (7)

以及
- (8)

通过对 (3) 应用双条件消去 (BE)。为了进一步分解它,你可能尝试推导出
或
,这样你就可以对 (7) 或 (8) 应用 CE。
如果你知道你想要推导哪一行,你可以通过使用引入规则来构建它。这是从 (5) 和 (6) 中推导出 (2) 的策略。
我们的推导包含两种类型的元素。
- 行号。这允许在后面引用该行。
- 公式。推导的目的是推导出公式,这是在该行推导出的公式。
- 注释。它指定了将公式输入推导中的理由。
- 行号和公式之间的垂直线。这些用于设置我们将在下一模块中介绍的子推导。
- 将前提和临时假设与其他行隔开的水平线。当我们进入谓词逻辑时,使用前提和临时假设会有限制。以一种易于识别的格式设置它们有助于遵守这些限制。
我们通常非正式地谈论公式,就好像它是整行一样,但该行还包括行号和注释。
前提的标注是“前提”。 我们要求推导中使用到的所有前提都出现在第一行。 不允许任何非前提行出现在前提之前。 理论上,一个论证可以有无穷多个前提。 但是,推导只有有限多行,所以推导中只能使用有限多个前提。 我们不要求所有前提都出现在其他行之前。 对于有无穷多个前提的论证来说,这是不可能的。 但我们确实要求推导中出现的所有前提都出现在任何其他行之前。
要求推导中使用到的前提出现在其第一行,比绝对必要的要求更严格。 然而,当我们进入谓词逻辑时,某些限制将变得必要,这使得这个要求至少是一个有用的约定。
我们在上一模块中介绍了除两条推理规则之外的所有推理规则,并在下一模块中介绍另外两条推理规则。
这个推导系统没有任何公理。
我们将为以下论证构造一个推导
∴ 
首先,我们将前提输入到推导中
|
1.
|
|
|
|
前提 |
2.
|
|
|
|
前提 |
3.
|
|
|
|
前提 |
|
注意行号和公式之间的竖线。 这是控制子推导的围栏的一部分。 我们将在下一模块中介绍子推导。 在此之前,我们只在推导的长度上画一条竖线。 还要注意前提下面的横线。 这是帮助区分前提与推导中其他行的围栏。
现在我们需要使用前提。 将 KE 应用于第一个前提两次,我们将添加以下几行
|
4.
|
|
|
|
1 KE |
5.
|
|
|
|
1 KE |
|
现在我们需要通过应用 CE 使用第二个前提。 由于 CE 有两个前件行,因此我们首先需要推导出所需的另一行。 因此,我们将添加以下几行
|
6.
|
|
|
|
4 DI |
7.
|
|
|
|
2, 6 CE |
|
现在我们将通过应用 CE 使用第三个前提。 同样,我们首先需要推导出所需的另一行。 新的行是
|
8.
|
|
|
|
5, 7 KI |
9.
|
|
|
|
3, 8 CE |
|
第 9 行是
, 这是我们论证的结论,所以我们完成了。 结论并不总是如此顺利地出现在我们面前,但这次它确实出现了。 完整的推导如下
|
1.
|
|
|
|
前提 |
2.
|
|
|
|
前提 |
3.
|
|
|
|
前提 |
4.
|
|
|
|
1 KE |
5.
|
|
|
|
1 KE |
6.
|
|
|
|
4 DI |
7.
|
|
|
|
2, 6 CE |
8.
|
|
|
|
5, 7 KI |
9.
|
|
|
|
3, 8 CE |
|
如前所述,我们还需要三个推理规则:条件引入 (CI)、否定引入 (NI) 和否定消除 (NE)。这些需要子推导。
我们从一个示例推导开始,它说明了条件引入,然后进行解释。对于以下论证的推导:
∴ 
如下所示
|
1.
|
|
|
|
前提 |
|
|
|
|
|
2.
|
|
|
|
|
假设 |
3.
|
|
|
|
|
1 KE |
|
|
|
|
|
4.
|
|
|
|
2–3 CI |
|
第 2 行和第 3 行构成了一个子推导。它从假设所期望公式的前件开始,并以推导出所期望公式的后件结束。在行号和公式之间有两个垂直的栅栏,以将其与推导的其余部分隔开,并指示其从属状态。第 2 行在其下方有一个水平的栅栏,以将假设与子推导的其余部分隔开。第 4 行是条件引入的应用。它不是从一两行推断出来的,而是从整个子推导(第 2-3 行)推断出来的。
条件引入是一个 *放电规则*。它放电(使无效)该假设,并且实际上使整个子推导无效。一旦我们应用了放电规则,子推导中的任何行(此处为第 2 行和第 3 行)都不能在推导中进一步使用。
为了推导出一个公式
,条件引入 (CI) 规则通过首先在子推导中假设前件
为真,然后推导出
作为子推导的结论来应用。符号上,CI 写成


此处,后续行不是从一个或多个先行行推断出来的,而是从整个子推导推断出来的。注释是子推导所占行范围和缩写 CI。与之前介绍的推理规则不同,条件引入不能用真值表来证明。相反,它是由 *命题连接词的性质* 中介绍的演绎原理证明的。为什么我们假设
为了推导出
的直觉是,如果
为假,则根据定义
为真。因此,如果我们表明无论何时
碰巧为真,
为真,那么
一定为真。
请注意,先行子推导可以包含一行,该行同时充当假设的
和推导出的
,如下推导所示:
- ∴

|
1.
|
|
|
|
|
假设 |
|
|
|
|
|
2.
|
|
|
|
1 CI |
|
为了说明否定引入,我们将提供一个针对以下论证的推导:
∴ 
|
1.
|
|
|
|
前提 |
2.
|
|
|
|
前提 |
|
|
|
|
|
3.
|
|
|
|
|
假设 |
4.
|
|
|
|
|
2 KE |
5.
|
|
|
|
|
3, 4 CE |
6.
|
|
|
|
|
2 KE |
|
|
|
|
|
7.
|
|
|
|
3–6 NI |
8.
|
|
|
|
1, 7 CE |
9.
|
|
|
|
8 DI |
|
第 3 到第 6 行构成了一个子推导。它从假设所需公式的相反开始,并以假设矛盾(一个公式及其否定)结束。和以前一样,行号和公式之间有两个垂直分隔符,将它与推导的其余部分隔开,并表明其从属状态。第 3 行下的水平分隔符再次将假设与子推导的其余部分隔开。第 7 行,它继整个子推导之后,是否定引入的应用。
在第 9 行,请注意注释“5 DI”将是不正确的。尽管从
推断出
是有效的,当我们到达第 9 行时,第 5 行不再处于活动状态。因此,我们不允许从第 5 行推导出任何东西。
否定引入 (NI)


结果行是从整个子推导中推断出来的。注释是子推导所占行的范围,缩写是 NI。否定引入有时被称为拉丁语名称Reductio ad Absurdum,有时被称为反证法。
与条件引入一样,否定引入不能通过真值表来证明。而是通过在命题联结词性质中介绍的归谬原则来证明。
为了说明否定消去,我们将提供一个针对以下论证的推导:
∴ 
|
1.
|
|
|
|
前提 |
|
|
|
|
|
2.
|
|
|
|
|
假设 |
3.
|
|
|
|
|
2 DI |
4.
|
|
|
|
|
1 KE |
|
|
|
|
|
5.
|
|
|
|
2–4 NE |
|
第 2 行到第 4 行构成了一个子推导。与前面的例子一样,它从假设所需的公式的反面开始,并以假设矛盾(一个公式及其否定)结束。第 5 行紧随整个子推导而来,是使用否定消除规则的结果。
否定消去 (NE)


结论行由整个子推导推断得出。注释是子推导占用的行范围,缩写是 NE。与否定引入一样,否定消除有时被称为拉丁语名称“归谬法”,有时被称为“反证法”。
与否定引入一样,否定消除也由在 句子联结词的性质 中介绍的归谬原理所证明。该规则在引入/消除命名约定中的位置比其他规则稍显笨拙。与其他消除规则不同,此规则消除的否定并不出现在已推导出的行中。相反,被消除的否定出现在子推导的假设中。
在本模块中介绍的推理规则,条件引入和否定引入,是放电规则。为了避免使用更复杂的术语,我们可以将 推理规则 中介绍的推理规则称为“标准规则”。标准规则是一个推理规则,其前件是一组行。放电规则是一个推理规则,其前件是一个子推导。
推导中一行深度是指该行编号与公式之间所站立的篱笆数量。推导中所有行至少具有一个深度。每个临时假设使深度增加一个。每个放电规则使深度减少一个。
有效行是可以作为标准推理规则的前件行使用的行。特别是,它是一行,其深度小于或等于当前行的深度。无效行是指不是有效行的行。
据说放电规则放电假设。它使其前件子推导中的所有行无效。
子推导可以嵌套。例如,我们提供了一个针对以下论证的推导:
∴ 
我们从前提开始,然后假设结论的前件。
注意:每次我们开始一个新的子推导并进入一个临时假设时,都会有一个特定的公式,我们希望在结束推导和消除假设时推导出它。为了使事情更容易理解,我们将把这个公式添加到假设的注释中。该公式不会正式成为注释的一部分,也不会影响推导的正确性。相反,它将作为我们自己的非正式提醒,说明我们要去哪里。
|
1.
|
|
|
|
前提 |
2.
|
|
|
|
前提 |
3.
|
|
|
|
前提 |
|
|
|
|
|
4.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aa44596d60b688c05bbdbe0bc7247ed056fb546a) |
|
这开始了一个子推导,以推导出论证的结论。现在我们将尝试一个析取消去(DE)以推导出它的后件

这将需要显示两个条件句,我们需要它们作为 DE 的前件行,即

以及

我们从第一个条件句开始。
|
5.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b1bf4e357c16d14c5edd2c38d2d82c0bcf02ac) |
|
|
|
|
|
|
|
6.
|
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8b390160716315f88a8ad089d9a9d61428354ee) |
|
这个子推导很容易完成。
|
7.
|
|
|
|
|
|
|
5, 6 KI |
8.
|
|
|
|
|
|
|
1, 7 CE |
9.
|
|
|
|
|
|
|
2 KE |
|
现在我们准备消除第 5 行和第 6 行的两个假设。
|
10.
|
|
|
|
|
|
6–9 NI |
|
|
|
|
|
|
11.
|
|
|
|
|
5–10 CI |
|
现在是为我们的 DE 计划(回到第 4 行)所需的第二个条件句。我们开始。
|
12.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e985539e01255392f5c1c6fe670de638714a63f8) |
|
|
|
|
|
|
|
13.
|
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8b390160716315f88a8ad089d9a9d61428354ee) |
14.
|
|
|
|
|
|
|
2 KE |
15.
|
|
|
|
|
|
|
3, 14 CE |
|
注意,在第 12 行和第 15 行之间存在矛盾。但第 12 行在错误的位置。我们需要它与第 15 行在同一个子推导中。以下第 16 行和第 17 行的一个愚蠢技巧将实现这一点。然后可以消除第 12 行和第 13 行的假设。
|
16.
|
|
|
|
|
|
|
12, 12 KI |
17.
|
|
|
|
|
|
|
16 KE |
|
|
|
|
|
|
|
18.
|
|
|
|
|
|
13–17 NI |
|
|
|
|
|
|
19.
|
|
|
|
|
12–18 CI |
|
最后,根据第 4 行、第 11 行和第 19 行,我们可以进行我们从第 4 行开始就一直在期待的 DE 操作。
|
20.
|
|
|
|
|
4, 11, 19 DE |
|
现在,通过撤销第 4 行的假设来完成推导。
|
21.
|
|
|
|
4–20 CI |
|
以下是完成的推导。
|
1.
|
|
|
|
前提 |
2.
|
|
|
|
前提 |
3.
|
|
|
|
前提 |
|
|
|
|
|
4.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aa44596d60b688c05bbdbe0bc7247ed056fb546a) |
|
|
|
|
|
|
5.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b1bf4e357c16d14c5edd2c38d2d82c0bcf02ac) |
|
|
|
|
|
|
|
6.
|
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8b390160716315f88a8ad089d9a9d61428354ee) |
7.
|
|
|
|
|
|
|
5, 6 KI |
8.
|
|
|
|
|
|
|
1, 7 CE |
9.
|
|
|
|
|
|
|
2 KE |
|
|
|
|
|
|
|
10.
|
|
|
|
|
|
6–9 NI |
|
|
|
|
|
|
11.
|
|
|
|
|
5–10 CI |
|
|
|
|
|
|
12.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e985539e01255392f5c1c6fe670de638714a63f8) |
|
|
|
|
|
|
|
13.
|
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8b390160716315f88a8ad089d9a9d61428354ee) |
14.
|
|
|
|
|
|
|
2 KE |
15.
|
|
|
|
|
|
|
3, 14 CE |
16.
|
|
|
|
|
|
|
12, 12 KI |
17.
|
|
|
|
|
|
|
16 KE |
|
|
|
|
|
|
|
18.
|
|
|
|
|
|
13–17 NI |
|
|
|
|
|
|
19.
|
|
|
|
|
12–18 CI |
20.
|
|
|
|
|
4, 11, 19 DE |
|
|
|
|
|
21.
|
|
|
|
4–20 CI |
|
一个定理是指一个公式,它已经提供了一个零前提推导。我们将保持一个已经证明的定理的编号列表。在接下来的推导中,我们将继续我们的非正式约定,将公式添加到假设的注释中,特别是我们希望通过新开始的子推导来推导的公式。
您可能还记得在构造一个复杂推导中,我们不得不使用一个愚蠢的技巧将公式复制到适当的子推导中(第 16 行和第 17 行)。我们可以证明一个定理,它将帮助我们避免这种令人讨厌的行为。

|
1.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/79933dc3c8b22ad47c5f28386ff6e8976b768d5e) |
|
|
|
|
|
2.
|
|
|
|
1 CI |
|
推导可以通过允许输入一条公式作为先前证明定理的替换实例来进行缩写。注释将是 'Tn',其中 n 是定理的编号。虽然我们不会正式要求,但我们也会在注释中显示替换(如果有)(见下面的推导中的第 3 行)。下一个定理的证明将使用T1。

|
1.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b8be83a1ab88d731a8b904852f116034ad2939) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97cf4af3c1bca8188faa85c99bb829c88690a523) |
3.
|
|
|
|
|
|
T1 [P/Q] |
4.
|
|
|
|
|
|
1, 3 CE |
|
|
|
|
|
|
5.
|
|
|
|
|
2–4 CI |
|
|
|
|
|
6.
|
|
|
|
1–5 CI |
|
我们需要证明在推导中以这种方式使用定理是合理的。为此,我们将展示如何生成T2的正确、非缩写推导,即不引用我们在其缩写证明中使用的定理的推导。
观察到,当我们在 T2 的推导中引入第 3 行时,我们将
代入 T1 中的
。假设您要在 T1 的证明中对每一行应用相同的替换。然后您将得到以下同样正确的推导。
|
1.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c3c0af0222220bbc7f981fe3c5a3d969cb2fd7a9) |
|
|
|
|
|
2.
|
|
|
|
1 CI |
|
现在假设您要将 T2 的证明中的第 3 行替换为这个推导。您需要调整行号,以便每行号只有一行。您还需要调整注释,以便它们引用的行号仍然正确。但是,经过这些调整后,您将得到以下 T2 的正确未缩写推导。
|
1.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b8be83a1ab88d731a8b904852f116034ad2939) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97cf4af3c1bca8188faa85c99bb829c88690a523) |
|
|
|
|
|
|
|
3.
|
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c3c0af0222220bbc7f981fe3c5a3d969cb2fd7a9) |
|
|
|
|
|
|
|
4.
|
|
|
|
|
|
3 CI |
5.
|
|
|
|
|
|
1, 4 CE |
|
|
|
|
|
|
6.
|
|
|
|
|
2–5 CI |
|
|
|
|
|
7.
|
|
|
|
1–6 CI |
|
因此,我们看到,将先前证明的定理引入推导中,仅仅是将该定理的证明包含到推导中的缩写。上面关于展开推导的说明可以更一般化和更严格,但我们将其保留在这个非正式的状态。有了生成正确展开推导的说明,就可以将先前证明的定理引入推导中。
在接下来的两个模块中将介绍其他定理。
本页介绍了推导推理规则的概念,并提供了一些此类规则。
现在我们可以将缩写进一步推行。推导推理规则是指不是作为推导系统的一部分给我们的推理规则,而是使用先前证明的定理的缩写。特别是,假设我们已经证明了一个特定的定理。在这个定理中,将每个句子字母统一替换为不同的希腊字母。假设结果具有以下形式。
.
[评论:在我看来,这和接下来的内容可能会让学生感到困惑。前面几节中避免元理论的意图在这里造成了一些问题,因为需要了解演绎定理才能使它更有意义。]
然后我们可以引入一个具有以下形式的推导推理规则





推导规则的应用可以通过用以下方法替换来消除
- 先前证明的定理,
- 重复使用合取引入(KI)来构建定理的前件,以及
- 使用条件消去(CE)来获得定理的后件。
然后可以像上面描述的那样消除先前证明的定理。这将留下一个展开推导。
当然,从推导中删除缩写并不理想,因为它会使推导更加复杂,更难阅读,但推导可以被展开的事实证明了缩写是合理的,所以我们首先可以使用缩写。
我们的第一个推导推理规则将基于 T1,它是

将句子字母替换为希腊字母,我们得到

现在我们生成推导的推理规则
- 重复 (R)


现在我们可以展示这个规则如何简化我们对 **T2** 的证明。
|
1.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b8be83a1ab88d731a8b904852f116034ad2939) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97cf4af3c1bca8188faa85c99bb829c88690a523) |
3.
|
|
|
|
|
|
1 R |
|
|
|
|
|
|
4.
|
|
|
|
|
2–3 CI |
|
|
|
|
|
5.
|
|
|
|
1–4 CI |
|
虽然这仅仅比我们对 **T2** 的原始证明少一行,但它不那么令人讨厌。我们可以使用推理规则而不是愚蠢的技巧。因此,推导更容易阅读和理解(更不用说更容易产生)。
接下来的两个定理——以及基于它们的推导规则——利用了双重否定公式和未否定公式之间的等价性。

|
1.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \lnot \lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5a010f77ae19f9aea6fabf12869899e6216e77bc) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d56c2499de3ac67a73cdcaca427dce5605b4320b) |
3.
|
|
|
|
|
|
1 R |
|
|
|
|
|
|
4.
|
|
|
|
|
2–3 NI |
|
|
|
|
|
5.
|
|
|
|
1–4 CI |
|
**T3** 证明了以下规则。
- 双重否定引入 (DNI)



|
1.
|
|
|
|
|
假设 ![{\displaystyle [\lnot \lnot \mathrm {P} \rightarrow \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d1bb69f44806a433fd72926eb47f9b4ffa7a043c) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/81936377579d3940eeb3983f919467358a9f12aa) |
3.
|
|
|
|
|
|
1 R |
|
|
|
|
|
|
4.
|
|
|
|
|
2–3 NE |
|
|
|
|
|
5.
|
|
|
|
1–4 CI |
|
T4 证明了以下规则。
- 双重否定消除 (DNE)



|
1.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/218e914cb2dfec118a310f2d3b6de200ee6e08d2) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b99e6e42dce9a0938a5354e1018054a02fca2ad3) |
3.
|
|
|
|
|
|
1 S |
4.
|
|
|
|
|
|
1 S |
|
|
|
|
|
|
5.
|
|
|
|
|
2–4 NE |
|
|
|
|
|
7.
|
|
|
|
1–5 CI |
|
我们的下一个规则基于 T5。
- 矛盾 (矛盾)



当您推导出矛盾,但想要使用的推导规则不是 NI 或 NE 时,此规则偶尔会有用。这可以避免完全微不足道的子推导。矛盾规则将用于下一条定理的证明。

|
1.
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {P} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de406ff15ac87549e0b995a4fa7d7e4dc2b2fea1) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97cf4af3c1bca8188faa85c99bb829c88690a523) |
3.
|
|
|
|
|
|
1, 2 矛盾 |
|
|
|
|
|
|
4.
|
|
|
|
|
2–3 CI |
|
|
|
|
|
5.
|
|
|
|
1–4 CI |
|
基于T2和T6,我们介绍以下推导规则。
- 条件加法,形式 I (CAdd)


- 条件加法,形式 II (CAdd)


“条件加法”这个名称并不常用。它是基于对析取引入的传统名称,即“加法”。这条规则不提供引入条件的通用方法。这是因为您需要的先行项行并不总是可推导的。然而,当先行项行恰好很容易获得时,应用这条规则比为条件引入产生子推导更简单。

|
1.
|
|
|
|
|
假设 ![{\displaystyle [(\mathrm {P} \rightarrow \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/822876910ec839e4e6294e59bb10a63c5aa3d174) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ebecf005a1793b292d92ddec0a677c0612909c89) |
3.
|
|
|
|
|
|
1 KE |
4.
|
|
|
|
|
|
2, 3 CE |
5.
|
|
|
|
|
|
1 KE |
|
|
|
|
|
|
6.
|
|
|
|
|
2–5 NI |
|
|
|
|
|
7.
|
|
|
|
1–6 CI |
|
现在我们用T7来证明以下规则。
- 拒取式 (MT)



拒取式有时也被称为“否定后件”。请注意,以下不是拒取式的实例,至少根据上面的定义。



拒取式的前提行是一个条件和其后件的否定。该推理的前提行是一个条件和其后件的相反,但不是其后件的否定。这里需要的推理需要像下面那样推导。
|
1.
|
|
|
|
前提 |
2.
|
|
|
|
前提 |
3.
|
|
|
|
2 DNI |
4.
|
|
|
|
1, 3 CE |
5.
|
|
|
|
4 DNE |
|
当然,可以将它作为一个定理来证明

然后你可以在这个定理的基础上添加一个新的推理规则——或者更可能的是,一个新的 Modus Tollens 形式。但是,我们在这里不会这样做。
到目前为止给出的派生规则对于消除推导中经常使用的一些令人讨厌的部分非常有用。它们将有助于使您的推导更容易生成,也更易读。但是,因为它们确实是派生规则,所以它们不是严格要求的,而是理论上可以省略的。
一些其他的定理和派生规则可以有效地添加。我们在这里列出一些有用的定理,但将它们的证明以及它们相关联的派生推理规则的定义留给读者。如果你构造了许多推导,你可能想维护你自己的个人列表,你会发现它很有用。








在目前的推理规则下,推导中的析取很难处理。使用已经推导出的析取并应用析取消除 (DE) 并不太糟糕,但有一个更易于使用的替代方案。首先推导出析取更困难。我们的析取引入 (DI) 规则被证明是完成这项任务的相当贫乏的工具。在本模块中,我们引入了派生规则,这些规则提供了处理推导中析取的替代方法。
我们从一个新的(将要)推导的推理规则开始。这将为析取消除 (DE) 提供一个有用的替代方案。
- 拒取式假言推理,形式 I (MTP)



- 拒取式假言推理,形式 II (MTP)



拒取式假言推理有时被称为析取三段论,偶尔也称为“狗的规则”。
这个新规则需要以下两个支持定理。

|
1.
|
|
|
|
|
假设 ![{\displaystyle [(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ce2fd880e79bd95061a9001884c5f98b39d25c94) |
2.
|
|
|
|
|
1 KE |
3.
|
|
|
|
|
1 KE |
4.
|
|
|
|
|
3 CAdd |
5.
|
|
|
|
|
T1 [P/Q] |
6.
|
|
|
|
|
2, 4, 5 DE |
|
|
|
|
|
7.
|
|
|
|
1–6 CI |
|

|
1.
|
|
|
|
|
假设 ![{\displaystyle [(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/017310eff4f2d7cae3bd6dd40e51e5acc578175e) |
2.
|
|
|
|
|
1 KE |
3.
|
|
|
|
|
1 KE |
4.
|
|
|
|
|
3 CAdd |
5.
|
|
|
|
|
T1 |
6.
|
|
|
|
|
2, 4, 5 DE |
|
|
|
|
|
7.
|
|
|
|
1–6 CI |
|
举个使用 MTP 的例子,我们重新做一下来自 构造复杂推导 的推导示例。
∴ 
|
1.
|
|
|
|
前提 |
2.
|
|
|
|
前提 |
3.
|
|
|
|
前提 |
|
|
|
|
|
4.
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aa44596d60b688c05bbdbe0bc7247ed056fb546a) |
|
|
|
|
|
|
5.
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8b390160716315f88a8ad089d9a9d61428354ee) |
6.
|
|
|
|
|
|
2 KE |
7.
|
|
|
|
|
|
3, 6 CE |
8.
|
|
|
|
|
|
4, 7 MTP |
9.
|
|
|
|
|
|
5, 8 KI |
10.
|
|
|
|
|
|
1, 9 CE |
11.
|
|
|
|
|
|
2 KE |
|
|
|
|
|
|
12.
|
|
|
|
|
5–11 NI |
|
|
|
|
|
13.
|
|
|
|
4–12 CI |
|
在第 4 行之后,我们没有费心为推导出 DE 所需的前件行创建子推导。相反,我们直接转到结论的后件的子推导。在第 8 行,我们应用了 MTP。
下一个推导规则显著减少了推导出析取的工作量,从而为析取引入 (DI) 提供了一个有用的替代方案。
- 条件析取 (CDJ)



|
1.
|
|
|
|
|
假设 ![{\displaystyle [(\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d274e3f04d76311583944ef8236ff241af80cfab) |
|
|
|
|
|
|
2.
|
|
|
|
|
|
假设 ![{\displaystyle [\mathrm {P} \lor \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d908c75773c25f4ce62e273bd9b6b7abe190692f) |
|
|
|
|
|
|
|
3.
|
|
|
|
|
|
|
假设 ![{\displaystyle [\lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ebecf005a1793b292d92ddec0a677c0612909c89) |
|
|
|
|
|
|
|
|
4.
|
|
|
|
|
|
|
3 DI |
5.
|
|
|
|
|
|
|
2 R |
|
|
|
|
|
|
|
6.
|
|
|
|
|
|
3–5 NI |
7.
|
|
|
|
|
|
1, 6 CE |
8.
|
|
|
|
|
|
7 DI |
|
|
|
|
|
|
9.
|
|
|
|
|
2–8 NI |
|
|
|
|
|
10.
|
|
|
|
1–9 CI |
|
这个推导将使用 **T12**(在Derived Inference Rules中介绍),尽管其证明被留给读者作为练习。以下推导的正确性,特别是第二行,假设您已经证明了 **T12**。
- ∴

|
1.
|
|
|
|
|
假设 ![{\displaystyle [\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4f17aa6df957ee3265b637942af874d9ab1c05c8) |
2.
|
|
|
|
|
T12 |
3.
|
|
|
|
|
1, 2 CE |
4.
|
|
|
|
|
3 KE |
5.
|
|
|
|
|
4 CAdd |
|
|
|
|
|
7.
|
|
|
|
1–6 CI |
8.
|
|
|
|
7 CDJ |
|
在这里,我们试图通过首先推导出 CDJ 所需的前项来推导出所需的条件。