为啥 Coq 中的逻辑连接词和布尔值是分开的？

Posted 2023-05-08

【中文标题】为啥 Coq 中的逻辑连接词和布尔值是分开的？

【英文标题】：Why are logical connectives and booleans separate in Coq?为什么 Coq 中的逻辑连接词和布尔值是分开的？

【发布时间】：2015-10-11 19:35:18

【问题描述】：

我来自 javascript/Ruby 编程背景，并且习惯于 true/false 的工作原理（在 JS 中）：

!true
// false
!false
// true

然后您可以将这些真/假值与&& 类似

var a = true, b = false;
a && !b;

所以 and 和 not（以及其他逻辑/布尔运算符）是单个系统的一部分；看起来“逻辑”系统和“布尔”系统是一回事。

然而，在 Coq 中，逻辑和布尔值是两个不同的东西。为什么是这样？下面的引用/链接演示了如何需要一个定理来关联它们。

我们已经看到在 Coq 的计算（Type）和逻辑（Prop）世界中可以找到类似结构的几个地方。这里还有一个：布尔运算符 andb 和 orb 显然是逻辑连接词 ∧ 和 ∨ 的类似物。这个类比可以通过以下定理变得更加精确，这些定理展示了如何将关于 andb 和 orb 在某些输入上的行为的知识转化为关于这些输入的命题事实。

Theorem andb_prop : ∀b c,
  andb b c = true → b = true ∧ c = true.

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211

【问题讨论】：

简短回答：并非您在 Coq 中可以陈述的所有内容都是可证明的（例如，以停止问题为例。您能证明它（真）还是反驳它（假），还是需要“灰色”这个状态？）。这只是解释的一小部分，但它应该能让你开始思考:)

【参考方案1】：

本质上，Coq 两者都有，因为它们对不同的事物有用：布尔对应于可以机械检查的事实（即，使用算法），而命题可以表达更多的概念。

严格来说，逻辑世界和布尔世界在 Coq 中并不是分开的：布尔世界是逻辑世界的一个子集。换句话说，可以将每个可以表述为布尔计算的语句都可以看作是一个逻辑命题（即Prop 类型的东西）：如果b : bool 表示一个语句，我们可以通过说b = true，其类型为Prop。

在 Coq 中逻辑不仅仅是布尔值的原因是前面的语句的逆不成立：并非所有逻辑事实都可以被视为布尔计算。换句话说，普通编程语言（如 Ruby 和 JavaScript）中的布尔值不会同时包含 Coq 中的 bool 和 Prop，因为 Props 可以表达这些语言中的布尔值不能表达的东西。

为了说明这一点，请考虑以下 Coq 谓词：

Definition commutative T (op : T -> T -> T) : Prop :=
  forall x y, op x y = op y x.

顾名思义，这个谓词断言运算符op 是可交换的。编程语言中的许多运算符都是可交换的：例如，对整数进行乘法和加法运算。事实上，在 Coq 中，我们可以证明以下陈述（我相信这些是 Software Foundations 书中的示例）：

Lemma plus_comm : commutative plus. Proof. (* ... *) Qed.
Lemma mult_comm : commutative mult. Proof. (* ... *) Qed.

现在，试着想想如何用更传统的语言翻译像commutative 这样的谓词。如果这看起来很困难，那并非偶然：有可能证明我们不能用这些语言编写一个返回布尔值的程序来测试一个操作是否可交换。你当然可以编写单元测试来检查这个事实对于特定的输入是否正确，例如：

2 + 3 == 3 + 2
4 * 5 == 5 * 4

但是，如果您的操作员使用无限数量的输入，这些单元测试只能涵盖所有可能情况的一小部分。因此，测试总是比完整的形式证明要弱。

如果Props 可以表达布尔值所能表达的一切，你可能想知道为什么我们还要在 Coq 中使用布尔值。原因是 Coq 是一个 建设性逻辑，这正是 Vinz 在他的评论中所暗示的。这个事实最广为人知的后果是，在 Coq 中我们无法证明以下直观原则：

Definition excluded_middle :=
  forall P : Prop, P \/ ~ P.

本质上说每个命题要么是真要么是假。 “这怎么可能失败？”，你可能会问自己。粗略地说，在构造逻辑（尤其是 Coq）中，每个证明都对应于我们可以执行的算法。特别是，当您在构造逻辑中证明A \/ B 形式的陈述时，您可以从该证明中提取（始终终止）算法来回答A 或B 是否成立。因此，如果我们能够证明上述原理，我们将有一个算法，给定某个命题，告诉我们该命题是否有效。然而，可计算性理论表明，由于不可判定性，这通常是不可能的：如果我们将P 表示“程序p 在输入x 时停止”，则排除中间将产生halting problem 的判定器, 不存在。

现在，Coq 中布尔值的有趣之处在于，通过构造它们允许使用排中，因为它们确实对应于我们可以运行的算法。具体来说，我们可以证明：

Lemma excluded_middle_bool :
  forall b : bool, b = true \/ negb b = true.
Proof. intros b; destruct b; simpl; auto. Qed.

因此，在 Coq 中，将布尔值视为命题的特殊情况是有用的，因为它们允许进行其他命题所不具备的推理形式，即案例分析。

当然，你可以认为要求每个证明都对应一个算法是愚蠢的，事实上大多数逻辑都允许排中原理。默认情况下遵循此方法的证明助手示例包括 Isabelle/HOL 和 Mizar 系统。在这些系统中，我们不必区分布尔值和命题，它们被视为同一事物。例如，伊莎贝尔只有bool，没有Prop。 Coq 还允许您通过假设允许您对一般命题执行案例分析的公理来模糊布尔值和命题之间的区别。另一方面，在这样的设置中，当你编写一个返回布尔值的函数时，你可能无法获得可以作为算法执行的东西，而在 Coq 中默认情况下总是如此。

【讨论】：

有意思，谢谢你的详细分析。我会花一些时间来理解。您介意添加要记住的关键点的摘要吗？它们似乎是“并非所有逻辑事实都可以视为布尔计算”，“在 Coq 中，不能证明命题的排中，但可以证明布尔值”，“在构造逻辑（和 Coq）中，每个证明都对应于我们的算法可以执行，但您不能为命题的排中创建算法”（为什么？不确定我是否完全理解）

跟进问题：mathoverflow.net/questions/212121/…

我试图添加一些关于文本中最后一点的更多细节（我看到你删除了 MathOverflow 上的问题？）。我还在开头添加了一个（非常简短的）摘要。

哎呀，把它移到这里：math.stackexchange.com/questions/1370805/…