Coqでロジックはどのようにエンコードされますか?

Aug 24 2020

しずえは一種の論理的枠組みです。メタ理論を使用して、論理の公理と規則、およびそれらについての理由を紹介できます。たとえば、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をどのようにエンコードしますか?

回答

2 Li-yaoXia Aug 25 2020 at 01:41

私はイザベルを知らないので、の意味についていくつかの微妙な点を見逃している可能性があります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.