Minimalist formalization of first-order signatures, logic, theories and models. As an example, we formalize a small fragment of ZF set theory.

ZF.v

(*
   A formalization of first-order logic, theories and their models.
   As an example we formalize the language of ZF set theory and a a small fragment of ZF.
*)

(* A signature is given by function symbols, relation symbols, and their arities. *)
Structure Signature :=
  { funSym : Type (* names of function symbols *)
  ; funArity : funSym -> Type (* arities of function symbols *)
  ; relSym : Type (* names of relation symbols *)
  ; relArity : relSym -> Type (* arities of relation symbols *)
  }.

Arguments funArity {_} _.
Arguments relArity {_} _.

(* A context is just a type whose elements are the variables. *)
Definition Context := Type.

Inductive EmptyContext := .

(* Extension of a context by a fresh variable. The constructors are named S and Z
   for "successor" and "zero", because we use them later on to construct deBruijn indices. *)
Inductive Extend (Γ : Context) : Context :=
  | Z : Extend Γ
  | S : Γ -> Extend Γ
.

Arguments S {_} _.
Arguments Z {_}.

(* Terms in a context, where a context is simply a type whose elements are variables. *)
Inductive term (Σ : Signature) (Γ : Context) : Type :=
  | var : Γ -> term Σ Γ
  | tm : forall (f : funSym Σ), (funArity f -> term Σ Γ) -> term Σ Γ
.

Arguments var {_} {_} _.
Arguments tm {_} {_} _ _.

(* First-order formulas over a given signature and context. *)
Inductive formula (Σ : Signature) (Γ : Context) : Type :=
  | rel : forall (R: relSym Σ), (relArity R -> term Σ Γ) -> formula Σ Γ
  | equal : term Σ Γ -> term Σ Γ -> formula Σ Γ
  | true : formula Σ Γ
  | conj : formula Σ Γ -> formula Σ Γ -> formula Σ Γ
  | disj : formula Σ Γ -> formula Σ Γ -> formula Σ Γ
  | impl : formula Σ Γ -> formula Σ Γ -> formula Σ Γ
  | not : formula Σ Γ -> formula Σ Γ
  | all : formula Σ (Extend Γ) -> formula Σ Γ
  | some : formula Σ (Extend Γ) -> formula Σ Γ
.

Arguments rel {_} {_} _ _.
Arguments equal {_} {_} _ _.
Arguments true {_} {_}.
Arguments conj {_} {_} _ _.
Arguments disj {_} {_} _ _.
Arguments impl {_} {_} _ _.
Arguments not {_} {_} _.
Arguments all {_} {_} _.
Arguments some {_} {_} _.

Definition iff {Σ : Signature} {Γ : Context} (p q : formula Σ Γ) :=
  conj (impl p q) (impl q p).

Definition closedFormula Σ := formula Σ EmptyContext.

(* An interpretation of a signature Σ is given by a carrier
   and interpretations of the function and relation symbols of Σ. *)
Structure Interpretation (Σ : Signature) : Type :=
  { carrier :> Type
  ; interpRel : forall (R : relSym Σ), (relArity R -> carrier) -> Prop
  ; interpFun : forall (f : funSym Σ), (funArity f -> carrier) -> carrier
  }.

Arguments interpRel {_} {_} _ _.
Arguments interpFun {_} {_} _ _.

(* A valuation is a map from variables to the carrier of an interpretation. *)
Definition valuation {Σ} {I : Interpretation Σ} (Γ : Context) := Γ -> I.

Definition emptyValuation {Σ} {I : Interpretation Σ}: @valuation Σ I EmptyContext :=
  fun x => match x with end.

(* Extend a valuation η by one more value. *)
Definition extend {Σ} {I : Interpretation Σ} {Γ : Context} (η : valuation Γ) (v : I) (x : Extend Γ) : I :=
  match x with
  | S y => η y
  | Z => v
  end.

(* Extend an interpretation to terms. *)
Fixpoint interpTerm {Σ} {I : Interpretation Σ} {Γ : Context} (η : valuation Γ) (t : term Σ Γ) : I :=
  match t with
  | var x => η x
  | tm f ts => interpFun f (fun i => interpTerm η (ts i))
  end.

(* Extend an interpretation to formulas. *)
Fixpoint interpFormula {Σ} (I : Interpretation Σ) {Γ : Context} (η : valuation Γ) (F : formula Σ Γ) : Prop :=
  match F with
  | rel R ts => interpRel R (fun i => interpTerm η (ts i))
  | equal t u => interpTerm η t = interpTerm η u
  | true => True
  | conj F₁ F₂ => interpFormula I η F₁ /\ interpFormula I η F₂
  | disj F₁ F₂ => interpFormula I η F₁ \/ interpFormula I η F₂
  | impl F₁ F₂ => interpFormula I η F₁ -> interpFormula I η F₂
  | not F => ~ (interpFormula I η F)
  | all F => forall (v : I), interpFormula I (extend η v) F
  | some F => exists (v : I), interpFormula I (extend η v) F
  end.

