如何解决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.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。