Coq에서 논리는 어떻게 인코딩됩니까?

Question

Isabelle은 일종의 논리적 프레임 워크 입니다. 메타 이론을 사용하여 논리의 공리와 규칙을 소개하고 이에 대한 추론을 할 수 있습니다. 예를 들어 Isabelle 분포의 IFOL.thy에서 직관적 인 1 차 논리의 인코딩을 볼 수 있습니다. 다음은 수량 자 상수의 선언입니다.

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을 어떻게 인코딩합니까?

Answer 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.