(* A first-order theory over a signature Σ is given by a type of axiom names, and axiom statements. *)
Structure Theory (Σ : Signature) :=
  { axiom_name :> Type (* names of axioms *)
  ; axiom : axiom_name -> closedFormula Σ (* axiom statements *)
  }.

Arguments axiom {_} {_}.

(* A model is given by an interpretation and validation of the axioms. *)
Structure Model {Σ : Signature} (T : Theory Σ) :=
  { theoryInterp : Interpretation Σ
  ; theoryValid : forall (ax : T), interpFormula theoryInterp emptyValuation (axiom ax)
  }.

Section ZF.
  (* Example:
     ZF is a small "proto" fragment of ZF whose axioms are just the empty set and union.
     Note that the model given here does not validate extensionality. We would have to
     extend interpretations so that they interpret equality as equivalence relation if
     we wanted to validate extensionality (because Coq does not have quotients).
  *)

  (* Binary arity *)
  Inductive binary := arg1 | arg2.

  (* There is one relation symbol, called "elementOf" *)
  Inductive ZF_relSymbol := elementOf.

  (* The ZF signature. *)
  Definition ZFΣ : Signature :=
    {| funSym := Empty_set
    ;  funArity := fun x => match x with end
    ;  relSym := ZF_relSymbol
    ;  relArity := fun elementOf => binary
    |}.

  Definition ZF_term (Γ : Context) := term ZFΣ Γ.
  Definition ZF_formula := formula ZFΣ.
  Definition ZF_closedFormula := closedFormula ZFΣ.

  (* Short-hand for writing down "u is element of v" *)
  Definition elem {Γ : Context} (u v : ZF_term Γ) :=
    @rel ZFΣ Γ elementOf (fun i => match i with arg1 => u | arg2 => v end).

  (* The axioms names. *)
  Inductive ZF_axiom_name :=
  | ZF_empty
  | ZF_union
  .

  (* Axiom statements. *)
  Definition ZF_axiom (ax : ZF_axiom_name) : ZF_closedFormula :=
    match ax with

    | ZF_empty =>
        (* ∃ sz ∀ z, ¬ (z ∈ sz) *)
        some (all (not (elem (var Z) (var (S Z)))))

    | ZF_union =>
        (* ∀ x ∃ y . ∀ z . (z ∈ y) ⇔ (∃ w . w ∈ x ∧ y ∈ w) *)
        all (some (all (
          iff
            (elem (var Z) (var (S Z)))
            (some (conj
                    (elem (var Z) (var (S (S (S Z)))))
                    (elem (var (S Z)) (var Z))
                  ))
        )))
    end.

  Definition ZF_Theory : Theory ZFΣ :=
    {| axiom_name := ZF_axiom_name
     ; axiom := ZF_axiom
    |}.

  (* We next construct a model V of ZF_Theory. *)

  Inductive ZFSet : Type :=
  | zf : forall (A : Type), (A -> ZFSet) -> ZFSet.

  (* The underlying index type of a ZF-set *)
  Definition index (x : ZFSet) : Type :=
    match x with
    | zf A _ => A
    end.

  (* The element of a ZF-set at a given index. *)
  Definition el (x : ZFSet) (i : index x) : ZFSet.
  Proof.
    destruct x as [I f].
    exact (f i).
  Defined.

  (* The interpretation of ∈. *)
  Definition ZFelem (u : binary -> ZFSet) : Prop :=
    match u arg2 with
    | zf _ s => exists i, u arg1 = s i
    end.

  (* The interpretation of ZFΣ in ZFSet. *)
  Definition ZFI : Interpretation ZFΣ :=
    {| carrier := ZFSet
     ; interpRel := fun (r : relSym ZFΣ) => match r with elementOf => ZFelem end
     ; interpFun := fun f => match f with end
    |}.

  Definition ZFempty : ZFSet :=
    zf Empty_set (fun x => match x with end).

  Definition ZFunion (x : ZFSet) : ZFSet.
  Proof.
    destruct x as [I x].
    apply (zf {i : I & index (x i)}).
    intros [i j].
    exact (el (x i) j).
  Defined.

  (* Auxliary lemma, it should exist in the standard library. *)
  Definition convert {A B : Type} (e : A = B) (x : A) : B :=
    match e in (_ = T) return T with
    | eq_refl => x
    end.

  (* Finally, we define the model. *)
  Definition V : Model ZF_Theory.
  Proof.
    exists ZFI.
    intros [|].
    - (* empty set axiom *)
      exists ZFempty.
      intros x [[] ?].
    - (* union *)
      intros [I x].
      exists (ZFunion (zf I x)).
      intros [J y].
      split.
      + intros [[i j] eq].
        exists (x i).
        split.
        * now exists i.
        * destruct (x i).
          now exists j.
      + intros [[K z] [[i H] [k G]]].
        pose (k' := convert (f_equal index H) k).
        exists (existT (fun (i : I) => index (x i)) i k').
        destruct H as [].
        now transitivity (z k).
  Defined.
End ZF.