Come vengono codificate le logiche in Coq?

Question

Isabelle è una sorta di quadro logico . Puoi introdurre gli assiomi e le regole di una logica e ragionare su di essi usando la meta-teoria. Ad esempio, puoi vedere la codifica della logica intuizionistica del primo ordine in IFOL.thy della distribuzione Isabelle. Ecco la dichiarazione delle costanti del quantificatore:

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›

Questa procedura si adatta sicuramente alla logica di ordine superiore. Puoi anche vedere che le regole sono codificate nella meta-teoria che ha i simboli ⟹ e ⋀.

Tuttavia, in Coq non penso che tu abbia un quadro logico (?).

Come si codifica IFOL in Coq?

Answer 1

Non conosco Isabelle quindi potrei perdere alcune sottigliezze sul significato di axiomatization, ma ecco un'approssimazione approssimativa:

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.