Natural Deduction


Require Import List.
Import ListNotations.

Require Import Equations.Equations Equations.Prop.DepElim.
Require Import Lia.

Require Import SOL.
Require Import FullSyntax.
Require Import Subst.
Require Import Henkin Tarski.
Require Import VectorLib ListLib.
Require Import Decidable Enumerable.

Import SubstNotations.

Inductive peirce := class | intu.
Existing Class peirce.

Definition LEM := P, P P.

Section ND.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Implicit Type p : peirce.

  Reserved Notation "A ⊢ phi" (at level 61).
  Inductive prv : (p : peirce), list (form) form Prop :=

    (* Standard rules *)

    | II {p} A phi psi : ::A ⊢ A ⊢ -->
    | IE {p} A phi psi : A ⊢ --> A ⊢ A ⊢
    | Exp {p} A phi : A ⊢ ⊥ A ⊢
    | Ctx {p} A phi : A A ⊢
    | CI {p} A phi psi : A ⊢ A ⊢ A ⊢ ∧
    | CE1 {p} A phi psi : A ⊢ ∧ A ⊢
    | CE2 {p} A phi psi : A ⊢ ∧ A ⊢
    | DI1 {p} A phi psi : A ⊢ A ⊢ ∨
    | DI2 {p} A phi psi : A ⊢ A ⊢ ∨
    | DE {p} A phi psi theta : A ⊢ ∨ ::A ⊢ ::A ⊢ A ⊢
    | Peirce A phi psi : prv class A ((( --> ) --> ) --> )

    (* Quantifiers *)

    | AllI_i {p} A phi : map (subst_form_i ↑) A ⊢ A ⊢ ∀i
    | AllI_f {p} A ar phi : map (subst_form_f (↑ ar)) A ⊢ A ⊢ ∀f(ar)
    | AllI_p {p} A ar phi : map (subst_form_p (↑ ar)) A ⊢ A ⊢ ∀p(ar)

    | AllE_i {p} A t phi : A ⊢ ∀i A ⊢ [t..]i
    | AllE_f {p} A ar (f : function ar) phi : A ⊢ ∀f(ar) A ⊢ [f..]f
    | AllE_p {p} A ar (P : predicate ar) phi : A ⊢ ∀p(ar) A ⊢ [P..]p

    | ExI_i {p} A t phi : A ⊢ [t..]i A ⊢ ∃i
    | ExI_f {p} A ar (f : function ar) phi : A ⊢ [f..]f A ⊢ ∃f(ar)
    | ExI_p {p} A ar (P : predicate ar) phi : A ⊢ [P..]p A ⊢ ∃p(ar)

    | ExE_i {p} A phi psi : A ⊢ ∃i ::(map (subst_form_i ↑) A) ⊢ [↑]i A ⊢
    | ExE_f {p} A ar phi psi : A ⊢ ∃f(ar) ::(map (subst_form_f (↑ ar)) A) ⊢ [↑ ar]f A ⊢
    | ExE_p {p} A ar phi psi : A ⊢ ∃p(ar) ::(map (subst_form_p (↑ ar)) A) ⊢ [↑ ar]p A ⊢

    (* Comprehension *)
    | Comp {p} A ar phi : funcfree A ⊢ comprehension_form ar

  where "A ⊢ phi" := (prv _ A ).

  Definition tprv {p} (T : form Prop) (phi : form) :=
     A, ( psi, List.In A T ) @prv p A .

  Notation "A ⊢c phi" := (@prv class A ) (at level 55).
  Notation "A ⊢i phi" := (@prv intu A ) (at level 55).
  Notation "A ⊩ phi" := (tprv A ) (at level 55).
  Notation "A ⊩c phi" := (@tprv class A ) (at level 55).
  Notation "A ⊩i phi" := (@tprv intu A ) (at level 55).

Lemmas establishing soundess of the comprehension axiom

  Lemma forall_n_subst_i ar phi sigma :
    (forall_n ar )[]i = forall_n ar [iter up_i ar ]i.
  Proof.
    induction ar in |-*; cbn. reflexivity. rewrite IHar. f_equal. f_equal.
    apply subst_ext_i. now rewrite iter_switch.
  Qed.

  Lemma forall_n_subst_p ar phi sigma :
    (forall_n ar )[]p = forall_n ar []p.
  Proof.
    induction ar; cbn; congruence.
  Qed.

  Lemma forall_n_subst_f ar phi sigma :
    (forall_n ar )[]f = forall_n ar []f.
  Proof.
    induction ar; cbn; congruence.
  Qed.

  Lemma comprehension_subst_i phi ar sigma P :
    (forall_n ar (atom P (tabulate ar var_indi) <--> [↑ ar]p))[]i = forall_n ar (atom P (tabulate ar var_indi) <--> [iter up_i ar ]i[↑ ar]p).
  Proof.
    rewrite forall_n_subst_i. cbn. erewrite subst_switch_i_p, map_tabulate, tabulate_ext.
    reflexivity. clear P. cbn. induction ar; intros m H; cbn. lia. destruct m; cbn. reflexivity.
    rewrite IHar. reflexivity. lia.
  Qed.

  Lemma comprehension_subst_f phi ar sigma P :
    (forall_n ar (atom P (tabulate ar var_indi) <--> [↑ ar]p))[]f = forall_n ar (atom P (tabulate ar var_indi) <--> []f[↑ ar]p).
  Proof.
    rewrite forall_n_subst_f. cbn. erewrite subst_switch_f_p, map_tabulate, tabulate_ext.
    reflexivity. reflexivity.
  Qed.

  Lemma comprehension_subst_p phi ar sigma :
    (forall_n ar (p$0 (tabulate ar var_indi) <--> [↑ ar]p))[up_p ar]p = forall_n ar (p$0 (tabulate ar var_indi) <--> []p[↑ ar]p).
  Proof.
    rewrite forall_n_subst_p. cbn. erewrite nat_eq_dec_same, up_form_p, tabulate_ext.
    reflexivity. reflexivity.
  Qed.

  Lemma forall_n_to_vec D (I : interp D) rho n phi :
     ⊨ forall_n n v : vec D n, ⟨ VectorLib.fold_left scons (get_indi ) v, get_func , get_pred ⟩ ⊨ .
  Proof.
    enough ( rho_i rho_f rho_p, ⟨rho_i, rho_f, rho_p⟩ ⊨ forall_n n v : vec D n, ⟨ VectorLib.fold_left scons rho_i v, rho_f, rho_p ⟩ ⊨ ) by now destruct .
    intros. clear . revert rho_i. induction n; intros rho_i; cbn.
    - split.
      + intros H v. now dependent elimination v.
      + intros H. apply (H (Vector.nil _)).
    - split.
      + intros H v. dependent elimination v. cbn. apply IHn, H.
      + intros H d. apply IHn. intros v. apply (H (Vector.cons _ d _ v)).
  Qed.

  Lemma fold_left_scons_lookup D (rho_i : D) n m (v : vec D n) :
    VectorLib.fold_left scons rho_i v (n+m) = rho_i m.
  Proof.
    revert rho_i m. induction v; intros rho_i m; cbn.
    + reflexivity.
    + replace (S (n+m)) with (n + S m) by lia. rewrite IHv. reflexivity.
  Qed.

  Lemma eval_tabulate D (I : interp D) rho_i rho_f rho_p ar (v : vec D ar) :
    Vector.map (eval _ ⟨ VectorLib.fold_left scons rho_i v, rho_f, rho_p ⟩) (tabulate ar var_indi) = v.
  Proof.
    revert rho_i. induction v; intros rho_i; cbn.
    - reflexivity.
    - f_equal.
      + enough (VectorLib.fold_left scons (h .: rho_i) v (n + 0) = h) by now replace (n + 0) with n in H by lia.
        apply fold_left_scons_lookup.
      + apply IHv.
  Qed.

  Lemma comprehension_sound D (I : interp D) (rho : env D) ar phi :
     ⊨ comprehension_form ar .
  Proof.
    pose (Q := v : vec D ar True).
    exists ( v ⟨ VectorLib.fold_left scons (get_indi ) v, get_func , Q .: get_pred ⟩ ⊨ [↑ ar]p).
    apply forall_n_to_vec. intros v. cbn -[sat]. split.
    - intros H. cbn in H.
      destruct PeanoNat.Nat.eq_dec as [|]; try easy. apply sat_comp_p.
      eapply sat_ext. 2: apply sat_comp_p, H. split; cbn.
      + now rewrite eval_tabulate.
      + split; try easy; cbn. unfold shift, shift_p, scons, scons_env_pred, scons_ar.
        destruct PeanoNat.Nat.eq_dec as [|]; cbn. reflexivity.
        destruct n. destruct PeanoNat.Nat.eq_dec as [|]; try easy. reflexivity.
    - intros H. cbn. destruct PeanoNat.Nat.eq_dec as [|]; try easy.
      apply sat_comp_p. eapply sat_ext. 2: apply sat_comp_p, H. split; cbn.
      + now rewrite eval_tabulate.
      + split; try easy; cbn. unfold shift, shift_p, scons, scons_env_pred, scons_ar.
        destruct PeanoNat.Nat.eq_dec as [|]; cbn. reflexivity.
        destruct n. destruct PeanoNat.Nat.eq_dec as [|]; try easy. reflexivity.
  Qed.

Tarski Soundness

