在 Coq 中定义谓词而不指定其真值条件答案

【问题标题】：Defining a predicate without specifying its truth condition in Coq在 Coq 中定义谓词而不指定其真值条件
【发布时间】：2014-10-25 22:21:03
【问题描述】：

我正在尝试将 Coq 用于一些简单的哲学谓词逻辑。例如，假设我想在 Coq 中表达“如果一个存在是人类，它就不是完美的”。我首先必须定义“存在”、“人类”和“完美”这些术语是什么。看起来，自然的方法是将第一个定义为一种类型，而将其他定义为该类型的一元谓词。

Inductive being : Type :=
| b : nat -> being. 

Inductive human : being -> Prop :=
| h : forall ( b : being ), human b.

Inductive perfect : being -> Prop :=
| p : forall ( b : being ), perfect b.

（being 用数字索引，以确保有多个不同的存在。）

有了这个定义，语句可以表示为

Lemma humans_are_imperfect : 
forall ( b : being ), human b -> ~ perfect b.
Admitted.

这种方法的问题在于它允许证明无意义，例如

Lemma humans_are_perfect : 
forall ( b : being ), human b -> perfect b.
intros b H. apply ( p b ). Qed.

很明显，human 和perfect 的定义存在问题，因为它乱七八糟地取任何being 并断言其人性和完美。所需要的是对 human 和 perfect 的定义，该定义仅指定它们的类型，而对于它们适用于哪些 beings 保持模棱两可。

如果将perfect 的真值条件内置到其定义中，则可以完全避免此问题，例如构造函数仅将非人类 beings 作为参数。但是，在哲学论证中，像这样预先提供所有信息并不总是可行的。很多时候，您必须将某种类型或谓词作为给定的，然后通过进一步的前提慢慢构建其细节。

我有一种感觉，我正在尝试做的事情不太适合 Coq 的归纳基础。也许我最好学习一门像 Prolog 这样的逻辑编程语言，但希望我错了。

【问题讨论】：

标签： predicate coq

【解决方案1】：

你想要做的事情可以在 Coq 中完美地表达，只需要使用高阶谓词逻辑，而不需要归纳定义。您可以通过假设存在类型being、谓词human 和perfect 以及与这些相关的推理规则来处理您的定理。

Section SomePhilosophy.

Variable being : Type.
Variable human perfect : being -> Prop.

Hypothesis human_not_perfect : forall b, human b -> ~ perfect b.

(* ... some theorems about the above notions ... *)

End SomePhilosophy.

关闭该部分后，您的所有定义都将根据满足您假设的being、human 和perfect 的选择变为参数化。在您最初的方法中，您通过预先确定being 是来限制您的理论，因为您给出了它的定义。在这里，being 可以做任何事情。

【讨论】：