Coq中的逻辑如何编码？

问题描述

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？

解决方法

我不认识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.