Soundess of the deduction system

  Theorem SoundnessI A phi :
    A ⊢i Tarski.valid A .
  Proof.
    remember intu as p.
    induction 1; intros D I HA.
    - intros . apply IHprv; trivial. intros [|]; firstorder.
    - apply ; trivial. apply ; trivial.
    - exfalso. eapply IHprv; trivial. apply HA.
    - firstorder.
    - split. now apply . now apply .
    - now apply IHprv.
    - now apply IHprv.
    - left. now apply IHprv.
    - right. now apply IHprv.
    - edestruct ; trivial. exact HA.
      + apply ; trivial. intros x [|]; firstorder.
      + apply ; trivial. intros x [|]; firstorder.
    - discriminate.
    - intros x. apply IHprv; trivial. intros [ [ ]]%in_map_iff.
      apply sat_comp_i. now destruct ; apply HA.
    - intros f. apply IHprv; trivial. intros [ [ ]]%in_map_iff.
      apply sat_comp_f. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      (* Why is this replace necessary? *)
      replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
      now rewrite eval_function_subst_cons_shift_f.
    - intros P. apply IHprv; trivial. intros [ [ ]]%in_map_iff.
      apply sat_comp_p. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
      now rewrite eval_predicate_subst_cons_shift_p.
    - eapply sat_comp_i, sat_ext. 2: apply (IHprv Heqp D I HA (eval _ t)).
      split; try easy. now destruct n.
    - eapply sat_comp_f, sat_ext. 2: eapply (IHprv Heqp D I HA (eval_function _ f)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - eapply sat_comp_p, sat_ext. 2: eapply (IHprv Heqp D I HA (eval_predicate _ P)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - exists (eval _ t). eapply sat_ext. 2: apply sat_comp_i, IHprv, HA; trivial.
      split; try easy. now destruct n.
    - exists (eval_function _ f). eapply sat_ext. 2: apply sat_comp_f, IHprv, HA; trivial.
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - exists (eval_predicate _ P). eapply sat_ext. 2: apply sat_comp_p, IHprv, HA; trivial.
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - edestruct as [x Hx]; eauto.
      specialize ( Heqp D I ⟨x .: get_indi , get_func , get_pred ⟩).
      apply sat_comp_i in . destruct ; apply .
      intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hx.
      apply sat_comp_i. destruct ; apply H'.
    - edestruct as [f Hf]; eauto.
      specialize ( Heqp D I ⟨get_indi , f .: get_func , get_pred ⟩).
      apply sat_comp_f in .
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hf.
        apply sat_comp_f. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
    - edestruct as [P HP]; eauto.
      specialize ( Heqp D I ⟨get_indi , get_func , P .: get_pred ⟩).
      apply sat_comp_p in .
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact HP.
        apply sat_comp_p. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
    - apply comprehension_sound.
  Qed.

  Theorem SoundnessC A phi :
    LEM A ⊢c Tarski.valid A .
  Proof.
    intros lem. induction 1; intros D I HA.
    - intros . apply IHprv. intros [|]; firstorder.
    - apply ; trivial. apply ; trivial.
    - exfalso. eapply IHprv. apply HA.
    - firstorder.
    - split. now apply . now apply .
    - now apply IHprv.
    - now apply IHprv.
    - left. now apply IHprv.
    - right. now apply IHprv.
    - edestruct . exact HA.
      + apply . intros x [|]; firstorder.
      + apply . intros x [|]; firstorder.
    - cbn. specialize (lem ( ⊨ )). tauto.
    - intros x. apply IHprv. intros [ [ ]]%in_map_iff.
      apply sat_comp_i. now destruct ; apply HA.
    - intros f. apply IHprv. intros [ [ ]]%in_map_iff.
      apply sat_comp_f. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      (* Why is this replace necessary? *)
      replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
      now rewrite eval_function_subst_cons_shift_f.
    - intros P. apply IHprv. intros [ [ ]]%in_map_iff.
      apply sat_comp_p. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
      now rewrite eval_predicate_subst_cons_shift_p.
    - eapply sat_comp_i, sat_ext. 2: apply (IHprv D I HA (eval _ t)).
      split; try easy. now destruct n.
    - eapply sat_comp_f, sat_ext. 2: eapply (IHprv D I HA (eval_function _ f)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - eapply sat_comp_p, sat_ext. 2: eapply (IHprv D I HA (eval_predicate _ P)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - exists (eval _ t). eapply sat_ext. 2: apply sat_comp_i, IHprv, HA.
      split; try easy. now destruct n.
    - exists (eval_function _ f). eapply sat_ext. 2: apply sat_comp_f, IHprv, HA.
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - exists (eval_predicate _ P). eapply sat_ext. 2: apply sat_comp_p, IHprv, HA.
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - edestruct as [x Hx]; eauto.
      specialize ( D I ⟨x .: get_indi , get_func , get_pred ⟩).
      apply sat_comp_i in . destruct ; apply .
      intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hx.
      apply sat_comp_i. destruct ; apply H'.
    - edestruct as [f Hf]; eauto.
      specialize ( D I ⟨get_indi , f .: get_func , get_pred ⟩).
      apply sat_comp_f in .
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hf.
        apply sat_comp_f. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
    - edestruct as [P HP]; eauto.
      specialize ( D I ⟨get_indi , get_func , P .: get_pred ⟩).
      apply sat_comp_p in .
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact HP.
        apply sat_comp_p. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
    - apply comprehension_sound.
  Qed.

  Corollary SoundnessIT T phi :
    T ⊩i Tarski.validT T .
  Proof.
    intros [A [HA ]] D I HT. eapply SoundnessI. apply .
    intros . apply HT, HA, .
  Qed.

  Corollary SoundnessCT T phi :
    LEM T ⊩c Tarski.validT T .
  Proof.
    intros lem [A [HA ]] D I HT. eapply SoundnessC; trivial. apply .
    intros . apply HT, HA, .
  Qed.

End ND.

Arguments prv {_ _ _} _ _.
Notation "A ⊢ phi" := (prv A ) (at level 61).
Notation "A ⊢c phi" := (@prv _ _ class A ) (at level 55).
Notation "A ⊢i phi" := (@prv _ _ intu A ) (at level 55).
Notation "A ⊩ phi" := (tprv A ) (at level 55).
Notation "A ⊩c phi" := (@tprv _ _ class A ) (at level 55).
Notation "A ⊩i phi" := (@tprv _ _ intu A ) (at level 55).

Enumerability


Section Enumerability.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Context {L_Funcs : list syms}.
  Hypothesis enum_Funcs' : list_enumerator__T L_Funcs syms.

  Context {L_Preds : list preds}.
  Hypothesis enum_Preds' : list_enumerator__T L_Preds preds.

  Hypothesis eq_dec_Funcs : eq_dec syms.
  Hypothesis eq_dec_Preds : eq_dec preds.

  Instance enum_term' : list_enumerator__T (L_term _ _) term := enum_term _ _.
  Instance enum_form' : list_enumerator__T (L_form _ _ _ _ _ _ _ _) form := enum_form _ _ _ _ _ _ _ _.

Redefine notation to avoid conflict with subst notation
  Notation "`[ s | p ∈ A ]" :=
    (map ( p s) A) (p pattern).

  Instance funcfree_dec phi : dec (funcfree ) := funcfree_dec .

  Fixpoint L_prv {p : peirce} (A : list form) (n : ) : list form := match n with
    | 0 A
    | S n L_prv A n
                 concat `[ [ --> | psi ∈ L_prv ( :: A) n ] | phi ∈ L_T form n ]
                 [ | (phi, psi) ∈ (L_prv A n × L_T form n) , ( --> L_prv A n) ]
                 [ | phi ∈ L_T form n, ⊥ L_prv A n ]
                 [ ∧ | (phi, psi) ∈ (L_prv A n × L_prv A n) ]
                 [ | (phi, psi) ∈ (L_T form n × L_T form n), ∧ L_prv A n]
                 [ | (phi, psi) ∈ (L_T form n × L_T form n), ∧ L_prv A n]
                 [ ∨ | (phi, psi) ∈ (L_T form n × L_T form n), L_prv A n]
                 [ ∨ | (phi, psi) ∈ (L_T form n × L_T form n), L_prv A n]
                 [ | (phi, psi, theta) ∈ (L_T form n × L_T form n × L_T form n),
                              L_prv (::A) n L_prv (::A) n ∨ L_prv A n]
                 (if p then [ (( --> ) --> ) --> | (phi, psi) ∈ (L_T form n × L_T form n) ] else nil )
                 [ ∀i | phi ∈ L_prv (map (subst_form_i ↑) A) n ]
                 concat `[ [ ∀f(ar) | phi ∈ L_prv (map (subst_form_f (↑ ar)) A) n ] | ar ∈ L_nat n ]
                 concat `[ [ ∀p(ar) | phi ∈ L_prv (map (subst_form_p (↑ ar)) A) n ] | ar ∈ L_nat n ]
                 [ [t..]i | (phi, t) ∈ (L_T form n × L_T term n), (∀i ) L_prv A n ]
                 [ [(var_func x ar)..]f | (x, ar, phi) ∈ (L_nat n × L_nat n × L_T form n), (∀f(ar) ) L_prv A n ]
                 [ [(sym f)..]f | (f, phi) ∈ (L_T n × L_T form n), (∀f(ar_syms f) ) L_prv A n ]
                 [ [(var_pred x ar)..]p | (x, ar, phi) ∈ (L_nat n × L_nat n × L_T form n), (∀p(ar) ) L_prv A n ]
                 [ [(pred P)..]p | (P, phi) ∈ (L_T n × L_T form n), (∀p(ar_preds P) ) L_prv A n ]
                 [ ∃i | (phi, t) ∈ (L_T form n × L_T term n), ([t..]i) L_prv A n ]
                 [ ∃f(ar) | (x, ar, phi) ∈ (L_nat n × L_nat n × L_T form n), ([(var_func x ar)..]f) L_prv A n ]
                 [ ∃f(ar_syms f) | (f, phi) ∈ (L_T n × L_T form n), ([(sym f)..]f) L_prv A n ]
                 [ ∃p(ar) | (x, ar, phi) ∈ (L_nat n × L_nat n × L_T form n), ([(var_pred x ar)..]p) L_prv A n ]
                 [ ∃p(ar_preds P) | (P, phi) ∈ (L_T n × L_T form n), ([(pred P)..]p) L_prv A n ]
                 [ | (phi, psi) ∈ (L_T form n × L_T form n), (∃i ) L_prv A n [↑]i L_prv (::(map (subst_form_i ↑) A)) n ]
                 [ | (phi, psi, ar) ∈ (L_T form n × L_T form n × L_nat n), (∃f(ar) ) L_prv A n [↑ ar]f L_prv (::(map (subst_form_f (↑ ar)) A)) n ]
                 [ | (phi, psi, ar) ∈ (L_T form n × L_T form n × L_nat n), (∃p(ar) ) L_prv A n [↑ ar]p L_prv (::(map (subst_form_p (↑ ar)) A)) n ]
                 [ ∃p(ar) (forall_n ar (p$0 (tabulate ar var_indi) <--> [↑ ar]p)) | (ar, phi) ∈ (L_nat n × L_T form n), funcfree ]
  end.

  Lemma enum_prv {p : peirce} A :
    list_enumerator (L_prv A) (prv A).
  Proof with eapply cum_ge'; eauto; lia.
    split.
    - rename x into . induction 1.
      + destruct IHprv as [], (el_T ) as []. exists (S ( + )); cbn.
        in_app 2. eapply in_concat_iff. eexists. split. 2:in_collect ... in_collect ...
      + destruct as [], as [], (el_T ) as []. exists (S ( + + )); cbn.
        in_app 3. in_collect (, )...
      + destruct IHprv as [], (el_T ) as []. exists (S ( + )); cbn.
        in_app 4. in_collect ...
      + now exists 0.
      + destruct as [], as []. exists (S ( + )); cbn.
        in_app 5. in_collect (, )...
      + destruct IHprv as [], (el_T ) as [], (el_T ) as []. exists (S ( + + )); cbn.
        in_app 6. in_collect (, )...
      + destruct IHprv as [], (el_T ) as [], (el_T ) as []. exists (S ( + + )); cbn.
        in_app 7. in_collect (, )...
      + destruct IHprv as [], (el_T ) as [], (el_T ) as []. exists (S ( + + )); cbn.
        in_app 8. in_collect (, )...
      + destruct IHprv as [], (el_T ) as [], (el_T ) as []. exists (S ( + + )); cbn.
        in_app 9. in_collect (, )...
      + destruct as [], as [], as [], (el_T ) as [], (el_T ) as [], (el_T ) as [].
        exists (S ( + + + + + )); cbn.
        in_app 10. in_collect (, , )...
      + destruct (el_T ) as [], (el_T ) as []. exists (S ( + )); cbn.
        in_app 11. in_collect (, )...
      + destruct IHprv as [m]. exists (S m); cbn. in_app 12. in_collect ...
      + destruct IHprv as [m]. exists (S (m + ar)); cbn.
        in_app 13. apply in_concat_iff. eexists. split.
        2: in_collect ar; apply L_nat_correct; lia. in_collect ...
      + destruct IHprv as [m]. exists (S (m + ar)); cbn.
        in_app 14. apply in_concat_iff. eexists. split.
        2: in_collect ar; apply L_nat_correct; lia. in_collect ...
      + destruct IHprv as [], (el_T ) as [], (el_T t) as []. exists (S( + + )); cbn.
        in_app 15. in_collect (, t)...
      + destruct IHprv as [], (el_T ) as []. destruct f.
        * exists (S ( + + n + ar)); cbn. in_app 16. in_collect (n, ar, ); try (apply L_nat_correct; lia)...
        * destruct (el_T f) as []. exists (S ( + + )); cbn. in_app 17. in_collect (f, )...
      + destruct IHprv as [], (el_T ) as []. destruct P.
        * exists (S ( + + n + ar)); cbn. in_app 18. in_collect (n, ar, ); try (apply L_nat_correct; lia)...
        * destruct (el_T P) as []. exists (S ( + + )); cbn. in_app 19. in_collect (P, )...
      + destruct IHprv as [], (el_T ) as [], (el_T t) as []. exists (S ( + + )); cbn.
        in_app 20. in_collect (, t)...
      + destruct IHprv as [], (el_T ) as []. destruct f.
        * exists (S ( + + n + ar)); cbn. in_app 21. in_collect (n, ar, ); try (apply L_nat_correct; lia)...
        * destruct (el_T f) as []. exists (S ( + + )); cbn. in_app 22. in_collect (f, )...
      + destruct IHprv as [], (el_T ) as []. destruct P.
        * exists (S ( + + n + ar)); cbn. in_app 23. in_collect (n, ar, ); try (apply L_nat_correct; lia)...
        * destruct (el_T P) as []. exists (S ( + + )); cbn. in_app 24. in_collect (P, )...
      + destruct as [], as [], (el_T ) as [], (el_T ) as []. exists (S ( + + + )); cbn.
        in_app 25. in_collect (, )...
      + destruct as [], as [], (el_T ) as [], (el_T ) as []. exists (S ( + + + + ar)); cbn.
        in_app 26. in_collect (, , ar); try (apply L_nat_correct; lia)...
      + destruct as [], as [], (el_T ) as [], (el_T ) as []. exists (S ( + + + + ar)); cbn.
        in_app 27. in_collect (, , ar); try (apply L_nat_correct; lia)...
      + destruct (el_T ) as [m]. exists (S (m + ar)); cbn.
        in_app 28. in_collect (ar, ); try (apply L_nat_correct; lia)...
    - intros [m]; induction m in A, x, H |-*; cbn in *.
      + now apply Ctx.
      + inv_collect.
        * eapply II; apply IHm; eauto.
        * eapply IE; apply IHm; eauto.
        * eapply Exp; apply IHm; eauto.
        * eapply CI; apply IHm; eauto.
        * eapply CE1; apply IHm; eauto.
        * eapply CE2; apply IHm; eauto.
        * eapply DI1; apply IHm; eauto.
        * eapply DI2; apply IHm; eauto.
        * eapply DE; apply IHm; eauto.
        * destruct p; cbn. inv_collect. apply Peirce. easy.
        * eapply AllI_i; apply IHm; eauto.
        * eapply AllI_f; apply IHm; eauto.
        * eapply AllI_p; apply IHm; eauto.
        * eapply AllE_i; apply IHm; eauto.
        * eapply AllE_f; apply IHm; eauto.
        * eapply AllE_f; apply IHm; eauto.
        * eapply AllE_p; apply IHm; eauto.
        * eapply AllE_p; apply IHm; eauto.
        * eapply ExI_i; apply IHm; eauto.
        * eapply ExI_f; apply IHm; eauto.
        * eapply ExI_f; apply IHm; eauto.
        * eapply ExI_p; apply IHm; eauto.
        * eapply ExI_p; apply IHm; eauto.
        * eapply ExE_i; apply IHm; eauto.
        * eapply ExE_f; apply IHm; eauto.
        * eapply ExE_p; apply IHm; eauto.
        * now eapply Comp.
  Qed.

  Lemma prv_enumerable {p : peirce} A :
    enumerable ( phi A ⊢ ).
  Proof.
    apply list_enumerable_enumerable. exists (L_prv A). apply enum_prv.
  Qed.

End Enumerability.

Deduction Facts


Section Facts.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {p : peirce}.

Weakening

  Theorem Weak A B phi :
    A B A ⊢ B ⊢ .
  Proof.
    intros H. revert B . induction H; intros B HB;
    try unshelve (solve [econstructor; intuition]); try now econstructor.
  Qed.

  Lemma subst_Weak_i sigma A phi :
    ( x, funcfreeTerm ( x)) A ⊢ List.map (subst_form_i ) A ⊢ []i.
  Proof.
    intros Hsigma H. revert Hsigma. induction H; intros Hsigma; cbn in *.
    - now apply II, IHprv.
    - eapply IE. now apply . now apply .
    - now apply Exp, IHprv.
    - apply Ctx, List.in_map, H.
    - apply CI. now apply . now apply .
    - now eapply CE1, IHprv.
    - now eapply CE2, IHprv.
    - now eapply DI1, IHprv.
    - now eapply DI2, IHprv.
    - eapply DE. now apply . now apply . now apply .
    - apply Peirce.
    - apply AllI_i. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros []; cbn. easy. now apply funcfreeTerm_subst_i. intros ?. now setoid_rewrite up_form_i.
    - apply AllI_f. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros x. now apply funcfreeTerm_subst_f. intros ?. apply subst_switch_i_f.
    - apply AllI_p. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. easy. intros ?. apply subst_switch_i_p.
    - specialize (IHprv ). apply AllE_i with ( := t[]i) in IHprv; trivial.
      rewrite subst_comp_i in *. erewrite subst_ext_i. apply IHprv. intros []; cbn; trivial.
      now setoid_rewrite subst_term_shift_i.
    - specialize (IHprv ). apply AllE_f with ( := f) in IHprv; trivial.
      rewrite subst_switch_i_f in IHprv. erewrite subst_ext_i. apply IHprv. intros n.
      now setoid_rewrite subst_term_shift_f.
    - specialize (IHprv ). apply AllE_p with ( := P) in IHprv; trivial.
      rewrite subst_switch_i_p in IHprv. erewrite subst_ext_p. apply IHprv. reflexivity.
    - specialize (IHprv ). eapply ExI_i with ( := t[]i). rewrite subst_comp_i in *.
      erewrite subst_ext_i. apply IHprv; trivial. intros [|]; cbn; trivial.
      now setoid_rewrite subst_term_shift_i.
    - specialize (IHprv ). eapply ExI_f with ( := f). rewrite subst_switch_i_f.
      erewrite subst_ext_i. apply IHprv; trivial. intros n. now setoid_rewrite subst_term_shift_f.
    - specialize (IHprv ). eapply ExI_p with ( := P). rewrite subst_switch_i_p.
      erewrite subst_ext_i. apply IHprv; trivial. reflexivity.
    - eapply ExE_i in ; trivial. eassumption. rewrite List.map_map. specialize ( (up_i )).
      setoid_rewrite up_form_i in . erewrite List.map_map, List.map_ext in .
      apply . intros []; cbn. easy. now apply funcfreeTerm_subst_i. intros ?. apply up_form_i.
    - eapply ExE_f in ; trivial. eassumption. rewrite List.map_map. specialize ( ( >> subst_f (↑ ar))).
      rewrite subst_switch_i_f. erewrite List.map_map, List.map_ext in .
      apply . intros x. now apply funcfreeTerm_subst_f. intros ?. now setoid_rewrite subst_switch_i_f.
    - eapply ExE_p in ; trivial. eassumption. rewrite List.map_map. specialize ( ).
      rewrite subst_switch_i_p. erewrite List.map_map, List.map_ext in .
      apply . easy. intros ?. now setoid_rewrite subst_switch_i_p.
    - rewrite comprehension_subst_i. apply Comp. apply funcfree_subst_i; trivial.
      induction ar; intros x; cbn. easy. destruct x; cbn. easy. now apply funcfreeTerm_subst_i.
  Qed.

  Lemma subst_Weak_f sigma A phi :
    A ⊢ List.map (subst_form_f ) A ⊢ []f.
  Proof.
    induction 1 in |- *; cbn in *.
    - apply II, IHprv.
    - eapply IE. apply . apply .
    - apply Exp, IHprv.
    - apply Ctx, List.in_map, H.
    - apply CI. apply . apply .
    - eapply CE1, IHprv.
    - eapply CE2, IHprv.
    - eapply DI1, IHprv.
    - eapply DI2, IHprv.
    - eapply DE. apply . apply . apply .
    - apply Peirce.
    - apply AllI_i. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros ?. symmetry. now setoid_rewrite subst_switch_i_f.
    - apply AllI_f. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros ?. now setoid_rewrite up_form_f.
    - apply AllI_p. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros ?. apply subst_switch_f_p.
    - specialize (IHprv ). apply AllE_i with ( := t[]f) in IHprv.
      rewrite subst_switch_i_f. erewrite subst_ext_i. apply IHprv. now intros [].
    - specialize (IHprv ). apply AllE_f with ( := f[]f) in IHprv.
      rewrite subst_comp_f in *. erewrite subst_ext_f. apply IHprv. intros [] ar'; cbn;
      repeat (try rewrite nat_eq_dec_same; try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn);
      now setoid_rewrite subst_function_shift_f.
    - specialize (IHprv ). apply AllE_p with ( := P) in IHprv.
      rewrite subst_switch_f_p in IHprv. erewrite subst_ext_p. apply IHprv. reflexivity.
    - specialize (IHprv ). eapply ExI_i with ( := t[]f). rewrite subst_switch_i_f in IHprv.
      erewrite subst_ext_i. apply IHprv. intros [|]; cbn; trivial.
    - specialize (IHprv ). eapply ExI_f with ( := f[]f). rewrite subst_comp_f in *.
      erewrite subst_ext_f. apply IHprv. intros [] ar'; cbn;
      repeat (try rewrite nat_eq_dec_same; try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn);
      now setoid_rewrite subst_function_shift_f.
    - specialize (IHprv ). eapply ExI_p with ( := P). rewrite subst_switch_f_p.
      erewrite subst_ext_f. apply IHprv. reflexivity.
    - eapply ExE_i in . eassumption. rewrite List.map_map. specialize ( ).
      rewrite subst_switch_i_f in . erewrite List.map_map, List.map_ext in .
      apply . intros ?. now setoid_rewrite subst_switch_i_f.
    - eapply ExE_f in . eassumption. rewrite List.map_map. specialize ( (up_f ar)).
      setoid_rewrite up_form_f in . erewrite List.map_map, List.map_ext in .
      apply . intros ?. apply up_form_f.
    - eapply ExE_p in . eassumption. rewrite List.map_map. specialize ( ).
      rewrite subst_switch_f_p. erewrite List.map_map, List.map_ext in .
      apply . intros ?. now setoid_rewrite subst_switch_f_p.
    - rewrite comprehension_subst_f. now apply Comp, funcfree_subst_f.
  Qed.

  Lemma subst_Weak_p sigma A phi :
    A ⊢ List.map (subst_form_p ) A ⊢ []p.
  Proof.
    induction 1 in |- *; cbn in *.
    - apply II, IHprv.
    - eapply IE. apply . apply .
    - apply Exp, IHprv.
    - apply Ctx, List.in_map, H.
    - apply CI. apply . apply .
    - eapply CE1, IHprv.
    - eapply CE2, IHprv.
    - eapply DI1, IHprv.
    - eapply DI2, IHprv.
    - eapply DE. apply . apply . apply .
    - apply Peirce.
    - apply AllI_i. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros ?. symmetry. apply subst_switch_i_p.
    - apply AllI_f. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros ?. symmetry. apply subst_switch_f_p.
    - apply AllI_p. setoid_rewrite List.map_map in IHprv. erewrite List.map_map, List.map_ext.
      apply IHprv. intros ?. now setoid_rewrite up_form_p.
    - specialize (IHprv ). apply AllE_i with ( := t) in IHprv.
      rewrite subst_switch_i_p. erewrite subst_ext_i. apply IHprv. now intros [].
    - specialize (IHprv ). apply AllE_f with ( := f) in IHprv.
      rewrite subst_switch_f_p in IHprv. erewrite subst_ext_p. apply IHprv. reflexivity.
    - specialize (IHprv ). apply AllE_p with ( := P[]p) in IHprv.
      rewrite subst_comp_p in *. erewrite subst_ext_p. apply IHprv. intros [] ar'; cbn;
      repeat (try rewrite nat_eq_dec_same; try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn);
      now setoid_rewrite subst_predicate_shift_p.
    - specialize (IHprv ). eapply ExI_i with ( := t). rewrite subst_switch_i_p in IHprv.
      erewrite subst_ext_i. apply IHprv. intros [|]; cbn; trivial.
    - specialize (IHprv ). eapply ExI_f with ( := f). rewrite subst_switch_f_p.
      erewrite subst_ext_f. apply IHprv. reflexivity.
    - specialize (IHprv ). eapply ExI_p with ( := P[]p). rewrite subst_comp_p in *.
      erewrite subst_ext_p. apply IHprv. intros [] ar'; cbn;
      repeat (try rewrite nat_eq_dec_same; try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn);
      now setoid_rewrite subst_predicate_shift_p.
    - eapply ExE_i in . eassumption. rewrite List.map_map. specialize ( ).
      rewrite subst_switch_i_p in . erewrite List.map_map, List.map_ext in .
      apply . intros ?. now setoid_rewrite subst_switch_i_p.
    - eapply ExE_f in . eassumption. rewrite List.map_map. specialize ( ).
      rewrite subst_switch_f_p. erewrite List.map_map, List.map_ext in .
      apply . intros ?. now setoid_rewrite subst_switch_f_p.
    - eapply ExE_p in . eassumption. rewrite List.map_map. specialize ( (up_p ar)).
      setoid_rewrite up_form_p in . erewrite List.map_map, List.map_ext in .
      apply . intros ?. apply up_form_p.
    - rewrite comprehension_subst_p. now apply Comp, funcfree_subst_p.
  Qed.

Nameless quantifier rules

  Definition cycle_shift_i n : term :=
     x if PeanoNat.Nat.eq_dec n x then i$0 else i$(S x).

  Definition cycle_shift_f n ar : ar, function ar :=
     x ar' if PeanoNat.Nat.eq_dec ar' ar
                 then if PeanoNat.Nat.eq_dec n x then var_func 0 else var_func (S x)
                 else var_func x.

  Definition cycle_shift_p n ar : ar, predicate ar :=
     x ar' if PeanoNat.Nat.eq_dec ar' ar
                 then if PeanoNat.Nat.eq_dec n x then var_pred 0 else var_pred (S x)
                 else var_pred x.

  Lemma cycle_shift_shift_i n phi :
    bounded_indi n [cycle_shift_i n]i = [↑]i.
  Proof.
    intros B. eapply subst_ext_bounded_i. apply B. intros k. unfold cycle_shift_i.
    destruct PeanoNat.Nat.eq_dec; trivial; lia.
  Qed.

  Lemma cycle_shift_shift_f n ar phi :
    bounded_func ar n [cycle_shift_f n ar]f = [↑ ar]f.
  Proof.
    intros B. eapply subst_ext_bounded_f. apply B. intros k ar'. unfold cycle_shift_f, shift, shift_f.
    repeat destruct PeanoNat.Nat.eq_dec; trivial; lia.
  Qed.

  Lemma cycle_shift_shift_p n ar phi :
    bounded_pred ar n [cycle_shift_p n ar]p = [↑ ar]p.
  Proof.
    intros B. eapply subst_ext_bounded_p. apply B. intros k ar'. unfold cycle_shift_p, shift, shift_p.
    repeat destruct PeanoNat.Nat.eq_dec; trivial; lia.
  Qed.

  Lemma cycle_shift_subject_i n phi :
    bounded_indi (S n) [(i$n)..]i[cycle_shift_i n]i = .
  Proof.
    intros B. erewrite subst_comp_i, subst_ext_bounded_i, subst_id_i; trivial.
    apply B. intros []; cbn; unfold cycle_shift_i; destruct PeanoNat.Nat.eq_dec; trivial; lia.
  Qed.

  Lemma cycle_shift_subject_f n ar phi :
    bounded_func ar (S n) [(var_func n ar)..]f[cycle_shift_f n ar]f = .
  Proof.
    intros B. erewrite subst_comp_f, subst_ext_bounded_f, subst_id_f; trivial.
    apply B. intros [] ar'; cbn; unfold cycle_shift_f;
    repeat (destruct PeanoNat.Nat.eq_dec as [|]; cbn; try rewrite !nat_eq_dec_same; cbn); trivial; lia.
  Qed.

  Lemma cycle_shift_subject_p n ar phi :
    bounded_pred ar (S n) [(var_pred n ar)..]p[cycle_shift_p n ar]p = .
  Proof.
    intros B. erewrite subst_comp_p, subst_ext_bounded_p, subst_id_p; trivial.
    apply B. intros [] ar'; cbn; unfold cycle_shift_p;
    repeat (destruct PeanoNat.Nat.eq_dec as [|]; cbn; try rewrite !nat_eq_dec_same; cbn); trivial; lia.
  Qed.

  Lemma nameless_equiv_all_i' A phi n :
    bounded_indi_L n A bounded_indi (S n) [p[↑]i | p ∈ A] ⊢ A ⊢ [(i$n)..]i.
  Proof.
    intros . split; intros H.
    - apply (subst_Weak_i (i$n)..) in H. rewrite map_map in *.
      erewrite List.map_ext, map_id in H; try apply H. intros. apply subst_form_shift_i.
      now intros [].
    - apply (subst_Weak_i (cycle_shift_i n)) in H. rewrite (List.map_ext_in _ (subst_form_i ↑)) in H.
      + now rewrite cycle_shift_subject_i in H.
      + intros HP. now apply cycle_shift_shift_i, .
      + intros x. unfold cycle_shift_i. now destruct PeanoNat.Nat.eq_dec.
  Qed.

  Lemma nameless_equiv_all_f' A phi n ar :
    bounded_func_L ar n A bounded_func ar (S n) [p[↑ ar]f | p ∈ A] ⊢ A ⊢ [(var_func n ar)..]f.
  Proof.
    intros . split; intros H.
    - apply (subst_Weak_f (var_func n ar)..) in H. rewrite map_map in *.
      erewrite List.map_ext, map_id in H; try apply H. intros. apply subst_form_shift_f.
    - apply (subst_Weak_f (cycle_shift_f n ar)) in H. rewrite (List.map_ext_in _ (subst_form_f (↑ ar))) in H.
      + now rewrite cycle_shift_subject_f in H.
      + intros HP. now apply cycle_shift_shift_f, .
  Qed.

  Lemma nameless_equiv_all_p' A phi n ar :
    bounded_pred_L ar n A bounded_pred ar (S n) [p[↑ ar]p | p ∈ A] ⊢ A ⊢ [(var_pred n ar)..]p.
  Proof.
    intros . split; intros H.
    - apply (subst_Weak_p (var_pred n ar)..) in H. rewrite map_map in *.
      erewrite List.map_ext, map_id in H; try apply H. intros. apply subst_form_shift_p.
    - apply (subst_Weak_p (cycle_shift_p n ar)) in H. rewrite (List.map_ext_in _ (subst_form_p (↑ ar))) in H.
      + now rewrite cycle_shift_subject_p in H.
      + intros HP. now apply cycle_shift_shift_p, .
  Qed.

  Lemma nameless_equiv_ex_i' A phi psi n :
    bounded_indi_L n A bounded_indi n bounded_indi (S n) (::[[↑]i | p0 ∈ A]) ⊢ [↑]i ([(i$n)..]i::A) ⊢ .
  Proof.
    intros HL Hphi Hpsi. split.
    - intros H % (subst_Weak_i ((i$n)..)). cbn in *.
      erewrite map_map, List.map_ext, map_id in H.
      + now rewrite subst_form_shift_i in H.
      + intros. apply subst_form_shift_i.
      + now intros [].
    - intros H % (subst_Weak_i (cycle_shift_i n)). cbn in *.
      rewrite (List.map_ext_in _ (subst_form_i ↑)) in H.
      + setoid_rewrite cycle_shift_subject_i in H. now rewrite cycle_shift_shift_i in H. easy.
      + intros HT. now apply cycle_shift_shift_i, HL.
      + intros x. unfold cycle_shift_i. now destruct PeanoNat.Nat.eq_dec.
  Qed.

  Lemma nameless_equiv_ex_f' A phi psi n ar :
    bounded_func_L ar n A bounded_func ar n bounded_func ar (S n) (::[[↑ ar]f | p0 ∈ A]) ⊢ [↑ ar]f ([(var_func n ar)..]f::A) ⊢ .
  Proof.
    intros HL Hphi Hpsi. split.
    - intros H % (subst_Weak_f ((var_func n ar)..)). cbn in *.
      erewrite map_map, List.map_ext, map_id in H.
      + now rewrite subst_form_shift_f in H.
      + intros. apply subst_form_shift_f.
    - intros H % (subst_Weak_f (cycle_shift_f n ar)). cbn in *.
      rewrite (List.map_ext_in _ (subst_form_f (↑ ar))) in H.
      + setoid_rewrite cycle_shift_subject_f in H. now rewrite cycle_shift_shift_f in H. easy.
      + intros HT. now apply cycle_shift_shift_f, HL.
  Qed.

  Lemma nameless_equiv_ex_p' A phi psi n ar :
    bounded_pred_L ar n A bounded_pred ar n bounded_pred ar (S n) (::[[↑ ar]p | p0 ∈ A]) ⊢ [↑ ar]p ([(var_pred n ar)..]p::A) ⊢ .
  Proof.
    intros HL Hphi Hpsi. split.
    - intros H % (subst_Weak_p ((var_pred n ar)..)). cbn in *.
      erewrite map_map, List.map_ext, map_id in H.
      + now rewrite subst_form_shift_p in H.
      + intros. apply subst_form_shift_p.
    - intros H % (subst_Weak_p (cycle_shift_p n ar)). cbn in *.
      rewrite (List.map_ext_in _ (subst_form_p (↑ ar))) in H.
      + setoid_rewrite cycle_shift_subject_p in H. now rewrite cycle_shift_shift_p in H. easy.
      + intros HT. now apply cycle_shift_shift_p, HL.
  Qed.

  Lemma nameless_equiv_all_i A phi :
    { t | map (subst_form_i ↑) A ⊢ A ⊢ [t..]i }.
  Proof.
    destruct (find_bounded_indi_L (::A)) as [n H].
    exists i$n. apply nameless_equiv_all_i'.
    - intros ? ?. apply H. auto.
    - eapply bounded_indi_up; try apply H; auto.
  Qed.

  Lemma nameless_equiv_ex_i A phi psi :
    { t | ( :: List.map (subst_form_i ↑) A) ⊢ [↑]i ([t..]i::A) ⊢ }.
  Proof.
    destruct (find_bounded_indi_L (::::A)) as [n H].
    exists i$n. apply nameless_equiv_ex_i'.
    - intros ? ?. apply H. auto.
    - apply H. auto.
    - eapply bounded_indi_up; try apply H; auto.
  Qed.

  Lemma nameless_equiv_all_f A phi ar :
    { x | map (subst_form_f (↑ ar)) A ⊢ A ⊢ [(var_func x ar)..]f }.
  Proof.
    destruct (find_bounded_func_L ar (::A)) as [n H].
    exists n. apply nameless_equiv_all_f'.
    - intros ? ?. apply H. auto.
    - eapply bounded_func_up; try apply H; auto.
  Qed.

  Lemma nameless_equiv_ex_f A phi psi ar :
    { x | ( :: List.map (subst_form_f (↑ ar)) A) ⊢ [↑ ar]f ([(var_func x ar)..]f::A) ⊢ }.
  Proof.
    destruct (find_bounded_func_L ar (::::A)) as [n H].
    exists n. apply nameless_equiv_ex_f'.
    - intros ? ?. apply H. auto.
    - apply H. auto.
    - eapply bounded_func_up; try apply H; auto.
  Qed.

  Lemma nameless_equiv_all_p A phi ar :
    { x | map (subst_form_p (↑ ar)) A ⊢ A ⊢ [(var_pred x ar)..]p }.
  Proof.
    destruct (find_bounded_pred_L ar (::A)) as [n H].
    exists n. apply nameless_equiv_all_p'.
    - intros ? ?. apply H. auto.
    - eapply bounded_pred_up; try apply H; auto.
  Qed.

  Lemma nameless_equiv_ex_p A phi psi ar :
    { x | ( :: List.map (subst_form_p (↑ ar)) A) ⊢ [↑ ar]p ([(@var_pred _ x ar)..]p::A) ⊢ }.
  Proof.
    destruct (find_bounded_pred_L ar (::::A)) as [n H].
    exists n. apply nameless_equiv_ex_p'.
    - intros ? ?. apply H. auto.
    - apply H. auto.
    - eapply bounded_pred_up; try apply H; auto.
  Qed.

Helper lemmas for proving equivalences

  Lemma switch_imp A phi psi :
    (::A ⊢ ) (A ⊢ --> ).
  Proof.
    split; intros H. now apply II. eapply IE. eapply Weak. 2: apply H. firstorder. now apply Ctx.
  Qed.

  Lemma prv_equiv_bin op phi1 phi2 psi1 psi2 A :
    A ⊢ <--> A ⊢ <--> A ⊢ (bin op ) <--> (bin op ).
  Proof.
    intros . destruct op; cbn.
    - apply CI.
      + apply II. apply CI.
        * eapply IE. eapply CE1. eapply Weak. 2: apply ; firstorder. firstorder. eapply CE1. now apply Ctx.
        * eapply IE. eapply CE1. eapply Weak. 2: apply ; firstorder. firstorder. eapply CE2. now apply Ctx.
      + apply II. apply CI.
        * eapply IE. eapply CE2. eapply Weak. 2: apply ; firstorder. firstorder. eapply CE1. now apply Ctx.
        * eapply IE. eapply CE2. eapply Weak. 2: apply ; firstorder. firstorder. eapply CE2. now apply Ctx.
    - apply CI.
      + apply II. eapply DE. now apply Ctx.
        * apply DI1. eapply IE. eapply CE1. eapply Weak. 2: apply ; firstorder. firstorder. now apply Ctx.
        * apply DI2. eapply IE. eapply CE1. eapply Weak. 2: apply ; firstorder. firstorder. now apply Ctx.
      + apply II. eapply DE. now apply Ctx.
        * apply DI1. eapply IE. eapply CE2. eapply Weak. 2: apply ; firstorder. firstorder. now apply Ctx.
        * apply DI2. eapply IE. eapply CE2. eapply Weak. 2: apply ; firstorder. firstorder. now apply Ctx.
    - apply CI.
      + apply II, II. eapply IE. eapply CE1. eapply Weak. 2: apply ; firstorder. firstorder. eapply IE.
        apply Ctx. right. now left. eapply IE. eapply CE2. eapply Weak. 2: apply ; firstorder. firstorder. now apply Ctx.
      + apply II, II. eapply IE. eapply CE2. eapply Weak. 2: apply ; firstorder. firstorder. eapply IE.
        apply Ctx. right. now left. eapply IE. eapply CE1. eapply Weak. 2: apply ; firstorder. firstorder. now apply Ctx.
  Qed.

  Lemma prv_equiv_quant_i op phi psi A :
    List.map (subst_form_i ↑) A ⊢ <--> A ⊢ (quant_indi op ) <--> (quant_indi op ).
  Proof.
    intros H. enough (A ⊢ ( <--> )[(var_indi (proj1_sig (find_bounded_indi_L (::::A))))..]i) as X.
    - destruct find_bounded_indi_L as [b Hb]; cbn in *. destruct op.
      + apply CI.
        * apply II. apply AllI_i. eapply nameless_equiv_all_i'; revgoals.
          -- eapply IE. eapply CE1. eapply Weak. 2: apply X. firstorder. now apply AllE_i, Ctx.
          -- apply bounded_indi_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. apply bounded_indi_up with (n:=b). lia. all: apply Hb; firstorder.
        * apply II. apply AllI_i. eapply nameless_equiv_all_i'; revgoals.
          -- eapply IE. eapply CE2. eapply Weak. 2: apply X. firstorder. now apply AllE_i, Ctx.
          -- apply bounded_indi_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. apply bounded_indi_up with (n:=b). lia. all: apply Hb; firstorder.
      + apply CI.
        * apply II. eapply ExE_i. now apply Ctx. eapply nameless_equiv_ex_i'; revgoals.
          -- eapply ExI_i. eapply IE. eapply CE1. eapply Weak. 2: apply X. firstorder. now apply Ctx.
          -- apply bounded_indi_up with (n:=b). lia. apply Hb. firstorder.
          -- cbn. apply bounded_indi_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. apply bounded_indi_up with (n:=b). lia. all: apply Hb; firstorder.
        * apply II. eapply ExE_i. now apply Ctx. eapply nameless_equiv_ex_i'; revgoals.
          -- eapply ExI_i. eapply IE. eapply CE2. eapply Weak. 2: apply X. firstorder. now apply Ctx.
          -- apply bounded_indi_up with (n:=b). lia. apply Hb. firstorder.
          -- cbn. apply bounded_indi_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. apply bounded_indi_up with (n:=b). lia. all: apply Hb; firstorder.
    - eapply subst_Weak_i in H. erewrite List.map_map, List.map_ext in H.
      2: intros; apply subst_form_shift_i. rewrite List.map_id in H. apply H. now intros [].
  Qed.

  Lemma prv_equiv_quant_f op phi psi A ar :
    List.map (subst_form_f (↑ ar)) A ⊢ <--> A ⊢ (quant_func op ar ) <--> (quant_func op ar ).
  Proof.
    intros H. enough (A ⊢ ( <--> )[(@var_func _ (proj1_sig (find_bounded_func_L ar (::::A))) ar)..]f) as X.
    - destruct find_bounded_func_L as [b Hb]; cbn in *. destruct op.
      + apply CI.
        * apply II. apply AllI_f. eapply nameless_equiv_all_f'; revgoals.
          -- eapply IE. eapply CE1. eapply Weak. 2: apply X. firstorder. now apply AllE_f, Ctx.
          -- apply bounded_func_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_func_up with (n:=b). lia. all: apply Hb; firstorder.
        * apply II. apply AllI_f. eapply nameless_equiv_all_f'; revgoals.
          -- eapply IE. eapply CE2. eapply Weak. 2: apply X. firstorder. now apply AllE_f, Ctx.
          -- apply bounded_func_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_func_up with (n:=b). lia. all: apply Hb; firstorder.
      + apply CI.
        * apply II. eapply ExE_f. now apply Ctx. eapply nameless_equiv_ex_f'; revgoals.
          -- eapply ExI_f. eapply IE. eapply CE1. eapply Weak. 2: apply X. firstorder. now apply Ctx.
          -- apply bounded_func_up with (n:=b). lia. apply Hb. firstorder.
          -- cbn. left. split. reflexivity. apply bounded_func_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_func_up with (n:=b). lia. all: apply Hb; firstorder.
        * apply II. eapply ExE_f. now apply Ctx. eapply nameless_equiv_ex_f'; revgoals.
          -- eapply ExI_f. eapply IE. eapply CE2. eapply Weak. 2: apply X. firstorder. now apply Ctx.
          -- apply bounded_func_up with (n:=b). lia. apply Hb. firstorder.
          -- cbn. left. split. reflexivity. apply bounded_func_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_func_up with (n:=b). lia. all: apply Hb; firstorder.
    - eapply subst_Weak_f in H. erewrite List.map_map, List.map_ext in H.
      2: intros; apply subst_form_shift_f. rewrite List.map_id in H. apply H.
  Qed.

  Lemma prv_equiv_quant_p op phi psi A ar :
    List.map (subst_form_p (↑ ar)) A ⊢ <--> A ⊢ (quant_pred op ar ) <--> (quant_pred op ar ).
  Proof.
    intros H. enough (A ⊢ ( <--> )[(@var_pred _ (proj1_sig (find_bounded_pred_L ar (::::A))) ar)..]p) as X.
    - destruct find_bounded_pred_L as [b Hb]; cbn in *. destruct op.
      + apply CI.
        * apply II. apply AllI_p. eapply nameless_equiv_all_p'; revgoals.
          -- eapply IE. eapply CE1. eapply Weak. 2: apply X. firstorder. now apply AllE_p, Ctx.
          -- apply bounded_pred_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_pred_up with (n:=b). lia. all: apply Hb; firstorder.
        * apply II. apply AllI_p. eapply nameless_equiv_all_p'; revgoals.
          -- eapply IE. eapply CE2. eapply Weak. 2: apply X. firstorder. now apply AllE_p, Ctx.
          -- apply bounded_pred_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_pred_up with (n:=b). lia. all: apply Hb; firstorder.
      + apply CI.
        * apply II. eapply ExE_p. now apply Ctx. eapply nameless_equiv_ex_p'; revgoals.
          -- eapply ExI_p. eapply IE. eapply CE1. eapply Weak. 2: apply X. firstorder. now apply Ctx.
          -- apply bounded_pred_up with (n:=b). lia. apply Hb. firstorder.
          -- cbn. left. split. reflexivity. apply bounded_pred_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_pred_up with (n:=b). lia. all: apply Hb; firstorder.
        * apply II. eapply ExE_p. now apply Ctx. eapply nameless_equiv_ex_p'; revgoals.
          -- eapply ExI_p. eapply IE. eapply CE2. eapply Weak. 2: apply X. firstorder. now apply Ctx.
          -- apply bounded_pred_up with (n:=b). lia. apply Hb. firstorder.
          -- cbn. left. split. reflexivity. apply bounded_pred_up with (n:=b). lia. apply Hb. firstorder.
          -- intros ? [|]. cbn. left. split. reflexivity. apply bounded_pred_up with (n:=b). lia. all: apply Hb; firstorder.
    - eapply subst_Weak_p in H. erewrite List.map_map, List.map_ext in H.
      2: intros; apply subst_form_shift_p. rewrite List.map_id in H. apply H.
  Qed.

  Lemma prv_equiv_subst_p phi psi sigma :
    List.nil ⊢ <--> List.nil ⊢ []p <--> []p.
  Proof.
    intros H. change (List.map (subst_form_p ) List.nil ⊢ ( <--> )[]p).
    apply subst_Weak_p, H.
  Qed.

  Lemma prv_equiv_symmetry A phi psi :
    A ⊢ <--> A ⊢ <--> .
  Proof.
    intros H. apply CI.
    - eapply II, IE. eapply CE2. eapply Weak. 2: apply H. firstorder. now apply Ctx.
    - eapply II, IE. eapply CE1. eapply Weak. 2: apply H. firstorder. now apply Ctx.
  Qed.

Provability of forall_n

  Lemma iter_up_i_le sigma n m :
    m < n iter up_i n m = var_indi m.
  Proof.
    induction n in m |-*; cbn; intros H.
    - lia.
    - destruct m; cbn. reflexivity. rewrite IHn. reflexivity. lia.
  Qed.

  Lemma iter_up_i_ge sigma n m :
    m n iter up_i n m = ( (m-n))[ x var_indi (n+x)]i.
  Proof.
    induction n in m |-*; cbn; intros H.
    - replace (m-0) with m by lia. destruct ; cbn. reflexivity. f_equal.
      erewrite Vector.map_ext, Vector.map_id. reflexivity. intros t. now setoid_rewrite subst_term_id_i.
    - destruct m; cbn; try lia. rewrite IHn. destruct ; cbn. reflexivity. f_equal. rewrite Vector.map_map.
      apply Vector.map_ext. intros t. now rewrite subst_term_comp_i. lia.
  Qed.

  Lemma prv_forall_n A n phi (v : vec term n) :
    A ⊢ forall_n n A ⊢ [ x if Compare_dec.lt_dec x n then nth_error (n - S x) v (i$0) else var_indi (x-n)]i.
  Proof.
    revert . induction n; intros H; cbn in *.
    - erewrite subst_ext_i. rewrite subst_id_i in H. apply H. intros n.
      replace (n-0) with n by lia. reflexivity.
    - eapply AllE_i with (t := Vector.hd v) in H. rewrite forall_n_subst_i in H.
      apply IHn with (v := Vector.tl v) in H. rewrite subst_comp_i in H. erewrite subst_ext_i. apply H.
      intros n'. destruct (PeanoNat.Nat.eq_dec n' n) as [|].
      + destruct Compare_dec.lt_dec; try lia. rewrite iter_up_i_ge; cbn. 2: lia. replace (n-n) with 0 by lia. cbn.
        setoid_rewrite subst_term_comp_i. cbn. erewrite subst_term_ext_i, subst_term_id_i.
        now destruct n; depelim v. intros x; cbn. destruct Compare_dec.lt_dec; try lia.
        now replace (n+x-n) with x by lia.
      + destruct Compare_dec.lt_dec.
        * rewrite iter_up_i_le. 2: lia. cbn. destruct Compare_dec.lt_dec; try lia.
          replace (n - n') with (S (n - S n')) by lia. now depelim v.
        * rewrite iter_up_i_ge. 2: lia. destruct (n'-n) eqn:; try lia; cbn.
          destruct Compare_dec.lt_dec; try lia. f_equal. lia.
  Qed.

  Lemma tabulate_var_indi_subst ar (v : vec term ar) :
    Vector.map (subst_term_i ( x if Compare_dec.lt_dec x ar then nth_error (ar - S x) v (var_indi 0) else var_indi (x-ar))) (tabulate ar var_indi) = v.
  Proof.
    rewrite map_tabulate; cbn. erewrite tabulate_ext. apply tabulate_nth. intros x H.
    destruct Compare_dec.lt_dec; try lia. reflexivity.
  Qed.

End Facts.

Incompleteness

The deduction system is not complete for Traski semantics

Require Import Incompleteness PA.

Section Incompleteness.

  Theorem InfinitarilyIncompleteI :
     T phi, decidable T validT T T ⊩i .
  Proof.
    intros complete. apply InfinitaryIncompleteness with (prv := @prv _ _ intu).
    - apply SoundnessIT.
    - apply complete.
  Qed.

  Theorem InfinitarilyIncompleteC :
    LEM T phi, decidable T validT T T ⊩c .
  Proof.
    intros lem complete. apply InfinitaryIncompleteness with (prv := @prv _ _ class).
    - intros. now apply SoundnessCT.
    - apply complete.
  Qed.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Context {L_Funcs : list syms}.
  Hypothesis enum_Funcs' : list_enumerator__T L_Funcs syms.

  Context {L_Preds : list preds}.
  Hypothesis enum_Preds' : list_enumerator__T L_Preds preds.

  Hypothesis eq_dec_Funcs : eq_dec syms.
  Hypothesis eq_dec_Preds : eq_dec preds.

  Theorem IncompleteI :
    MP ( A phi, valid A A ⊢i ) decidable .
  Proof.
    intros mp H. apply (Incompleteness (@prv _ _ intu)).
    - apply SoundnessI.
    - apply H.
    - eapply prv_enumerable. apply enum_Funcs'. apply enum_Preds'.
      apply eq_dec_Funcs. apply eq_dec_Preds.
    - apply eq_dec_Funcs.
    - apply eq_dec_Preds.
    - apply mp.
  Qed.

  Theorem IncompleteC :
    LEM ( A phi, valid A A ⊢c ) decidable .
  Proof.
    intros lem H. apply (Incompleteness (@prv _ _ class)).
    - intros. now apply SoundnessC.
    - apply H.
    - eapply prv_enumerable. apply enum_Funcs'. apply enum_Preds'.
      apply eq_dec_Funcs. apply eq_dec_Preds.
    - apply eq_dec_Funcs.
    - apply eq_dec_Preds.
    - intros f . specialize (lem (tsat f)). tauto.
  Qed.

End Incompleteness.

Henkin Soundness


Require Import Henkin.

Section Henkin.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Lemma comprehension_form_subst_i ar phi sigma :
    (comprehension_form ar )[]i = comprehension_form ar ([iter up_i ar ]i).
  Proof.
    unfold comprehension_form. cbn. rewrite forall_n_subst_i. cbn. erewrite subst_switch_i_p, map_tabulate, tabulate_ext.
    reflexivity. induction ar; intros m H; cbn. lia. destruct m; cbn. reflexivity.
    setoid_rewrite IHar. reflexivity. lia.
  Qed.

  Lemma funcfreeTerm_subst_i t sigma :
    ( n, funcfreeTerm ( n)) funcfreeTerm t funcfreeTerm (t[]i).
  Proof.
    intros . induction t; cbn. apply . easy.
    eapply Forall_map, Forall_ext_Forall. apply IH. apply .
  Qed.

  Lemma funcfree_subst_i phi sigma :
    ( n, funcfreeTerm ( n)) funcfree funcfree([]i).
  Proof.
    induction in |-*; intros H F; firstorder.
    - apply Forall_map. apply Forall_in. intros t . apply funcfreeTerm_subst_i.
      apply H. eapply Forall_in in F. apply F. easy.
    - apply IHphi; trivial. intros []; cbn; trivial. specialize (H n).
      destruct ; cbn in *. easy. destruct f. easy.
      apply Forall_map. apply Forall_in. intros t . apply funcfreeTerm_subst_i.
      now intros ?. eapply Forall_in in H. apply H. easy.
  Qed.

  Section Model.

    Variable D : Type.
    Context {I : interp D}.
    Variable funcIncluded : ar, (vec D ar D) Prop.
    Variable predIncluded : ar, (vec D ar Prop) Prop.

    Lemma forall_n_to_vec_Henkin rho n phi :
      Henkin.sat funcIncluded predIncluded (forall_n n ) v : vec D n, Henkin.sat funcIncluded predIncluded ⟨ VectorLib.fold_left scons (get_indi ) v, get_func , get_pred ⟩ .
    Proof.
      enough ( rho_i rho_f rho_p, Henkin.sat funcIncluded predIncluded ⟨rho_i, rho_f, rho_p⟩ (forall_n n ) v : vec D n, Henkin.sat funcIncluded predIncluded ⟨ VectorLib.fold_left scons rho_i v, rho_f, rho_p ⟩ ) by now destruct .
      intros. clear . revert rho_i. induction n; intros rho_i; cbn.
      - split.
        + intros H v. now dependent elimination v.
        + intros H. apply (H (Vector.nil _)).
      - split.
        + intros H v. dependent elimination v. cbn. apply IHn, H.
        + intros H d. apply IHn. intros v. apply (H (Vector.cons _ d _ v)).
    Qed.

    Lemma comprehension_form_correct ar phi rho :
      Henkin.sat funcIncluded predIncluded (comprehension_form ar ) P, predIncluded ar P v, P v Henkin.sat funcIncluded predIncluded ⟨ VectorLib.fold_left scons (get_indi ) v, get_func , get_pred ⟩ .
    Proof.
      split; cbn.
      - intros [P [ ]]. exists P. split. exact . intros v.
        apply forall_n_to_vec_Henkin with (v := v) in . cbn in .
        rewrite nat_eq_dec_same, eval_tabulate in . setoid_rewrite sat_comp_p in .
        cbn in . erewrite sat_ext in . apply . split. reflexivity. intros ar' v'.
        split. reflexivity. cbn. unfold shift, shift_p. destruct PeanoNat.Nat.eq_dec as [|]; cbn.
        now rewrite nat_eq_dec_same. now destruct n; cbn; destruct PeanoNat.Nat.eq_dec; try lia.
      - intros [P [ ]]. exists P. split. exact . apply forall_n_to_vec_Henkin.
        intros v. cbn. erewrite nat_eq_dec_same, eval_tabulate, sat_comp_p, sat_ext.
        apply . cbn. split. reflexivity. intros ar' v'. split. reflexivity.
        cbn. unfold shift, shift_p. destruct PeanoNat.Nat.eq_dec as [|]; cbn.
        now rewrite nat_eq_dec_same. now destruct n; cbn; destruct PeanoNat.Nat.eq_dec; try lia.
    Qed.

  End Model.

  Lemma HenkinSoundnessI A phi :
    A ⊢i Henkin.valid A .
  Proof.
    remember intu as p.
    induction 1; intros D I funcs preds HI HCompr Hrho HA.
    - intros . apply IHprv; trivial. intros [|]; firstorder.
    - apply ; trivial. apply ; trivial.
    - exfalso. eapply IHprv; try easy. apply HI. apply HCompr.
    - firstorder.
    - split. now apply . now apply .
    - now apply IHprv.
    - now apply IHprv.
    - left. now apply IHprv.
    - right. now apply IHprv.
    - edestruct ; trivial. apply HI. apply HCompr. apply Hrho. apply HA.
      + apply ; trivial. intros x [|]; auto.
      + apply ; trivial. intros x [|]; auto.
    - discriminate.
    - intros x. apply IHprv; trivial. intros [ [ ]]%in_map_iff.
      apply sat_comp_i. now destruct ; apply HA.
    - intros f Hf. apply IHprv; trivial. now apply henkin_env_cons_f.
      intros [ [ ]]%in_map_iff.
      apply sat_comp_f. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
      now rewrite eval_function_subst_cons_shift_f.
    - intros P HP. apply IHprv; trivial. now apply henkin_env_cons_p.
      intros [ [ ]]%in_map_iff.
      apply sat_comp_p. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
      now rewrite eval_predicate_subst_cons_shift_p.
    - eapply sat_comp_i, sat_ext. 2: apply (IHprv Heqp D I funcs preds HI HCompr Hrho HA (eval _ t)).
      split; try easy. now destruct n.
    - eapply sat_comp_f, sat_ext. 2: eapply (IHprv Heqp D I funcs preds HI HCompr Hrho HA (eval_function _ f)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
      eapply eval_function_included. apply HI. apply Hrho.
    - eapply sat_comp_p, sat_ext. 2: eapply (IHprv Heqp D I funcs preds HI HCompr Hrho HA (eval_predicate _ P)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
      eapply eval_predicate_included. apply HI. apply Hrho.
    - exists (eval _ t). eapply sat_ext. 2: apply sat_comp_i, IHprv, HA; try easy.
      split; try easy. now destruct n.
    - exists (eval_function _ f). eexists.
      + eapply eval_function_included. apply HI. apply Hrho.
      + eapply sat_ext. 2: apply sat_comp_f, IHprv, HA; try easy. split; try easy.
        intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - exists (eval_predicate _ P). eexists.
      + eapply eval_predicate_included. apply HI. apply Hrho.
      + eapply sat_ext. 2: apply sat_comp_p, IHprv, HA; try easy. split; try easy.
        intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - edestruct as [x Hx]; eauto.
      specialize ( Heqp D I funcs preds HI HCompr ⟨x .: get_indi , get_func , get_pred ⟩).
      apply sat_comp_i in ; try easy. destruct ; apply .
      intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hx.
      apply sat_comp_i. destruct ; apply H'.
    - edestruct as [f [Hf' Hf]]; eauto.
      specialize ( Heqp D I funcs preds HI HCompr ⟨get_indi , f .: get_func , get_pred ⟩).
      apply sat_comp_f in ; try easy.
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
      + now apply henkin_env_cons_f.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hf.
        apply sat_comp_f. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
    - edestruct as [P [HP' HP]]; eauto.
      specialize ( Heqp D I funcs preds HI HCompr ⟨get_indi , get_func , P .: get_pred ⟩).
      apply sat_comp_p in ; try easy.
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
      + now apply henkin_env_cons_p.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact HP.
        apply sat_comp_p. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
    - apply HCompr. apply Hrho. easy.
  Qed.

  Lemma HenkinSoundnessC A phi :
    LEM A ⊢c Henkin.valid A .
  Proof.
    intros lem. induction 1; intros D I funcs preds HI HCompr Hrho HA.
    - intros . apply IHprv; trivial. intros [|]; firstorder.
    - apply ; trivial. apply ; trivial.
    - exfalso. eapply IHprv; try easy. apply HI. apply HCompr.
    - firstorder.
    - split. now apply . now apply .
    - now apply IHprv.
    - now apply IHprv.
    - left. now apply IHprv.
    - right. now apply IHprv.
    - edestruct ; trivial. apply HI. apply HCompr. apply Hrho. apply HA.
      + apply ; trivial. intros x [|]; auto.
      + apply ; trivial. intros x [|]; auto.
    - specialize (lem (sat funcs preds )). cbn. tauto.
    - intros x. apply IHprv; trivial. intros [ [ ]]%in_map_iff.
      apply sat_comp_i. now destruct ; apply HA.
    - intros f Hf. apply IHprv; trivial. now apply henkin_env_cons_f.
      intros [ [ ]]%in_map_iff.
      apply sat_comp_f. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
      now rewrite eval_function_subst_cons_shift_f.
    - intros P HP. apply IHprv; trivial. now apply henkin_env_cons_p.
      intros [ [ ]]%in_map_iff.
      apply sat_comp_p. cbn. eapply sat_ext. 2: apply HA, .
      split; try easy; split; try easy; cbn.
      replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
      now rewrite eval_predicate_subst_cons_shift_p.
    - eapply sat_comp_i, sat_ext. 2: apply (IHprv D I funcs preds HI HCompr Hrho HA (eval _ t)).
      split; try easy. now destruct n.
    - eapply sat_comp_f, sat_ext. 2: eapply (IHprv D I funcs preds HI HCompr Hrho HA (eval_function _ f)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
      eapply eval_function_included. apply HI. apply Hrho.
    - eapply sat_comp_p, sat_ext. 2: eapply (IHprv D I funcs preds HI HCompr Hrho HA (eval_predicate _ P)).
      split; try easy. intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
      eapply eval_predicate_included. apply HI. apply Hrho.
    - exists (eval _ t). eapply sat_ext. 2: apply sat_comp_i, IHprv, HA; try easy.
      split; try easy. now destruct n.
    - exists (eval_function _ f). eexists.
      + eapply eval_function_included. apply HI. apply Hrho.
      + eapply sat_ext. 2: apply sat_comp_f, IHprv, HA; try easy. split; try easy.
        intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - exists (eval_predicate _ P). eexists.
      + eapply eval_predicate_included. apply HI. apply Hrho.
      + eapply sat_ext. 2: apply sat_comp_p, IHprv, HA; try easy. split; try easy.
        intros; destruct n; cbn; now destruct PeanoNat.Nat.eq_dec as [|].
    - edestruct as [x Hx]; eauto.
      specialize ( D I funcs preds HI HCompr ⟨x .: get_indi , get_func , get_pred ⟩).
      apply sat_comp_i in ; try easy. destruct ; apply .
      intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hx.
      apply sat_comp_i. destruct ; apply H'.
    - edestruct as [f [Hf' Hf]]; eauto.
      specialize ( D I funcs preds HI HCompr ⟨get_indi , f .: get_func , get_pred ⟩).
      apply sat_comp_f in ; try easy.
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
      + now apply henkin_env_cons_f.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact Hf.
        apply sat_comp_f. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_func n )[@shift _ shift_f ar]f) by reflexivity.
        now rewrite eval_function_subst_cons_shift_f.
    - edestruct as [P [HP' HP]]; eauto.
      specialize ( D I funcs preds HI HCompr ⟨get_indi , get_func , P .: get_pred ⟩).
      apply sat_comp_p in ; try easy.
      + eapply sat_ext. 2: apply . split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
      + now apply henkin_env_cons_p.
      + intros . intros [|[ [ H'%HA]] % in_map_iff]. exact HP.
        apply sat_comp_p. eapply sat_ext. 2: apply H'.
        split; try easy; split; try easy; cbn.
        replace (↑ ar n ) with ((var_pred n )[@shift _ shift_p ar]p) by reflexivity.
        now rewrite eval_predicate_subst_cons_shift_p.
    - apply HCompr. apply Hrho. easy.
  Qed.

  Corollary HenkinSoundnessIT T phi :
    T ⊩i Henkin.validT T .
  Proof.
    intros [A [HA ]] D I funcs preds HI HC Hrho HT.
    eapply HenkinSoundnessI; try eassumption.
    intros . apply HT, HA, .
  Qed.

  Corollary HenkinSoundnessCT T phi :
    LEM T ⊩c Henkin.validT T .
  Proof.
    intros lem [A [HA ]] D I funcs preds HI HC Hrho HT.
    eapply HenkinSoundnessC; try eassumption.
    intros . apply HT, HA, .
  Qed.

End Henkin.