如何为 Coq 中的蕴涵建模引入规则？

Question

我正在学习自然推论和练习 Coq。

我们考虑一个公式：

Inductive P :=
| ...
| And: P -> P -> P
| Imp: P -> P -> P. (* implication *)

现在我添加一堆可证明性的推理规则：

Inductive Deriv: P -> Prop :=
| ...
| intro_and: forall p q, Deriv p -> Deriv q -> Deriv (And p q)
| elim_and1: forall p q, Deriv (And p q) -> Deriv p
| elim_and2: forall p q, Deriv (And p q) -> Deriv q
| ...

但我坚持使用暗示的引入规则。我试过这个：

| intro_imp: forall p q, (Deriv p -> Deriv q) -> Deriv (Imp p q)

，这显然不行，因为归纳格出现在负数的位置。

蕴涵的引入规则为：

[p]
 .
 .
 q
-------
p ⊃ q

如何为 Coq 中的蕴涵引入规则建模？

Answer 1

直接在 Coq 中按原样表述自然演绎有点困难，因为最自然的表述会隐藏前提。因此，我们在引入蕴涵时不能参考我们正在放电的前提。

我认为最简单的解决方案是在判断中使假设显式，即Deriv的类型为list P -> P -> Prop。这个想法是 Deriv hs p 表示 p 在假设 hs 下是可证明的。这意味着放弃自然演绎的原始希尔伯特式公式，其中假设是隐含的（检查例如 the Wikipedia article）。停留在您提供的片段中，这可能会导致类似这样的结果（使用只有一个结论的序列）：

Inductive Deriv : list P -> P -> Prop := (* How to use a hypothesis *) | premise_intro hs p : In p hs -> Deriv hs p (* In most rules, we just maintain the list of hypotheses *) | and_intro hs p1 p2 : Deriv hs p1 -> Deriv hs p2 -> Deriv hs (And p1 p2) | and_elim1 hs p1 p2 : Deriv hs (And p1 p2) -> Deriv hs p1 | and_elim2 hs p1 p2 : Deriv hs (And p1 p2) -> Deriv hs p2 | imp_elim hs p1 p2 : Deriv hs (Imp p1 p2) -> Deriv hs p1 -> Deriv hs p2 (* When introducing an implication, we remove the hypothesis from our list *) | imp_intro hs p1 p2 : Deriv (p1 :: hs) p2 -> Deriv hs (Imp p1 p2).

如何为 Coq 中的蕴涵建模引入规则？

How to model introduction rule for implication in Coq?

logic

coq

first-order-logic