Coq 中的逻辑是如何编码的？答案

【问题标题】：How are logics encoded in Coq?Coq 中的逻辑是如何编码的？
【发布时间】：2020-08-24 10:19:56
【问题描述】：

Isabelle 是一种逻辑框架。您可以使用元理论介绍逻辑的公理和规则并对其进行推理。例如，您可以在 Isabelle 分布的 IFOL.thy 中看到直觉一阶逻辑的编码。下面是量词常量的声明：

typedecl o

judgment
  Trueprop :: ‹o ⇒ prop›  (‹(_)› 5)

axiomatization
  All :: ‹('a ⇒ o) ⇒ o›  (binder ‹∀› 10) and
  Ex :: ‹('a ⇒ o) ⇒ o›  (binder ‹∃› 10)
where
  allI: ‹(⋀x. P(x)) ⟹ (∀x. P(x))› and
  spec: ‹(∀x. P(x)) ⟹ P(x)› and
  exI: ‹P(x) ⟹ (∃x. P(x))› and
  exE: ‹⟦∃x. P(x); ⋀x. P(x) ⟹ R⟧ ⟹ R›

这个过程当然适合高阶逻辑。您还可以看到规则被编码在具有符号⟹和⋀的元理论中。

但是，在 Coq 中，我认为您没有逻辑框架 (?)。

如何在 Coq 中编码 IFOL？

【问题讨论】：

标签： coq

【解决方案1】：

我不认识 Isabelle，所以我可能会遗漏一些关于 axiomatization 含义的微妙之处，但这里有一个粗略的近似：

Parameter o : Type.

Parameter TrueProp : o -> Prop.

Implicit Types A : Type.

Notation "[ P ]" := (TrueProp P) : o_scope.
Local Open Scope o_scope.

Parameter All : forall {A}, (A -> o) -> o.
Parameter Ex  : forall {A}, (A -> o) -> o.

Parameter allI : forall {A} P, (forall x : A, [ P x ]) -> [ All P ].
Parameter spec : forall {A} P (x : A), [ All P ] -> [ P x ].
Parameter exI : forall {A} P (x : A), [ P x ] -> [ Ex P ].
Parameter exE : forall {A} (P : A -> o) (R : Prop), ([ Ex P ] /\ (forall x : A, [ P x ] -> R)) -> R.

【讨论】：