(*this program compiles with COQ 8.9*)

(*
2021/08/06

Author: Foys
If you want to contact me the address is foYER.a41v;
put all letters in the string above lower case and replace the letter v in
the string above by <<"arobase" gmx.fr>>
*)

Section Signatures_and_arities_of_formulas_and_terms.

  Record Signature :=
    make_sgn
      {
        Function_symbol: Type;
        Relation_symbol: Type;
        function_arity: Function_symbol -> nat;
        relation_arity: Relation_symbol -> nat
      }.

  Section definitions_of_terms_predicates_and_formulas.

    Variable Sg: Signature.

    Section terms_and_predicates.

      Variable Variable_letter:Type. (*we introduce this in order to deal with
                                    bound_variables more easily than if we had constants*)

      Inductive NFO_Term: nat -> Type :=
      |nfo_variable_to_term: Variable_letter -> NFO_Term 0
      |nfo_symbol_to_term: forall (x: Function_symbol Sg), NFO_Term (function_arity Sg x)
      |nfo_app_term: forall n:nat, NFO_Term (S n) -> NFO_Term 0 -> NFO_Term n.

      Inductive NFO_Predicate: nat -> Type :=
      |nfo_symbol_to_predicate: forall (x: Relation_symbol Sg),
          NFO_Predicate (relation_arity Sg x)
      |nfo_app_predicate: forall n:nat, NFO_Predicate (S n) -> NFO_Term 0 -> NFO_Predicate n.

    End terms_and_predicates.

    Inductive NFO_Formula: Type -> Type :=
    |nfof_atomic_formula: forall (context:Type) (x:NFO_Predicate context 0),
        NFO_Formula context
    |nfof_nand: forall context:Type, NFO_Formula context -> NFO_Formula context ->
                                     NFO_Formula context
    |nfof_forall: forall context:Type,
        NFO_Formula (option context) -> NFO_Formula context.

    (*Bound variables are dealt with the "locally nameless convention",which is a variant
      of De Bruijn indices, using the coq option operator. we start with a given context
      and the variables added to it can be viewed as numbers.*)

    Section definition_of_the_other_logical_connectors.

      Definition nfof_not (C:Type) (x:NFO_Formula C):NFO_Formula C:=
        nfof_nand C x x.

      Definition nfof_implies (C:Type) (x y:NFO_Formula C):NFO_Formula C:=
        nfof_nand C x (nfof_not C y).

      Definition nfof_and (C:Type) (x y:NFO_Formula C):NFO_Formula C:=
        nfof_not C (nfof_nand C x y).

      Definition nfof_or (C:Type) (x y:NFO_Formula C):NFO_Formula C:=
        nfof_nand C (nfof_not C x) (nfof_not C y).

      Definition nfof_equiv (C:Type) (x y:NFO_Formula C):NFO_Formula C:=
        nfof_and C (nfof_implies C x y) (nfof_implies C y x).

      Definition nfof_exists (C:Type) (f:NFO_Formula (option C)):NFO_Formula C:=
        nfof_not C (nfof_forall C (nfof_not (option C) f)).

    (*attempting to optimize these definitions is pointless; the very fact we use nand
       as a primary connector causes unfixable complexity issues and programs executed
       with the classes we define will probably make your computer crash. The purpose of
       first order logic as we define it is to explore its theoretical properties and
       prove mathematical theorems and in order to do this it is better to have the
       smallest number of items in inductive definitions, so that the proof is shorter.*)

    End definition_of_the_other_logical_connectors.

    Section definition_of_substitution_of_variables_in_terms_and_atomic_formulas.

      Variables C D:Type.
      Variable environment: C -> NFO_Term D 0.

      Fixpoint nfo_term_substitution (n:nat) (x:NFO_Term C n) {struct x}:NFO_Term D n :=
        match x in (NFO_Term _ n0) return (NFO_Term D n0) with
        | nfo_variable_to_term _ c => environment c
        | nfo_symbol_to_term _ x0 => nfo_symbol_to_term D x0
        | nfo_app_term _ n0 x1 x2 =>
          nfo_app_term D n0 (nfo_term_substitution (S n0) x1) (nfo_term_substitution 0 x2)
        end.

      Fixpoint nfo_predicate_substitution (n:nat) (x:NFO_Predicate C n) {struct x}:
        NFO_Predicate D n :=
        match x in (NFO_Predicate _ n0) return (NFO_Predicate D n0) with
        | nfo_symbol_to_predicate _ x0 => nfo_symbol_to_predicate D x0
        | nfo_app_predicate _ n0 x1 x2 =>
          nfo_app_predicate D n0 (nfo_predicate_substitution (S n0) x1)
                            (nfo_term_substitution 0 x2)
        end.

    End definition_of_substitution_of_variables_in_terms_and_atomic_formulas.

    Definition change_of_variable_in_terms (C D:Type) (ve: C -> D):=
      nfo_term_substitution C D (fun x:C => nfo_variable_to_term D (ve x)).

    Definition constant_nfo_term_embedding
               (C:Type):(forall n:nat, NFO_Term C n -> NFO_Term (option C) n):=
      change_of_variable_in_terms C (option C) (Some).

    Definition change_of_variable_in_predicates (C D:Type) (ve: C -> D):=
      nfo_predicate_substitution C D (fun x:C => nfo_variable_to_term D (ve x)).

    Definition constant_nfo_predicate_embedding
               (C:Type):(forall n:nat, NFO_Predicate C n -> NFO_Predicate (option C) n):=
      change_of_variable_in_predicates C (option C) (Some).

    Definition add_var_to_environment (C D:Type)(env: C -> NFO_Term D 0):
      option C -> NFO_Term (option D) 0:=
      option_rect (fun _:option C => NFO_Term (option D) 0)
                  (fun y:C => change_of_variable_in_terms D (option D) Some 0 (env y))
                  (nfo_variable_to_term (option D) (None)).

    Fixpoint nfo_formula_substitution
             (C D:Type)
             (environment: C -> NFO_Term D 0)
             (f: NFO_Formula C)
             {struct f}:NFO_Formula D:=
      match f in (NFO_Formula T) return ((T -> NFO_Term D 0) -> NFO_Formula D) with
      | nfof_atomic_formula context x =>
        fun environment0 : context -> NFO_Term D 0 =>
          nfof_atomic_formula D (nfo_predicate_substitution context D environment0 0 x)
      | nfof_nand context f1 f2 =>
        fun environment0 : context -> NFO_Term D 0 =>
          nfof_nand D (nfo_formula_substitution context D environment0 f1)
                    (nfo_formula_substitution context D environment0 f2)
      | nfof_forall context f0 =>
        fun environment0 : context -> NFO_Term D 0 =>
          nfof_forall D
                      (nfo_formula_substitution
                         (option context) (option D)
                         (add_var_to_environment context D environment0) f0)
      end environment.

    Definition change_of_variable_in_formulas (C D:Type) (ve: C -> D):=
      nfo_formula_substitution C D (fun x:C => nfo_variable_to_term D (ve x)).

    Definition constant_nfo_formula_embedding
               (C:Type):NFO_Formula C -> NFO_Formula (option C):=
      change_of_variable_in_formulas C (option C) (Some).

    Definition assign_term_to_var (C:Type)(t: NFO_Term C 0):
      option C -> NFO_Term C 0:=
      option_rect (fun _:option C => NFO_Term C 0)
                  (nfo_variable_to_term C)
                  t.

    Definition nfo_term_specialization (C:Type) (t: NFO_Term C 0):=
      nfo_term_substitution (option C) C (assign_term_to_var C t).

    Definition nfo_predicate_specialization (C:Type) (t: NFO_Term C 0):=
      nfo_predicate_substitution (option C) C (assign_term_to_var C t).

    Definition nfo_formula_specialization (C:Type) (t: NFO_Term C 0):=
      nfo_formula_substitution (option C) C (assign_term_to_var C t).

    Theorem nfo_term_substitution_transitivity:
      forall (C D E:Type)
             (env_cd: C -> NFO_Term D 0)
             (env_de: D -> NFO_Term E 0)
             (n:nat)
             (t: NFO_Term C n),
        nfo_term_substitution D E env_de n (nfo_term_substitution C D env_cd n t)=
        nfo_term_substitution
          C E
          (fun a:C => nfo_term_substitution D E env_de 0 (env_cd a))
          n t.
    Proof.
      induction t.
      simpl.
      reflexivity.
      simpl.
      reflexivity.
      simpl.
      rewrite IHt1.
      rewrite IHt2.
      reflexivity.
    Defined.

    Theorem nfo_term_extensional_equality:
      forall (C D:Type)
             (env1 env2: C -> NFO_Term D 0),
        (forall c:C, env1 c = env2 c) ->
        forall (n:nat) (t: NFO_Term C n),
          nfo_term_substitution C D env1 n t =
          nfo_term_substitution C D env2 n t.
    Proof.
      intros C D env1 env2 eqenv.
      induction t.
      simpl.
      apply eqenv.
      simpl.
      reflexivity.
      simpl.
      rewrite IHt1.
      rewrite IHt2.
      reflexivity.
    Defined.

    Theorem nfo_predicate_substitution_transitivity:
      forall (C D E:Type)
             (env_cd: C -> NFO_Term D 0)
             (env_de: D -> NFO_Term E 0)
             (n:nat)
             (p: NFO_Predicate C n),
        nfo_predicate_substitution D E env_de n (nfo_predicate_substitution C D env_cd n p)=
        nfo_predicate_substitution
          C E
          (fun a:C => nfo_term_substitution D E env_de 0 (env_cd a))
          n p.
    Proof.
      induction p.
      simpl.
      reflexivity.
      simpl.
      rewrite IHp.
      rewrite nfo_term_substitution_transitivity.
      reflexivity.
    Defined.

    Theorem nfo_predicate_extensional_equality:
      forall (C D:Type)
             (env1 env2: C -> NFO_Term D 0),
        (forall c:C, env1 c = env2 c) ->
        forall (n:nat) (p: NFO_Predicate C n),
          nfo_predicate_substitution C D env1 n p =
          nfo_predicate_substitution C D env2 n p.
    Proof.
      intros C D env1 env2 eqenv.
      induction p.
      simpl.
      reflexivity.
      simpl.
      rewrite IHp.
      rewrite nfo_term_extensional_equality with (env2 := env2).
      reflexivity.
      assumption.
    Defined.

    Theorem nfo_formula_extensional_equality:
      forall (C:Type) (f:NFO_Formula C)
             (D:Type) (env1 env2: C -> NFO_Term D 0) (eqenv: forall c:C, env1 c = env2 c),
        nfo_formula_substitution C D env1 f =
        nfo_formula_substitution C D env2 f.
    Proof.
      intros C.
      induction f.
      intros.
      simpl.
      apply f_equal.
      apply nfo_predicate_extensional_equality.
      assumption.
      intros.
      simpl.
      apply f_equal2.
      apply IHf1.
      assumption.
      apply IHf2.
      assumption.
      intros.
      simpl.
      apply f_equal.
      apply IHf.
      intros.
      destruct c.
      simpl.
      apply f_equal.
      apply eqenv.
      reflexivity.
    Defined.

    Theorem nfo_formula_substitution_transitivity:
      forall (C:Type)(f:NFO_Formula C) (D E:Type)
             (env_cd: C -> NFO_Term D 0)
             (env_de: D -> NFO_Term E 0),
        nfo_formula_substitution D E env_de (nfo_formula_substitution C D env_cd f)=
        nfo_formula_substitution
          C E
          (fun a:C => nfo_term_substitution D E env_de 0 (env_cd a))
          f.
    Proof.
      induction f.
      intros.
      simpl.
      apply f_equal.
      apply nfo_predicate_substitution_transitivity.
      intros.
      simpl.
      apply f_equal2.
      apply IHf1.
      apply IHf2.
      intros.
      simpl.
      apply f_equal.
      rewrite IHf.
      apply nfo_formula_extensional_equality.
      intros.
      destruct c.
      simpl.
      unfold change_of_variable_in_terms.
      rewrite nfo_term_substitution_transitivity.
      rewrite nfo_term_substitution_transitivity.
      reflexivity.
      simpl.
      reflexivity.
    Defined.

    Theorem nfo_term_identity_substitution:
      forall (C:Type)(n:nat)(t:NFO_Term C n),
        nfo_term_substitution C C (fun x:C => nfo_variable_to_term C x) n t = t.
    Proof.
      induction t.
      simpl.
      reflexivity.
      simpl.
      reflexivity.
      simpl.
      rewrite IHt1.
      rewrite IHt2.
      reflexivity.
    Defined.

    Theorem nfo_predicate_identity_substitution:
      forall (C:Type)(n:nat)(p:NFO_Predicate C n),
        nfo_predicate_substitution C C (fun x:C => nfo_variable_to_term C x) n p = p.
    Proof.
      induction p.
      simpl.
      reflexivity.
      simpl.
      rewrite IHp.
      rewrite nfo_term_identity_substitution.
      reflexivity.
    Defined.

    Theorem nfo_formula_identity_substitution:
      forall (C:Type)(f:NFO_Formula C),
        nfo_formula_substitution C C (fun x:C => nfo_variable_to_term C x) f = f.
    Proof.
      induction f.
      simpl.
      rewrite nfo_predicate_identity_substitution.
      reflexivity.
      simpl.
      rewrite IHf1.
      rewrite IHf2.
      reflexivity.
      simpl.
      rewrite nfo_formula_extensional_equality with
          (C:= option context)
          (env2 := fun (x:option context) =>
                     nfo_variable_to_term (option context) x).
      rewrite IHf.
      reflexivity.
      intros.
      destruct c.
      simpl.
      reflexivity.
      simpl.
      reflexivity.
    Defined.

    Section specialization_on_constant_terms.

      Variable C:Type.
      Variable X: NFO_Term C 0.

      Theorem specialization_doesnt_change_constant_terms:
        forall (n:nat) (t:NFO_Term C n),
          nfo_term_specialization C X n (constant_nfo_term_embedding C n t) = t.
      Proof.
        intros.
        apply eq_trans with
            (y:=nfo_term_substitution C C (fun u:C => nfo_variable_to_term C u) n t).
        unfold nfo_term_specialization.
        unfold constant_nfo_term_embedding.
        unfold change_of_variable_in_terms.
        rewrite nfo_term_substitution_transitivity.
        apply nfo_term_extensional_equality.
        intros.
        simpl.
        reflexivity.
        apply nfo_term_identity_substitution.
      Defined.

      Theorem specialization_doesnt_change_constant_predicates:
        forall (n:nat) (p:NFO_Predicate C n),
          nfo_predicate_specialization C X n (constant_nfo_predicate_embedding C n p) = p.
      Proof.
        intros.
        apply eq_trans with
            (y:=nfo_predicate_substitution C C (fun u:C => nfo_variable_to_term C u) n p).
        unfold nfo_predicate_specialization.
        unfold constant_nfo_predicate_embedding.
        unfold change_of_variable_in_predicates.
        rewrite nfo_predicate_substitution_transitivity.
        apply nfo_predicate_extensional_equality.
        intros.
        simpl.
        reflexivity.
        apply nfo_predicate_identity_substitution.
      Defined.

      Theorem specialization_doesnt_change_constant_formulas:
        forall (f:NFO_Formula C),
          nfo_formula_specialization C X (constant_nfo_formula_embedding C f) = f.
      Proof.
        intros.
        apply eq_trans with
            (y:=nfo_formula_substitution C C (fun u:C => nfo_variable_to_term C u) f).
        unfold nfo_formula_specialization.
        unfold constant_nfo_formula_embedding.
        unfold change_of_variable_in_formulas.
        rewrite nfo_formula_substitution_transitivity.
        apply nfo_formula_extensional_equality.
        intros.
        simpl.
        reflexivity.
        apply nfo_formula_identity_substitution.
      Defined.

    End specialization_on_constant_terms.

    Section double_substitution_lemmas.

      Variable C:Type.
      Variable X: NFO_Term C 0.
      Variable Y: NFO_Term (option C) 0.

      Definition first_var_assign
                 (a:option (option C)):NFO_Term (option C) 0:=
        match a with
        |None => nfo_variable_to_term (option C) (None)
        |Some b => match b with
                   |None => constant_nfo_term_embedding C 0 X
                   |Some c => nfo_variable_to_term (option C) (Some c)
                   end
        end.

      Lemma double_substitution_for_variables:
        forall (c:option (option C)),
          nfo_term_substitution (option C) C (assign_term_to_var C X) 0
                                (assign_term_to_var (option C) Y c) =
          nfo_term_substitution
            (option C) C
            (assign_term_to_var
               C
               (nfo_term_substitution (option C) C (assign_term_to_var C X) 0 Y)) 0
            (first_var_assign c).
      Proof.
        destruct c.
        destruct o.
        simpl.
        reflexivity.
        simpl.
        unfold constant_nfo_term_embedding.
        unfold change_of_variable_in_terms.
        rewrite nfo_term_substitution_transitivity.
        apply eq_trans with
            (y:= nfo_term_substitution C C (fun u:C => nfo_variable_to_term C u) 0 X).
        apply eq_sym.
        apply nfo_term_identity_substitution.
        apply nfo_term_extensional_equality.
        intros.
        simpl.
        reflexivity.
        reflexivity.
      Defined.

      Theorem double_substitution_for_terms:
        forall (n:nat) (t:NFO_Term (option (option C)) n),
          nfo_term_specialization
            C X n
            (nfo_term_specialization (option C) Y n t) =
          nfo_term_specialization
            C (nfo_term_specialization C X 0 Y) n
            (nfo_term_substitution
               (option (option C)) (option C) first_var_assign n t).
      Proof.
        intros.
        unfold nfo_term_specialization.
        rewrite nfo_term_substitution_transitivity.
        rewrite nfo_term_substitution_transitivity.
        apply nfo_term_extensional_equality.
        apply double_substitution_for_variables.
      Defined.

      Theorem double_substitution_for_predicates:
        forall (n:nat) (t:NFO_Predicate (option (option C)) n),
          nfo_predicate_specialization
            C X n
            (nfo_predicate_specialization (option C) Y n t) =
          nfo_predicate_specialization
            C (nfo_term_specialization C X 0 Y) n
            (nfo_predicate_substitution
               (option (option C)) (option C) first_var_assign n t).
      Proof.
        intros.
        unfold nfo_predicate_specialization.
        rewrite nfo_predicate_substitution_transitivity.
        rewrite nfo_predicate_substitution_transitivity.
        apply nfo_predicate_extensional_equality.
        apply double_substitution_for_variables.
      Defined.

      Theorem double_substitution_for_formulas:
        forall (t:NFO_Formula (option (option C))),
          nfo_formula_specialization
            C X
            (nfo_formula_specialization (option C) Y t) =
          nfo_formula_specialization
            C (nfo_term_specialization C X 0 Y)
            (nfo_formula_substitution
               (option (option C)) (option C) first_var_assign t).
      Proof.
        intros.
        unfold nfo_formula_specialization.
        rewrite nfo_formula_substitution_transitivity.
        rewrite nfo_formula_substitution_transitivity.
        apply nfo_formula_extensional_equality.
        apply double_substitution_for_variables.
      Defined.

    End double_substitution_lemmas.

    Section Proof_theory.

      Section adding_an_hypothesis_to_a_set_of_sentences.

        Variable context:Type.
        Variable T: (NFO_Formula context) -> Type.
        Variable h: NFO_Formula context.

        Inductive add_hypothesis:(NFO_Formula context) -> Type :=
        |new_hyp: add_hypothesis h
        |base_hyp: forall (f:NFO_Formula context),T f -> add_hypothesis f.

      End adding_an_hypothesis_to_a_set_of_sentences.

      Definition add_hyp_subtheory
                 (C:Type) (h:NFO_Formula C) (T U:NFO_Formula C -> Type)
                 (st: forall p:NFO_Formula C, T p -> U p) (f:NFO_Formula C)
                 (a: add_hypothesis C T h f): add_hypothesis C U h f:=
        match a in (add_hypothesis _ _ _ f0) return (add_hypothesis C U h f0) with
        | new_hyp _ _ _ => new_hyp C U h
        | base_hyp _ _ _ f0 t => base_hyp C U h f0 (st f0 t)
        end.

      Section morphisms_of_theories.

        Variable C D:Type.
        Variable environment: C -> NFO_Term D 0.
        Variable theory: NFO_Formula C -> Type.

        Inductive nfo_theory_substitution: NFO_Formula D -> Type:=
        |fots_intro: forall f:NFO_Formula C,
            theory f -> nfo_theory_substitution
                          (nfo_formula_substitution C D environment f).

      End morphisms_of_theories.

      Definition substitution_subtheory
                 (C D:Type) (env: C -> NFO_Term D 0) (T U:NFO_Formula C -> Type)
                 (st: forall p:NFO_Formula C, T p -> U p) (f:NFO_Formula D)
                 (a: nfo_theory_substitution C D env T f):
        nfo_theory_substitution C D env U f.
      Proof.
        intros.
        destruct a.
        apply fots_intro.
        apply st.
        assumption.
      Defined.

      Definition change_of_variable_in_theories (C D:Type) (ve: C -> D):=
        nfo_theory_substitution C D (fun x:C => nfo_variable_to_term D (ve x)).

      Definition constant_nfo_theory_embedding
                 (C:Type):(NFO_Formula C -> Type) -> (NFO_Formula (option C) -> Type):=
        change_of_variable_in_theories C (option C) (Some).

      Section characterization_of_the_constant_embedding_of_a_theory.

        Variable context:Type.
        Variable theory: NFO_Formula context -> Type.

        Inductive constant_nfo_theory_embedding_alternative:
          NFO_Formula (option context) -> Type:=
        |cfotea_intro: forall f:NFO_Formula context,
            theory f ->
            constant_nfo_theory_embedding_alternative
              (constant_nfo_formula_embedding context f).

        Theorem constant_nfo_theory_embedding_check:
          forall f:NFO_Formula (option context),
            prod (constant_nfo_theory_embedding
                    context theory f ->
                  constant_nfo_theory_embedding_alternative f)
                 (constant_nfo_theory_embedding_alternative f ->
                  constant_nfo_theory_embedding
                    context theory f).
        Proof.
          intros.
          split.
          intro.
          destruct X.
          apply cfotea_intro.
          assumption.
          intro.
          destruct X.
          unfold constant_nfo_theory_embedding.
          unfold change_of_variable_in_theories.
          apply fots_intro.
          assumption.
        Defined.

      End characterization_of_the_constant_embedding_of_a_theory.

      Section natural_deduction.

        Inductive nand_natural_deduction:
          forall (C:Type) (hyp: NFO_Formula C -> Type), NFO_Formula C -> Type:=
        |nnd_ax: forall (C:Type) (hyp: NFO_Formula C -> Type) (f:NFO_Formula C),
            hyp f -> nand_natural_deduction C hyp f
        |nnd_nand_intro:
           forall (C:Type) (hyp: NFO_Formula C -> Type) (a b p q:NFO_Formula C),
             nand_natural_deduction C (add_hypothesis C (add_hypothesis C hyp a) b) p ->
             nand_natural_deduction C (add_hypothesis C (add_hypothesis C hyp a) b) q ->
             nand_natural_deduction C (add_hypothesis C (add_hypothesis C hyp a) b)
                                    (nfof_nand C p q) ->
             nand_natural_deduction C hyp (nfof_nand C a b)
        |nnd_nand_elim: forall (C:Type) (hyp: NFO_Formula C -> Type) (x y z:NFO_Formula C),
            nand_natural_deduction C hyp (nfof_nand C x (nfof_nand C y z)) ->
            nand_natural_deduction C hyp x ->
            nand_natural_deduction C hyp z
        |nnd_forall_intro: forall (C:Type) (hyp: NFO_Formula C -> Type)
                                  (f:NFO_Formula (option C)),
            nand_natural_deduction
              (option C) (constant_nfo_theory_embedding C hyp) f ->
            nand_natural_deduction C hyp (nfof_forall C f)
        |nnd_forall_elim: forall (C:Type) (hyp: NFO_Formula C -> Type)
                                 (f:NFO_Formula (option C))
                                 (t:NFO_Term C 0),
            nand_natural_deduction
              C hyp (nfof_forall C f) ->
            nand_natural_deduction
              C hyp (nfo_formula_specialization C t f).

        Fixpoint nnd_general_weakening
                 (C:Type)
                 (T: NFO_Formula C -> Type)
                 (f:NFO_Formula C)
                 (U:NFO_Formula C -> Type)
                 (st: forall p:NFO_Formula C, T p -> U p)
                 (pr: nand_natural_deduction C T f)
                 {struct pr}:nand_natural_deduction C U f.
        Proof.
          destruct pr.
          apply nnd_ax.
          apply st; assumption.
          apply nnd_nand_intro with (p:=p) (q:=q).
          apply nnd_general_weakening with (T:= add_hypothesis C (add_hypothesis C hyp a) b).
          apply add_hyp_subtheory; apply add_hyp_subtheory; assumption.
          assumption.
          apply nnd_general_weakening with (T:= add_hypothesis C (add_hypothesis C hyp a) b).
          apply add_hyp_subtheory; apply add_hyp_subtheory; assumption.
          assumption.
          apply nnd_general_weakening with (T:= add_hypothesis C (add_hypothesis C hyp a) b).
          apply add_hyp_subtheory; apply add_hyp_subtheory; assumption.
          assumption.
          apply nnd_nand_elim with (x:=x) (y:=y).
          apply nnd_general_weakening with (T:= hyp); assumption.
          apply nnd_general_weakening with (T:= hyp); assumption.
          apply nnd_forall_intro.
          apply nnd_general_weakening with (T:= constant_nfo_theory_embedding C hyp).
          apply substitution_subtheory.
          assumption.
          assumption.
          apply nnd_forall_elim.
          apply nnd_general_weakening with (T:=hyp).
          assumption.
          assumption.
        Defined.

        Definition nnd_hypothesis_weakening
                   (C:Type)
                   (T: NFO_Formula C -> Type)
                   (h f:NFO_Formula C)
                   (pr: nand_natural_deduction C T f):
          (nand_natural_deduction C (add_hypothesis C T h) f):=
          nnd_general_weakening C T f (add_hypothesis C T h)
                                (base_hyp C T h) pr.

        Fixpoint nfo_nnd_substitution
                 (C:Type) (T: NFO_Formula C -> Type) (f:NFO_Formula C)
                 (pr: nand_natural_deduction C T f)
                 (D:Type) (env: C -> NFO_Term D 0) {struct pr}:
          nand_natural_deduction
            D (nfo_theory_substitution C D env T) (nfo_formula_substitution C D env f).
        Proof.
          destruct pr.
          apply nnd_ax.
          apply fots_intro.
          assumption.
          simpl.
          apply nnd_nand_intro with
              (p:=nfo_formula_substitution C D env p)
              (q:=nfo_formula_substitution C D env q).
          apply nnd_general_weakening with
              (T:= nfo_theory_substitution C D env
                                           (add_hypothesis C (add_hypothesis C hyp a) b)).
          intros.
          destruct X.
          destruct a0.
          apply new_hyp.
          apply base_hyp.
          destruct a0.
          apply new_hyp.
          apply base_hyp.
          apply fots_intro.
          assumption.
          apply nfo_nnd_substitution.
          assumption.
          apply nnd_general_weakening with
              (T:= nfo_theory_substitution C D env
                                           (add_hypothesis C (add_hypothesis C hyp a) b)).
          intros.
          destruct X.
          destruct a0.
          apply new_hyp.
          apply base_hyp.
          destruct a0.
          apply new_hyp.
          apply base_hyp.
          apply fots_intro.
          assumption.
          apply nfo_nnd_substitution.
          assumption.
          apply nnd_general_weakening with
              (T:= nfo_theory_substitution C D env
                                           (add_hypothesis C (add_hypothesis C hyp a) b)).
          intros.
          destruct X.
          destruct a0.
          apply new_hyp.
          apply base_hyp.
          destruct a0.
          apply new_hyp.
          apply base_hyp.
          apply fots_intro.
          assumption.
          apply nfo_nnd_substitution with (D:=D) (env:=env) in pr3.
          simpl in pr3.
          assumption.
          apply nnd_nand_elim with
              (x:= nfo_formula_substitution C D env x)
              (y:= nfo_formula_substitution C D env y).
          apply nfo_nnd_substitution with (D:=D) (env:=env) in pr1.
          assumption.
          apply nfo_nnd_substitution.
          assumption.
          apply nnd_forall_intro.
          apply nnd_general_weakening with
              (T:= nfo_theory_substitution
                     (option C)
                     (option D)
                     (add_var_to_environment C D env)
                     (constant_nfo_theory_embedding C hyp)).
          intros.
          unfold constant_nfo_theory_embedding.
          destruct X.
          unfold change_of_variable_in_theories.
          unfold constant_nfo_theory_embedding in c.
          unfold change_of_variable_in_theories in c.
          destruct c.
          simpl.
          rewrite nfo_formula_substitution_transitivity.
          rewrite nfo_formula_extensional_equality
            with (C:=C) (D:= option D)
                 (env2:= fun v:C =>
                           nfo_term_substitution
                             D (option D)
                             (fun t:D => nfo_variable_to_term (option D) (Some t))
                             0
                             (env v)
                 ).
          rewrite <- nfo_formula_substitution_transitivity.
          apply fots_intro.
          apply fots_intro.
          assumption.
          intros.
          simpl.
          unfold change_of_variable_in_terms.
          reflexivity.
          apply nfo_nnd_substitution.
          assumption.
          apply nfo_nnd_substitution with (D:=D) (env := env) in pr.
          simpl in pr.
          apply nnd_forall_elim with (t:= nfo_term_substitution C D env 0 t) in pr.
          unfold nfo_formula_specialization in pr.
          unfold nfo_formula_specialization.
          rewrite nfo_formula_substitution_transitivity.
          rewrite nfo_formula_extensional_equality with
              (env2 := fun (v: option C) =>
                         nfo_term_substitution
                           (option D) D
                           (assign_term_to_var D (nfo_term_substitution C D env 0 t))
                           0
                           (nfo_term_substitution (option C) (option D)
                                                  (add_var_to_environment C D env)
                                                  0
                                                  (nfo_variable_to_term (option C) v))
              ).
          rewrite nfo_formula_substitution_transitivity in pr.
          assumption.
          intros c.
          destruct c.
          simpl.
          unfold change_of_variable_in_terms.
          rewrite nfo_term_substitution_transitivity.
          simpl.
          rewrite nfo_term_identity_substitution.
          reflexivity.
          simpl.
          reflexivity.
        Defined.

        Section ND_proofs_of_some_usual_inference_rules.

          Section classical_inference_rules_for_propositional_connectors.

            Variable C:Type.
            Variable T: NFO_Formula C -> Type.

            Notation D:= (nfof_nand C).

            Notation "G |- F":= (nand_natural_deduction C G F) (at level 61).
            Notation P:= (NFO_Formula C).

            Ltac ni v w := apply nnd_nand_intro with (p:=v) (q:=w).
            Ltac ne p q:= apply nnd_nand_elim with (x:=p) (y:=q).
            Ltac ax := apply nnd_ax.
            Ltac nh := apply new_hyp.
            Ltac bh := apply base_hyp.
            Ltac wh := apply nnd_hypothesis_weakening.
            Ltac ap := assumption.

            Definition nnd_nand_symmetry:
              forall (U:P -> Type) (p q:P), U |- D p q -> U |- D q p.
            Proof.
              intros.
              ni p q.
              ax; nh.
              ax; bh; nh.
              wh; wh; ap.
            Defined.

            Ltac ns := apply nnd_nand_symmetry.

            Definition nnd_nand_elim_2:
              forall (U:P -> Type) (x y z:P), U |- D x (D y z) -> U |- x -> U |- y.
            Proof.
              intros.
              ne x z.
              ni x (D y z).
              wh; wh; ap.
              ns; ax; nh.
              wh; wh; ap.
              ap.
            Defined.

            Ltac ne2 m n:= apply nnd_nand_elim_2 with (x:=m) (z:=n).

            Definition nnd_explosion:
              forall (U:P -> Type)(x y z:P),
                (U |- x) ->
                (U |- y) ->
                (U |- D x y) ->
                (U |- z).
            Proof.
              intros.
              ne x z.
              ni x y.
              wh; wh; ap.
              wh; wh; ap.
              wh; wh; ap.
              ap.
            Defined.

            Ltac nex m n := apply nnd_explosion with (x:=m) (y:=n).

            Definition nnd_non_contradiction:
              forall (U:P -> Type)(x:P),
                U|- D x (D x x).
            Proof.
              intros.
              ni x x.
              ax; bh; nh.
              ax; bh; nh.
              ax; nh.
            Defined.

            Ltac nc := apply nnd_non_contradiction.

            Definition nnd_double_implies_intro:
              forall (U:P -> Type)(x y z:P),
                ((add_hypothesis C U x) |- y) ->
                ((add_hypothesis C U x) |- z) ->
                U |- D x (D y z).
            Proof.
              intros.
              ni y z.
              wh; ap.
              wh; ap.
              ax; nh.
            Defined.

            Ltac ndii := apply nnd_double_implies_intro.

            Definition nnd_nand_cases:
              forall (U:P -> Type)(x y z:P),
                ((add_hypothesis C (add_hypothesis C U x) y)|- z) ->
                ((add_hypothesis C U (D x y)) |- z) ->
                (U |- z).
            Proof.
              intros.
              ne (D (D z z) (D x y)) z.
              ns.
              ni x y.
              ne2 (D z z) y.
              ax; nh.
              ax; bh; nh.
              ne (D z z) x.
              ax; nh.
              ax; bh; nh.
              wh.
              ni z z.
              apply nnd_general_weakening with (T:= add_hypothesis C (add_hypothesis C U x) y).
              intros.
              destruct X1.
              nh.
              destruct a.
              bh; nh.
              bh; bh; bh; ap.
              ap.
              apply nnd_general_weakening with (T:= add_hypothesis C (add_hypothesis C U x) y).
              intros.
              destruct X1.
              nh.
              destruct a.
              bh; nh.
              bh; bh; bh; ap.
              ap.
              ax; bh; bh; nh.
              ns; ni z z.
              wh; ap.
              wh; ap.
              ax; nh.
            Defined.

            Definition nnd_implies_intro:
              forall (U:P -> Type)(x y:P),
                (add_hypothesis C U x) |- y -> U |- nfof_implies C x y.
            Proof.
              intros.
              ni y y.
              wh; ap.
              wh; ap.
              ax; nh.
            Defined.

            Definition nnd_implies_elim:
              forall (U:P -> Type)(x y:P),
                (U |- nfof_implies C x y) ->
                (U |- x) ->
                (U |- y).
            Proof.
              intros.
              ne x y.
              ap.
              ap.
            Defined.

            Definition nnd_and_intro:
              forall (U:P -> Type)(x y:P),
                (U |- x) ->
                (U |- y) ->
                (U |- nfof_and C x y).
            Proof.
              intros.
              ni x y.
              wh; wh; ap.
              wh; wh; ap.
              ax; nh.
            Defined.

            Definition nnd_and_elim_left:
              forall (U:P -> Type)(x y:P),
                U |- (nfof_and C x y) -> U |- x.
            Proof.
              intros.
              ne2 (D (D x y) (D x y)) y.
              ns; nc.
              ap.
            Defined.

            Definition nnd_and_elim_right:
              forall (U:P -> Type)(x y:P),
                U |- (nfof_and C x y) -> U |- y.
            Proof.
              intros.
              ne (D (D x y) (D x y)) x.
              ns; nc.
              ap.
            Defined.

            Definition nnd_not_intro:
              forall (U:P -> Type)(x y:P),
                ((add_hypothesis C U x) |- y) ->
                ((add_hypothesis C U x) |- nfof_not C y) ->
                (U |- nfof_not C x).
            Proof.
              intros.
              ni y y.
              wh; ap.
              wh; ap.
              wh; ap.
            Defined.

            Definition nnd_not_elim:
              forall (U:P -> Type)(x y:P),
                (U |- x) ->
                (U |- nfof_not C x) ->
                U |- y.
            Proof.
              intros.
              nex x x.
              ap.
              ap.
              ap.
            Defined.

            Definition nnd_reductio_ad_absurdum:
              forall (U:P -> Type)(x:P),
                U |- nfof_not C (nfof_not C x) -> U |- x.
            Proof.
              intros.
              ne (D (D x x) (D x x)) x.
              ns; nc.
              ap.
            Defined.

            Definition nnd_contraposition:
              forall (U:P -> Type) (x y:P),
                (U |- nfof_implies C x y) ->
                (U |- nfof_implies C (nfof_not C y) (nfof_not C x)).
            Proof.
              intros.
              ni x (D y y).
              apply nnd_reductio_ad_absurdum.
              ax; nh.
              ax; bh; nh.
              wh; wh; ap.
            Defined.

            Definition nnd_or_intro_left:
              forall (U:P -> Type)(x y:P),
                U |- x -> U |- nfof_or C x y.
            Proof.
              intros.
              ni x x.
              wh; wh; ap.
              wh; wh; ap.
              ax; bh; nh.
            Defined.

            Definition nnd_or_intro_right:
              forall (U:P -> Type)(x y:P),
                U |- y -> U |- nfof_or C x y.
            Proof.
              intros.
              ni y y.
              wh; wh; ap.
              wh; wh; ap.
              ax; nh.
            Defined.

            Definition nnd_or_elim:
              forall (U:P -> Type)(x y z:P),
                ((add_hypothesis C U x) |- z) ->
                ((add_hypothesis C U y) |- z) ->
                (U |- nfof_or C x y) ->
                (U |- z).
            Proof.
              intros.
              apply nnd_reductio_ad_absurdum.
              ni (D x x) (D y y).
              wh.
              apply nnd_implies_elim with (x:= nfof_not C z).
              apply nnd_contraposition.
              wh.
              apply nnd_implies_intro.
              ap.
              ax; nh.
              wh.
              apply nnd_implies_elim with (x:= nfof_not C z).
              apply nnd_contraposition.
              wh.
              apply nnd_implies_intro.
              ap.
              ax; nh.
              wh; wh; ap.
            Defined.

          End classical_inference_rules_for_propositional_connectors.

          Section classical_inference_rules_and_theorems_for_quantifiers.

            Variable C:Type.
            Variable T: NFO_Formula C -> Type.

            Notation D:= (nfof_nand C).

            Notation "G |- F":= (nand_natural_deduction C G F) (at level 61).
            Notation P:= (NFO_Formula C).

            Ltac ni v w := apply nnd_nand_intro with (p:=v) (q:=w).
            Ltac ne p q:= apply nnd_nand_elim with (x:=p) (y:=q).
            Ltac ax := apply nnd_ax.
            Ltac nh := apply new_hyp.
            Ltac bh := apply base_hyp.
            Ltac wh := apply nnd_hypothesis_weakening.
            Ltac ap := assumption.

            Definition nnd_exists_intro:
              forall (f: NFO_Formula (option C)) (t:NFO_Term C 0),
                (T |- (nfo_formula_specialization C t f)) ->
                (T |- nfof_exists C f).
            Proof.
              intros.
              apply nnd_not_intro with (y:= nfo_formula_specialization C t f).
              wh; ap.
              assert (nfof_not C (nfo_formula_specialization C t f) =
                      nfo_formula_specialization
                        C t
                        (nfof_not (option C) f))
                as E.
              unfold nfo_formula_specialization; simpl; reflexivity.
              rewrite E.
              apply nnd_forall_elim.
              ax; nh.
            Defined.


            Definition nnd_exists_elim:
              forall (f:NFO_Formula (option C))
                     (g:P),
                (T |- nfof_exists C f) ->
                (nand_natural_deduction
                   (option C)
                   (add_hypothesis (option C) (constant_nfo_theory_embedding C T) f)
                   (constant_nfo_formula_embedding C g)) ->
                (T |- g).
            Proof.
              intros.
              apply nnd_reductio_ad_absurdum.
              apply nnd_not_intro with (y:= nfof_forall C (nfof_not (option C) f)).
              apply nnd_forall_intro.
              apply nnd_implies_elim with
                  (x:= constant_nfo_formula_embedding C (nfof_not C g)).
              assert (constant_nfo_formula_embedding C (nfof_not C g) =
                      nfof_not (option C) (constant_nfo_formula_embedding C g)) as E.
              reflexivity.
              rewrite E.
              apply nnd_contraposition.
              apply nnd_implies_intro.
              apply nnd_general_weakening with
                  (T:= (add_hypothesis (option C) (constant_nfo_theory_embedding C T) f)).
              intros.
              destruct X1.
              nh.
              bh.
              destruct c.
              apply fots_intro.
              bh; ap.
              ap.
              ax.
              apply fots_intro.
              nh.
              wh; ap.
            Defined.


            Definition nnd_forall_elim_2:
              forall (U: NFO_Formula C -> Type) (f:NFO_Formula (option C)),
                U |- nfof_forall C f ->
                     nand_natural_deduction
                       (option C)
                       (constant_nfo_theory_embedding C U) f.
            Proof.
              intros.
              unfold constant_nfo_theory_embedding.
              unfold change_of_variable_in_theories.
              apply nfo_nnd_substitution
                with (env:= fun x:C => nfo_variable_to_term (option C) (Some x))
                in X.
              simpl in X.
              apply nnd_forall_elim
                with (t:= nfo_variable_to_term (option C) (None))
                in X.
              simpl in X.
              unfold nfo_formula_specialization in X.
              rewrite nfo_formula_substitution_transitivity in X.
              assert
                (nfo_formula_substitution
                   (option C) (option C)
                   (fun a : option C =>
                      nfo_term_substitution
                        (option (option C)) (option C)
                        (assign_term_to_var
                           (option C)
                           (nfo_variable_to_term (option C) (None))) 0
                        (add_var_to_environment
                           C (option C)
                           (fun x : C => nfo_variable_to_term
                                           (option C) (Some x)) a)) f
                 =
                 (nfo_formula_substitution
                    (option C) (option C)
                    (fun u:(option C) => nfo_variable_to_term (option C) u) f)
                ) as e.
              apply nfo_formula_extensional_equality.
              intros.
              destruct c.
              simpl.
              reflexivity.
              simpl.
              reflexivity.
              rewrite e in X.
              rewrite nfo_formula_identity_substitution in X.
              assumption.
            Defined.

            Notation "v --> w":= (nfof_implies C v w) (right associativity, at level 51).

            Definition nnd_universal_modus_ponens: forall f g:NFO_Formula (option C),
                T |-
                (nfof_forall C (nfof_implies (option C) f g)) --> (nfof_forall C f)
                                                           --> (nfof_forall C g).
            Proof.
              intros.
              apply nnd_implies_intro.
              apply nnd_implies_intro.
              apply nnd_forall_intro.
              apply nnd_implies_elim with (x:=f).
              apply nnd_forall_elim_2.
              ax; bh; nh.
              apply nnd_forall_elim_2.
              ax; nh.
            Defined.

            Definition nnd_constant_forall: forall f:NFO_Formula C,
                T |- (nfof_implies C f
                                (nfof_forall C (constant_nfo_formula_embedding C f))).
            Proof.
              intros.
              apply nnd_implies_intro.
              apply nnd_forall_intro.
              apply nnd_ax.
              apply fots_intro.
              nh.
            Defined.

            Definition nnd_specialization_formula:
              forall (f:NFO_Formula (option C)) (t:NFO_Term C 0),
                T |- nfof_implies C (nfof_forall C f) (nfo_formula_specialization C t f).
            Proof.
              intros.
              apply nnd_implies_intro.
              apply nnd_forall_elim.
              ax; nh.
            Defined.

            Section the_witness_property.

              Ltac mp r := apply nnd_implies_elim with (x:=r).
              Ltac ded := apply nnd_implies_intro.

              Variable s:NFO_Term C 0.
              Variable f:NFO_Formula (option C).
              Variable g:P.
              Definition nnd_or_permutation: forall (U:P -> Type) (a b:P),
                  U|- (a --> b) --> b ->
                      U|- (b --> a) --> a.
              Proof.
                intros.
                apply nnd_nand_cases with (x:=a) (y:= nfof_nand C b b).
                ded; ax; bh; bh; nh.
                ded; mp b.
                ax; nh.
                mp (a --> b).
                wh; wh; assumption.
                ax; bh; nh.
              Defined.

              Definition nnd_or_permutation_formula: forall a b:P,
                  T|- ((a --> b) --> b) --> (b --> a) --> a.
              Proof.
                intros.
                ded.
                apply nnd_or_permutation.
                ax; nh.
              Defined.

              Definition nnd_or_forall_intro: forall (f1:P) (g1: NFO_Formula (option C)),
                  nand_natural_deduction
                    (option C) (constant_nfo_theory_embedding C T)
                    (nfof_implies
                       (option C)
                       (nfof_implies (option C) (constant_nfo_formula_embedding C f1) g1)
                       g1)
                  ->
                  T |- (f1 --> (nfof_forall C g1)) --> (nfof_forall C g1).
              Proof.
                intros.
                ded.
                apply nnd_forall_intro.
                mp (nfof_implies (option C) (constant_nfo_formula_embedding C f1) g1).
                apply nnd_general_weakening with
                    (T:=(constant_nfo_theory_embedding C T)).
                intros.
                destruct X0.
                apply fots_intro.
                bh; assumption.
                assumption.
                ded.
                apply nnd_general_weakening with
                    (T:=(constant_nfo_theory_embedding
                           C (add_hypothesis
                                C (add_hypothesis C T (f1 --> (nfof_forall C g1))) f1))).
                intros.
                destruct X0.
                simpl.
                destruct a.
                nh.
                bh.
                apply fots_intro.
                assumption.
                apply nnd_forall_elim_2.
                mp f1.
                ax; bh; nh.
                ax; nh.
              Defined.

              Definition nnd_universal_witness:
                nand_natural_deduction
                  (option C)
                  (constant_nfo_theory_embedding C T)
                  (nfof_implies
                     (option C)
                     (nfof_implies
                        (option C)
                        f
                        (constant_nfo_formula_embedding C (nfof_forall C f))
                     )
                     (constant_nfo_formula_embedding C g)
                  ) -> T |- g.
              Proof.
                intros.
                mp ((nfof_forall C f) --> g).
                mp ((g --> (nfof_forall C f)) --> (nfof_forall C f)).
                apply nnd_or_permutation_formula.
                apply nnd_or_forall_intro.
                ded.
                apply nnd_nand_cases with
                    (x:=f)
                    (y:= nfof_not (option C)
                                  (constant_nfo_formula_embedding C (nfof_forall C f))).
                ax; bh; nh.
                mp (constant_nfo_formula_embedding C g).
                ax; bh; nh.
                mp (nfof_implies (option C) f
                              (constant_nfo_formula_embedding C (nfof_forall C f))).
                wh; wh; assumption.
                ax; nh.
                ded.
                rewrite <- specialization_doesnt_change_constant_formulas with (f:=g) (X:=s).
                apply nnd_forall_elim.
                apply nnd_forall_intro.
                mp (nfof_implies (option C) f
                              (constant_nfo_formula_embedding C (nfof_forall C f))).
                apply nnd_general_weakening with (T:= constant_nfo_theory_embedding C T).
                intros.
                destruct X0.
                apply fots_intro.
                bh; assumption.
                assumption.
                ded.
                wh.
                ax.
                apply fots_intro.
                nh.
              Defined.

            End the_witness_property.

          End classical_inference_rules_and_theorems_for_quantifiers.

        End ND_proofs_of_some_usual_inference_rules.

      End natural_deduction.


      Section basic_semantics.

        Variable Univ:Type.

        Fixpoint function_type_interpretation (n:nat) {struct n}:Type:=
          match n with
          |0 => Univ
          |S k => Univ -> (function_type_interpretation k)
          end.

        Fixpoint relation_type_interpretation (n:nat) {struct n}:Type:=
          match n with
          |0 => Prop
          |S k => Univ -> (relation_type_interpretation k)
          end.

        Variable (env_t: forall x: Function_symbol Sg,
                     function_type_interpretation (function_arity Sg x)).
        Variable (env_r: forall x: Relation_symbol Sg,
                     relation_type_interpretation (relation_arity Sg x)).

        Section interpretation_of_terms_and_predicates.

          Variable C:Type.
          Variable (env_c: C -> Univ).

          Fixpoint fo_term_interpretation
                   (n:nat)
                   (t: NFO_Term C n)
                   {struct t}: function_type_interpretation n:=
            match t in (NFO_Term _ n0) return (function_type_interpretation n0) with
            | nfo_variable_to_term _ c => env_c c
            | nfo_symbol_to_term _ x => env_t x
            | nfo_app_term _ n0 t1 t2 =>
              let t3 := fo_term_interpretation (S n0) t1 in
              let t4 := fo_term_interpretation 0 t2 in t3 t4
            end.

          Fixpoint fo_predicate_interpretation
                   (n:nat)
                   (p: NFO_Predicate C n)
                   {struct p}: relation_type_interpretation n:=
            match p in (NFO_Predicate _ n0) return (relation_type_interpretation n0) with
            | nfo_symbol_to_predicate _ x => env_r x
            | nfo_app_predicate _ n0 p0 n1 =>
              let p1 := fo_predicate_interpretation (S n0) p0 in
              let n2 := fo_term_interpretation 0 n1 in p1 n2
            end.

        End interpretation_of_terms_and_predicates.

        Fixpoint nfo_formula_interpretation
                 (C:Type) (env_c: C -> Univ) (f:NFO_Formula C)
                 {struct f}:Prop:=
          match f in (NFO_Formula T) return ((T -> Univ) -> Prop) with
          | nfof_atomic_formula context x =>
            fun env_c0 : context -> Univ =>
              let x0 := fo_predicate_interpretation context env_c0 0 x in x0
          | nfof_nand context f1 f2 =>
            fun env_c0 : context -> Univ =>
              let f3 := nfo_formula_interpretation context env_c0 f1 in
              let f4 := nfo_formula_interpretation context env_c0 f2 in f3 -> f4 -> False
          | nfof_forall context f0 =>
            fun env_c0 : context -> Univ =>
              all
                (fun u : Univ =>
                   nfo_formula_interpretation
                     (option context)
                     (option_rect (fun _ : option context => Univ) env_c0 u) f0)
          end env_c.

        Fixpoint fo_term_interpretation_extensionality
                 (C:Type)
                 (env_c1 env_c2: C -> Univ)
                 (ext: forall l:C, env_c1 l = env_c2 l)
                 (k:nat)
                 (t:NFO_Term C k)
                 {struct t}:
          fo_term_interpretation C env_c1 k t =
          fo_term_interpretation C env_c2 k t.
        Proof.
          destruct t.
          simpl; apply ext.
          simpl; reflexivity.
          simpl.
          rewrite fo_term_interpretation_extensionality with
              (env_c1:= env_c1)(env_c2:= env_c2).
          rewrite fo_term_interpretation_extensionality with
              (env_c1:= env_c1)(env_c2:= env_c2).
          reflexivity.
          assumption.
          assumption.
        Defined.

        Fixpoint fo_predicate_interpretation_extensionality
                 (C:Type)
                 (env_c1 env_c2: C -> Univ)
                 (ext: forall l:C, env_c1 l = env_c2 l)
                 (k:nat)
                 (p:NFO_Predicate C k)
                 {struct p}:
          fo_predicate_interpretation C env_c1 k p =
          fo_predicate_interpretation C env_c2 k p.
        Proof.
          destruct p.
          simpl; reflexivity.
          simpl.
          rewrite fo_predicate_interpretation_extensionality
            with (env_c1:= env_c1)(env_c2:= env_c2).
          rewrite fo_term_interpretation_extensionality with
              (env_c1:= env_c1)(env_c2:= env_c2).
          reflexivity.
          assumption.
          assumption.
        Defined.

        Lemma nand_equiv: forall A A' B B':Prop,
            (A <-> A') -> (B <-> B') -> ((A -> B -> False) <-> (A' -> B' -> False)).
        Proof.
          intros.
          tauto.
        Defined.

        Lemma all_equiv: forall (P Q: Univ -> Prop),
            (forall x:Univ, P x <-> Q x) ->
            ((all P) <-> (all Q)).
        Proof.
          intros.
          split.
          intros; intro.
          apply H; apply H0.
          intros; intro.
          apply H; apply H0.
        Defined.

        Fixpoint nfo_formula_interpretation_extensionality
                 (C:Type)
                 (env_c1 env_c2: C -> Univ)
                 (ext: forall l:C, env_c1 l = env_c2 l)
                 (f:NFO_Formula C)
                 {struct f}:
          nfo_formula_interpretation C env_c1 f <->
          nfo_formula_interpretation C env_c2 f.
        Proof.
          destruct f.
          simpl;
            rewrite fo_predicate_interpretation_extensionality with (env_c2:= env_c2).
          apply iff_refl.
          assumption.
          simpl; apply nand_equiv.
          apply nfo_formula_interpretation_extensionality.
          assumption.
          apply nfo_formula_interpretation_extensionality.
          assumption.
          simpl; apply all_equiv.
          intros.
          apply nfo_formula_interpretation_extensionality.
          intros.
          destruct l.
          simpl; apply ext.
          simpl; reflexivity.
        Defined.

        Fixpoint fo_term_interpretation_substitution
                 (C D:Type)
                 (env_cd: C -> NFO_Term D 0)
                 (env_d: D -> Univ)
                 (k:nat)
                 (t:NFO_Term C k)
                 {struct t}:
          fo_term_interpretation
            C
            (fun x:C => fo_term_interpretation D env_d 0 (env_cd x))
            k t
          = fo_term_interpretation
              D env_d k
              (nfo_term_substitution C D env_cd k t).
        Proof.
          destruct t.
          simpl; reflexivity.
          simpl; reflexivity.
          simpl.
          rewrite fo_term_interpretation_substitution.
          rewrite fo_term_interpretation_substitution.
          reflexivity.
        Defined.

        Fixpoint fo_predicate_interpretation_substitution
                 (C D:Type)
                 (env_cd: C -> NFO_Term D 0)
                 (env_d: D -> Univ)
                 (k:nat)
                 (p:NFO_Predicate C k)
                 {struct p}:
          fo_predicate_interpretation
            C
            (fun x:C => fo_term_interpretation D env_d 0 (env_cd x))
            k p
          = fo_predicate_interpretation
              D env_d k
              (nfo_predicate_substitution C D env_cd k p).
        Proof.
          destruct p.
          simpl; reflexivity.
          simpl.
          rewrite fo_term_interpretation_substitution.
          rewrite fo_predicate_interpretation_substitution.
          reflexivity.
        Defined.

        Fixpoint nfo_formula_interpretation_substitution
                 (C D:Type)
                 (env_cd: C -> NFO_Term D 0)
                 (env_d: D -> Univ)
                 (f:NFO_Formula C)
                 {struct f}:
          nfo_formula_interpretation
            C
            (fun x:C => fo_term_interpretation D env_d 0 (env_cd x))
            f
          <->
          nfo_formula_interpretation
            D env_d
            (nfo_formula_substitution C D env_cd f).
        Proof.
          destruct f.
          simpl; rewrite fo_predicate_interpretation_substitution; apply iff_refl.
          simpl.
          apply nand_equiv.
          apply nfo_formula_interpretation_substitution.
          apply nfo_formula_interpretation_substitution.
          simpl.
          apply all_equiv.
          intros.
          simpl.
          apply iff_trans with
              (B:=
                 nfo_formula_interpretation
                   (option context)
                   (fun x0 : option context =>
                      fo_term_interpretation
                        (option D) (option_rect (fun _ : option D => Univ) env_d x) 0
                        (add_var_to_environment context D env_cd x0)) f
              ).
          apply nfo_formula_interpretation_extensionality.
          intros.
          destruct l.
          simpl.
          unfold change_of_variable_in_terms.
          rewrite <- fo_term_interpretation_substitution.
          simpl.
          reflexivity.
          simpl.
          reflexivity.
          apply nfo_formula_interpretation_substitution.
        Defined.

        Section regular_formulas.

          (*Because COQ is intuitionnist, we need to restrict our analysis to
       a certain type of propositions; fortunately all interpretations of formulas will
       have the property we define below (and in fact, all formulas have it
       under the extra assumption that the excluded middle holds). *)

          Definition regular (P:Prop):Prop:= ((P -> False) -> False) -> P.

          Lemma regular_implies: forall A B:Prop,
              regular B -> regular (A -> B).
          Proof.
            intros A B.
            unfold regular.
            intros.
            apply H.
            intro.
            apply H0.
            intro.
            apply H2.
            apply H3.
            apply H1.
          Defined.

          Lemma regular_false: regular False.
          Proof.
            intro.
            apply H.
            intro; assumption.
          Defined.

          Lemma regular_forall: forall P: Univ -> Prop,
              (forall x:Univ, regular (P x)) -> regular (all P).
          Proof.
            intro P.
            unfold regular.
            intros.
            intro t.
            apply H.
            intro.
            apply H0.
            intro.
            apply H1.
            apply H2.
          Defined.

        End regular_formulas.

        Section the_soundness_theorem.

          Hypothesis regular_atoms:
            forall (C:Type) (env_c: C -> Univ)(p:NFO_Predicate C 0),
              regular (fo_predicate_interpretation C env_c 0 p).

          Theorem regular_interpretation: forall (C:Type)(env_c: C -> Univ)(f:NFO_Formula C),
              regular (nfo_formula_interpretation C env_c f).
          Proof.
            induction f.
            simpl.
            apply regular_atoms.
            simpl.
            apply regular_implies.
            apply regular_implies.
            apply regular_false.
            simpl.
            apply regular_forall.
            intros.
            apply IHf.
          Defined.

          Fixpoint nnd_soundness
                   (C:Type)
                   (hyp: NFO_Formula C -> Type)
                   (env_c: C -> Univ)
                   (true_hyp: forall h:NFO_Formula C,
                       hyp h -> nfo_formula_interpretation C env_c h)
                   (f:NFO_Formula C)
                   (pr: nand_natural_deduction C hyp f)
                   {struct pr}:
            nfo_formula_interpretation C env_c f.
          Proof.
            intros.
            destruct pr.
            apply true_hyp; assumption.
            simpl.
            intros.
            apply nnd_soundness with (env_c := env_c) in pr3.
            simpl in pr3.
            apply pr3.
            apply nnd_soundness with (env_c := env_c) in pr1.
            assumption.
            intros.
            destruct X.
            assumption.
            destruct a0.
            assumption.
            apply true_hyp.
            assumption.
            apply nnd_soundness with (env_c := env_c) in pr2.
            assumption.
            intros.
            destruct X.
            assumption.
            destruct a0.
            assumption.
            apply true_hyp.
            assumption.
            intros.
            destruct X.
            assumption.
            destruct a0.
            assumption.
            apply true_hyp.
            assumption.
            apply nnd_soundness with (env_c:= env_c) in pr1.
            apply nnd_soundness with (env_c:= env_c) in pr2.
            simpl in pr1.
            apply regular_interpretation.
            intro.
            apply pr1.
            assumption.
            intro; assumption.
            assumption.
            assumption.
            simpl.
            intro u.
            apply nnd_soundness with (hyp := constant_nfo_theory_embedding C hyp).
            intros.
            destruct X.
            apply nfo_formula_interpretation_substitution.
            apply nfo_formula_interpretation_extensionality with (env_c1:= env_c).
            intros.
            simpl.
            reflexivity.
            apply true_hyp.
            assumption.
            assumption.
            apply nnd_soundness with (env_c := env_c) in pr.
            simpl in pr.
            apply nfo_formula_interpretation_substitution.
            apply nfo_formula_interpretation_extensionality with
                (env_c1:= option_rect (fun _: option C => Univ) env_c
                                      (fo_term_interpretation C env_c 0 t)).
            intros.
            destruct l.
            simpl.
            reflexivity.
            simpl.
            reflexivity.
            apply pr.
            assumption.
          Defined.

        End the_soundness_theorem.

      End basic_semantics.

    End Proof_theory.

  End definitions_of_terms_predicates_and_formulas.

End Signatures_and_arities_of_formulas_and_terms.