Reduction to FOL


Require Import FOL SOL FullSyntax Tarski Henkin Deduction.
Require Import Vector VectorLib Util.

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

Require Import Enumerable Decidable.

Import VectorNotations.
Import SubstNotations.

Definition toFOLBinop b := match b with
  | FullSyntax.Conj FOL.Conj
  | FullSyntax.Disj FOL.Disj
  | FullSyntax.Impl FOL.Impl
end.

Definition toSOLBinop b := match b with
  | FOL.Conj FullSyntax.Conj
  | FOL.Disj FullSyntax.Disj
  | FOL.Impl FullSyntax.Impl
end.

Definition toSOLQuantop b := match b with
  | FOL.All FullSyntax.All
  | FOL.Ex FullSyntax.Ex
end.

Definition toFOLQuantop b := match b with
  | FullSyntax.All FOL.All
  | FullSyntax.Ex FOL.Ex
end.

Lemma toSOLBinop_toFOLBinop b :
  toSOLBinop (toFOLBinop b) = b.
Proof.
  now destruct b.
Qed.


Section Signature.

  Context {Σf2 : SOL.funcs_signature}.
  Context {Σp2 : SOL.preds_signature}.

  (* Add symbols for predicate application to the SOL signature.  *)

  Inductive FOLSyms :=
    | NormalSym : syms FOLSyms.

  Inductive FOLPreds :=
    | NormalPred : preds FOLPreds
    | PredApp : FOLPreds.

  Instance Σf1 : FOL.funcs_signature := {|
    FOL.syms := FOLSyms ;
    FOL.ar_syms f := match f with NormalSym f SOL.ar_syms f end
  |}.

  Instance Σp1 : FOL.preds_signature := {|
    FOL.preds := FOLPreds ;
    FOL.ar_preds P := match P with NormalPred P SOL.ar_preds P | PredApp ar S ar end
  |}.

The extended signatures preserve discreteness and enumerablility

  Lemma Sigma_f1_eq_dec :
    eq_dec Σf2 eq_dec Σf1.
  Proof.
    intros H [x] [y]. enough (dec (x = y)) as [|].
    now left. right. congruence. apply H.
  Qed.


  Lemma Sigma_p1_eq_dec :
    eq_dec Σp2 eq_dec Σp1.
  Proof.
    intros H [p|n] [p'|n'].
    - enough (dec (p = p')) as [|]. now left. right. congruence. apply H.
    - right. congruence.
    - right. congruence.
    - decide (n = n') as [|]. now left. right. congruence.
  Qed.


  Lemma Sigma_f1_enumerable :
    enumerable__T Σf2 enumerable__T Σf1.
  Proof.
    intros [f Hf]. exists ( n match f n with Some x Some (NormalSym x) | None None end).
    intros [x]. destruct (Hf x) as [n H]. exists n. now rewrite H.
  Qed.


  Lemma Sigma_p1_enumerable :
    enumerable__T Σp2 enumerable__T Σp1.
  Proof.
    intros [f Hf].
    exists ( n match n with
                      | 0 match f ( n) with Some x Some (NormalPred x) | None None end
                      | _ Some (PredApp ( n))
                    end).
    intros [x|n].
    - destruct (Hf x) as [n H]. exists (embed (0,n)). now rewrite pi1_correct, pi2_correct, H.
    - exists (embed (1,n)). now rewrite pi1_correct, pi2_correct.
  Qed.


Notations for first-order syntax

  Notation "⊥'" := FOL.falsity.
  Notation "A ∧' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Conj A B) (at level 41).
  Notation "A ∨' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Disj A B) (at level 42).
  Notation "A '-'' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Impl A B) (at level 43, right associativity).
  Notation "A ''' B" := ((A -->' B) ∧' (B -->' A)) (at level 44, right associativity).
  Notation "∀' Phi" := (@FOL.quant Σf1 Σp1 FOL.full_operators _ FOL.All Phi) (at level 50).
  Notation "∃' Phi" := (@FOL.quant Σf1 Σp1 FOL.full_operators _ FOL.Ex Phi) (at level 50).

  Notation "phi `[ sigma ]" := (FOL.subst_form ) (at level 7, left associativity, format "phi '/' `[ sigma ]") : subst_scope.
  Notation "f >>' g" := (FOL.funcomp g f) (at level 50) : subst_scope.
  Notation "s '..''" := (FOL.scons s FOL.var) (at level 4, format "s ..'") : subst_scope.
  Notation "↑'" := (S >>' FOL.var) : subst_scope.

  Notation "A ⊢1 phi" := (FOL.prv _ A ) (at level 61).
  Notation "A ⊢2 phi" := (Deduction.prv A ) (at level 61).

  Lemma FOL_term_ind (p : FOL.term Prop) :
    ( x, p (FOL.var x)) ( F v (IH : VectorLib.Forall p v), p (FOL.func F v)) t, p t.
  Proof.
    intros . fix F 1. intros [n|f v].
    - apply .
    - apply . induction v. easy. split. apply F. apply IHv.
  Qed.


Definition of Translation Function

The idea is to use functions pos_i, pos_f and pos_p that given a position in the SOL environment tell us the positition of the same object in the FOL environment. Quantifiers update those mappings by adding 0 the the matching kind and shiftig the other two.

  Definition pcons (pos : ) : :=
     n match n with 0 0 | S n S (pos n) end.

  Definition pcons' (ar : ) (pos : ) : :=
     n ar' match n with
      | 0 if PeanoNat.Nat.eq_dec ar ar' then 0 else S (pos 0 ar')
      | S n if PeanoNat.Nat.eq_dec ar ar' then S (pos n ar') else S (pos (S n) ar') end.

  Definition pshift (pos : ) : := n S (pos n).
  Definition pshift' (pos : ) : := n ar S (pos n ar).

  Fixpoint toFOLTerm (pos_i : ) (t : SOL.term) : FOL.term := match t with
    | SOL.var_indi x FOL.var (pos_i x)
    | SOL.func (var_func x ar) v FOL.var 0
    | SOL.func (sym f) v FOL.func (NormalSym f) (Vector.map (toFOLTerm pos_i) v)
  end.

  Fixpoint toFOLForm (pos_i : ) (pos_p : ) (phi : SOL.form) : FOL.form := match with
    | SOL.fal FOL.falsity
    | SOL.atom (pred P) v FOL.atom (NormalPred P) (Vector.map (toFOLTerm pos_i) v)
    | SOL.atom (var_pred x ar) v FOL.atom (PredApp ar) (FOL.var (pos_p x ar) :: Vector.map (toFOLTerm pos_i) v)
    | SOL.bin op FOL.bin (toFOLBinop op) (toFOLForm pos_i pos_p ) (toFOLForm pos_i pos_p )
    | SOL.quant_indi op FOL.quant (toFOLQuantop op) (toFOLForm (pcons pos_i) (pshift' pos_p) )
    | SOL.quant_func op ar FOL.falsity
    | SOL.quant_pred op ar FOL.quant (toFOLQuantop op) (toFOLForm (pshift pos_i) (pcons' ar pos_p) )
  end.

  Definition initial_pos_i n := embed (0, n).
  Definition initial_pos_p n ar := embed (1, embed (n, ar)).

  Definition toFOLForm' (phi : SOL.form) := toFOLForm initial_pos_i initial_pos_p .

  Lemma toFOLTerm_ext_i pos_i pos_i' t :
    ( n, bounded_indi_term n t pos_i n = pos_i' n)
     toFOLTerm pos_i t = toFOLTerm pos_i' t.
  Proof.
    intros Hi. induction t; cbn.
    - rewrite Hi. reflexivity. cbn; lia.
    - reflexivity.
    - f_equal. apply map_ext_in. intros t H. eapply Forall_in in IH. apply IH.
      intros n . apply Hi. intros . apply . eapply Forall_in in . apply . all: easy.
  Qed.


  Lemma toFOLForm_ext_i pos_i pos_i' pos_p phi :
    ( n, bounded_indi n pos_i n = pos_i' n)
     toFOLForm pos_i pos_p = toFOLForm pos_i' pos_p .
  Proof.
    induction in pos_i, pos_i', pos_p |-*; cbn; intros Hi.
    - reflexivity.
    - destruct p; cbn; f_equal. f_equal. all: apply map_ext_in; intros t H;
      apply toFOLTerm_ext_i; intros n' ; apply Hi; intros ; apply ;
      eapply Forall_in in ; try apply ; easy.
    - erewrite , ; firstorder.
    - f_equal. apply IHphi. intros [] H; cbn. reflexivity. now rewrite Hi.
    - reflexivity.
    - f_equal. apply IHphi. intros n' H. unfold pshift. now rewrite Hi.
  Qed.


  Lemma toFOLForm_ext_p pos_i pos_p pos_p' phi :
    ( n ar, bounded_pred ar n pos_p n ar = pos_p' n ar)
     toFOLForm pos_i pos_p = toFOLForm pos_i pos_p' .
  Proof.
    induction in pos_i, pos_p, pos_p' |-*; intros Hp; cbn.
    - reflexivity.
    - destruct p; f_equal. rewrite Hp. reflexivity. cbn; lia.
    - erewrite , ; firstorder.
    - erewrite IHphi. reflexivity. intros n ar H. unfold pshift'. now rewrite Hp.
    - reflexivity.
    - erewrite IHphi. reflexivity. intros [] ar H; cbn; destruct PeanoNat.Nat.eq_dec as [|].
      reflexivity. all: rewrite Hp; try reflexivity; cbn; now intros [[]|[]]; try lia.
  Qed.


  Definition closed phi := bounded_indi 0 ( ar, bounded_func ar 0 ) ( ar, bounded_pred ar 0 ).

  Lemma toFOLForm_closed_ext pos_i pos_p pos_i' pos_p' phi :
    closed toFOLForm pos_i pos_p = toFOLForm pos_i' pos_p' .
  Proof.
    intros C. erewrite toFOLForm_ext_p, toFOLForm_ext_i. reflexivity.
    - intros n H. exfalso. apply H. eapply bounded_indi_up. 2: apply C. lia.
    - intros n ar H. exfalso. apply H. eapply bounded_pred_up. 2: apply C. lia.
  Qed.


  Lemma comprehension_form_funcfree ar phi :
    funcfree funcfree (comprehension_form ar ).
  Proof.
    intros H. apply forall_n_funcfree. repeat split; cbn.
    1,4: induction ar; firstorder. all: now apply funcfree_subst_p.
  Qed.


  Definition C := phi ar psi, funcfree = close All (comprehension_form ar ).
  Definition toFOLTheory (T : SOL.form Prop) := phi phi', = toFOLForm' T .

  Lemma toFOLTheory_enumerable T :
    enumerable T enumerable (toFOLTheory T).
  Proof.
    intros [f Hf]. exists ( n match f n with Some Some (toFOLForm' ) | None None end).
    intros . split.
    - intros [ [ H]]. apply Hf in H as [n H]. exists n. now rewrite H.
    - intros [n H]. destruct f eqn:.
      + inversion H. eexists. split. reflexivity. apply Hf. now exists n.
      + easy.
  Qed.


  Lemma C_enumerable :
    enumerable__T Σf2 enumerable__T Σp2 enumerable C.
  Proof.
    intros . unfold C. destruct form_enumerable as [f Hf]; trivial.
    apply enumT_binop. apply enumT_quantop.
    exists ( n match f ( n) with Some if funcfree_dec then Some (close All (comprehension_form ( n) )) else None | None None end).
    intros . split.
    - intros [ar [ [ ]]]. destruct (Hf ) as [n ].
      exists (embed (n, ar)). rewrite pi1_correct, pi2_correct, , .
      now destruct funcfree_dec.
    - intros [n ]. destruct f eqn:; try easy. destruct funcfree_dec; try easy.
      inversion . eauto.
  Qed.


Semantic Reduction

Translate Henkin Model to First-Order Model.


  Section HenkinModel_To_FOModel.

    Variable : Type.

    Context {I2 : Tarski.interp }.

    Variable funcs : ar, (vec ar ) Prop.
    Variable preds : ar, (vec ar Prop) Prop.

    Inductive :=
      | fromIndi :
      | fromPred : ar (P : vec ar Prop), preds ar P .

    Hypothesis D2_inhabited : .
    Hypothesis funcs_inhabited : ar, { f | funcs ar f }.
    Hypothesis preds_inhabited : ar, { P | preds ar P }.

    Definition error_i := D2_inhabited.
    Definition error_p ar := proj1_sig (preds_inhabited ar).

    Lemma error_p_included ar :
      preds ar (error_p ar).
    Proof.
      unfold error_p. now destruct preds_inhabited.
    Qed.


    Definition toIndi (d1 : ) := match with fromIndi | _ error_i end.

    Definition toPred ar (d1 : ) := match with
      | fromPred ar' _ match PeanoNat.Nat.eq_dec ar ar' with
                            | left e match eq_sym e in _ = ar return vec ar Prop with eq_refl end
                            | right _ error_p ar
                          end
      | _ error_p ar
    end.

    Instance I1 : FOL.interp := {|
      FOL.i_func f := match f with
          | NormalSym f v fromIndi (Tarski.i_f _ f (Vector.map toIndi v))
        end ;
      FOL.i_atom P := match P with
          | NormalPred P v Tarski.i_P _ P (Vector.map ( d match d with fromIndi d d | _ error_i end) v)
          | PredApp ar v match Vector.hd v with
                                    | fromPred ar' P _ match PeanoNat.Nat.eq_dec ar ar' with
                                                          | left e P match e in _ = ar' return vec _ ar' with eq_refl Vector.map toIndi (Vector.tl v) end
                                                          | right _ error_p ar (Vector.map toIndi (Vector.tl v))
                                                        end
                                    | _ error_p ar (Vector.map toIndi (Vector.tl v))
                                  end
          end
    |}.

    Lemma toFOLTerm_correct_2To1 rho1 rho2 pos_i t :
      funcfreeTerm t
       ( n, toIndi ( (pos_i n)) = get_indi n)
       toIndi (FOL.eval (toFOLTerm pos_i t)) = Tarski.eval t.
    Proof.
      intros F Hi. induction t; cbn.
      - apply Hi.
      - now exfalso.
      - f_equal. f_equal. rewrite !map_map. eapply map_ext_forall, Forall_ext_Forall.
        apply IH. apply F.
    Qed.


    Ltac destruct_eq_dec :=
      repeat (cbn; try rewrite nat_eq_dec_same; cbn; try destruct PeanoNat.Nat.eq_dec as [|]; try destruct PeanoNat.Nat.eq_dec as [|]).

    Lemma toFOLForm_correct_2To1 rho1 rho2 pos_i pos_p phi :
      funcfree
       ( n, toIndi ( (pos_i n)) = get_indi n)
       ( n ar, toPred ar ( (pos_p n ar)) = get_pred n ar)
       FOL.sat (toFOLForm pos_i pos_p ) Henkin.sat funcs preds .
    Proof.
      revert pos_i pos_p. induction ; intros pos_i pos_p F Hi Hp; cbn.
      - reflexivity.
      - destruct p; cbn.
        + rewrite Hp.
          assert (map toIndi (map (FOL.eval ) (map (toFOLTerm pos_i) v)) = map (eval ) v) as . {
            rewrite !map_map. eapply map_ext_forall, Forall_in.
            intros t H. erewrite toFOLTerm_correct_2To1. reflexivity.
            eapply Forall_in in F. apply F. easy. apply Hi. }
          destruct ( (pos_p n ar)); try easy. cbn. now destruct PeanoNat.Nat.eq_dec as [|].
        + assert ( x y, x = y x y) as X by now intros x y . apply X; clear X.
          f_equal. rewrite !map_map. eapply map_ext, Forall2_identical, Forall_in.
          intros t H. rewrite (toFOLTerm_correct_2To1 _ pos_i). now destruct FOL.eval.
          eapply Forall_in in F. apply F. easy. apply Hi.
      - specialize ( pos_i pos_p ltac:(firstorder) ltac:(firstorder) ltac:(firstorder));
        specialize ( pos_i pos_p ltac:(firstorder) ltac:(firstorder) ltac:(firstorder)).
        destruct b; cbn; tauto.
      - destruct q; cbn; split.
        + intros H d. eapply IHphi. 4: apply (H (fromIndi d)). easy. intros []. all: firstorder.
        + intros H [d|ar P ?].
          * eapply IHphi. 4: apply (H d). easy. intros []. all: firstorder.
          * eapply IHphi. 4: apply (H error_i). easy. intros []. all: firstorder.
        + intros [[d|ar P ?] H].
          * exists d. eapply IHphi. 4: apply H. easy. intros []. all: firstorder.
          * exists error_i. eapply IHphi. 4: apply H. easy. intros []. all: firstorder.
        + intros [d H]. exists (fromIndi d). eapply IHphi. 4: apply H. easy. intros []. all: firstorder.
      - now exfalso.
      - destruct q; cbn; split.
        + intros H P HP'. eapply IHphi. 4: apply (H (fromPred _ P HP')). 3: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros H [d|ar P ?].
          * eapply IHphi. 4: apply (H (error_p _)), error_p_included. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
          * destruct (PeanoNat.Nat.eq_dec n ar) as [|].
            -- eapply IHphi. 4: apply (H P). 3: intros [] ar'; destruct_eq_dec. all: firstorder.
            -- eapply IHphi. 4: apply (H (error_p _)), error_p_included. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros [[d|ar P HP'] H].
          * exists (error_p _), (error_p_included _). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
          * destruct (PeanoNat.Nat.eq_dec n ar) as [|].
            -- exists P, HP'. eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
            -- exists (error_p _), (error_p_included _). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros [P [HP' H]]. exists (fromPred _ P HP'). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
    Qed.


    Definition toFOLEnv rho2 (H : henkin_env funcs preds ) := n match unembed n with
      | (0, n) fromIndi (get_indi n)
      | (_, x) fromPred _ (get_pred ( x) ( x)) ltac:(apply H)
    end.

    Lemma toFOLEnv_correct_i rho2 (H : henkin_env funcs preds ) :
       n, toIndi (toFOLEnv H (initial_pos_i n)) = get_indi n.
    Proof.
      intros n. unfold toFOLEnv, initial_pos_i. now rewrite unembed_embed.
    Qed.


    Lemma toFOLEnv_correct_p rho2 (H : henkin_env funcs preds ) :
       n ar, toPred ar (toFOLEnv H (initial_pos_p n ar)) = get_pred n ar.
    Proof.
      intros n ar. unfold toFOLEnv, initial_pos_p.
      rewrite unembed_embed, pi1_correct, pi2_correct.
      destruct H. cbn. now rewrite nat_eq_dec_same.
    Qed.


    Lemma toFOLForm_correct_2To1' rho2 (H : henkin_env funcs preds ) phi :
      funcfree FOL.sat (toFOLEnv H) (toFOLForm' ) Henkin.sat funcs preds .
    Proof.
      intros F. apply toFOLForm_correct_2To1. apply F.
      apply toFOLEnv_correct_i. apply toFOLEnv_correct_p.
    Qed.


  End HenkinModel_To_FOModel.

Translate First-Order Model to Henkin Model.


  Section FOModel_To_HenkinModel.

    Variable : Type.
    Context {I1 : FOL.interp }.

    Definition := .

    Definition funcs ar (f : vec ar ) := True.

    Definition preds ar (P : vec ar Prop) :=
       d : , v, P v i_atom (P:=PredApp ar) (d::v).

    Instance I2 : Tarski.interp := {|
      Tarski.i_f f v := i_func (f:=NormalSym f) v ;
      Tarski.i_P P v := i_atom (P:=NormalPred P) v
    |}.

    Lemma toFOLTerm_correct_1To2 rho1 rho2 pos_i t :
      funcfreeTerm t
       ( n, get_indi n = (pos_i n))
       Tarski.eval t = FOL.eval (toFOLTerm pos_i t).
    Proof.
      intros F Hi. induction t; cbn.
      - apply Hi.
      - now exfalso.
      - f_equal. rewrite map_map. eapply map_ext_forall, Forall_ext_Forall.
        apply IH. apply F.
    Qed.


    Ltac destruct_eq_dec :=
      repeat (cbn; try rewrite nat_eq_dec_same; cbn; try destruct PeanoNat.Nat.eq_dec as [|]; try destruct PeanoNat.Nat.eq_dec as [|]).

    Lemma toFOLForm_correct_1To2 rho1 rho2 pos_i pos_p phi :
      funcfree
       ( n, get_indi n = (pos_i n))
       ( n ar, v, get_pred n ar v i_atom (P:=PredApp ar) ( (pos_p n ar) :: v))
       FOL.sat (toFOLForm pos_i pos_p ) Henkin.sat funcs preds .
    Proof.
      revert pos_i pos_p. induction ; intros pos_i pos_p F Hi Hp; cbn.
      - reflexivity.
      - destruct p; cbn.
        + rewrite Hp. assert ( x y, x = y x y) as X by now intros x y . apply X; clear X.
          f_equal. rewrite !map_map. eapply map_ext_forall, Forall_in. intros t H.
          erewrite toFOLTerm_correct_1To2. reflexivity.
          eapply Forall_in in F. apply F. easy. apply Hi.
        + assert ( x y, x = y x y) as X by now intros x y . apply X; clear X.
          f_equal. rewrite !map_map. eapply map_ext_forall, Forall_in. intros t H.
          erewrite toFOLTerm_correct_1To2. reflexivity.
          eapply Forall_in in F. apply F. easy. apply Hi.
      - destruct F as [ ]. specialize ( pos_i pos_p Hi Hp);
        specialize ( pos_i pos_p Hi Hp). destruct b; cbn; tauto.
      - destruct q; cbn; split.
        + intros H d. eapply IHphi. 4: apply (H d). easy. intros []. all: trivial; apply Hi.
        + intros H d. eapply IHphi. 4: apply (H d). easy. intros []. all: trivial; apply Hi.
        + intros [d H]. exists d. eapply IHphi. 4: apply H. easy. intros []. all: trivial; apply Hi.
        + intros [d H]. exists d. eapply IHphi. 4: apply H. easy. intros []. all: trivial; apply Hi.
      - now exfalso.
      - destruct q; cbn; split.
          + intros H P [d Hd]. eapply IHphi. 4: apply (H d). 3: intros [] ar'; destruct_eq_dec. all: try easy.
          + intros H d. eapply IHphi. 4: apply (H ( v @i_atom Σf1 Σp1 _ _ (PredApp n) (d::v))).
            4: now exists d. 3: intros [] ar'; cbn; destruct_eq_dec. all: easy.
          + intros [d H]. exists ( v @i_atom Σf1 Σp1 _ _ (PredApp n) (d::v)).
            eexists. now exists d. eapply IHphi. 4: apply H. 3: intros [] ar'; cbn; destruct_eq_dec. all: easy.
          + intros [f [[d Hd] H]]. exists d. eapply IHphi. 4: apply H. 3: intros [] ar'; cbn; destruct_eq_dec. all: easy.
    Qed.


    Definition toSOLEnv rho1 :=
       n (initial_pos_i n),
         _ ar v 0,
         n ar v i_atom (P:=PredApp ar) ( (initial_pos_p n ar) :: v) .

    Lemma toSOLEnv_henkin_env rho1 :
      henkin_env funcs preds (toSOLEnv ).
    Proof.
      intros n ar. split. easy. now exists ( (initial_pos_p n ar)).
    Qed.


    Lemma toFOLForm_correct_1To2' rho1 phi :
      funcfree FOL.sat (toFOLForm' ) Henkin.sat funcs preds (toSOLEnv ) .
    Proof.
      intros F. apply toFOLForm_correct_1To2. apply F. reflexivity. reflexivity.
    Qed.


    Lemma constructed_henkin_model_comprehension rho1 :
      ( phi, toFOLTheory C FOL.sat ) rho2, ( x ar, preds ar (get_pred x ar)) n phi, funcfree Henkin.sat funcs preds (comprehension_form n ).
    Proof.
      intros H n F. apply close_sat_funcfree with ( := toSOLEnv ).
      - apply comprehension_form_funcfree, F.
      - intros x ar'. unfold preds. eexists. cbn. reflexivity.
      - apply toFOLForm_correct_1To2'.
        + apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree, F.
        + apply H. eexists. split. reflexivity. now exists n, .
      - apply .
    Qed.


    Lemma constructed_henkin_interp_correct rho :
      ( x ar, preds ar (get_pred x ar)) ( phi, C Henkin.sat funcs preds ) henkin_interp I2 funcs preds.
    Proof.
      intros Hrho HC. split. easy.
      intros P. unfold preds. assert (Henkin.sat funcs preds (close All (comprehension_form (ar_preds P) (atom (pred P) (tabulate (ar_preds P) var_indi))))) as .
      { apply HC. eexists. eexists. split. 2: reflexivity. now apply tabulate_Forall. }
      eapply close_sat_funcfree with ( := ) in .
      - apply comprehension_form_correct in as [P' [[d ] ]]. exists d.
        intros v. specialize ( v). cbn in . rewrite Deduction.eval_tabulate in .
        cbn. setoid_rewrite . setoid_rewrite . reflexivity.
      - now apply comprehension_form_funcfree, tabulate_Forall.
      - apply Hrho.
      - apply Hrho.
    Qed.


  End FOModel_To_HenkinModel.

Full Translation of Validity


  Notation "A ∪ B" := ( x A x B x) (at level 30).

  Definition validFO `{falsity_flag} (T : FOL.form Prop) phi :=
     D (I : FOL.interp D) rho, ( psi, T FOL.sat ) FOL.sat .

  Lemma henkin_valid_iff_firstorder_valid (T : SOL.form Prop) phi :
    funcfree ( psi, T funcfree ) Henkin.validT T validFO (toFOLTheory (T C)) (toFOLForm' ).
  Proof.
    intros F TF. split.
    - intros H HT. apply toFOLForm_correct_1To2'; trivial. apply H.
      + apply constructed_henkin_interp_correct with ( := toSOLEnv _ ).
        * intros x ar. unfold preds. eexists. cbn. reflexivity.
        * intros [? [? [? ]]]. apply toFOLForm_correct_1To2'.
          now apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree.
          apply HT. eexists. split. reflexivity. right. eexists. eexists. split. 2: reflexivity. easy.
      + eapply constructed_henkin_model_comprehension.
        intros [? []]. apply HT. eexists. split. reflexivity. now right.
      + apply toSOLEnv_henkin_env.
      + intros . apply toFOLForm_correct_1To2'. now apply TF. apply HT. firstorder.
    - intros H funcs preds HI HC H_rho2 HT.
      unshelve eapply toFOLForm_correct_2To1'; trivial.
      + exact (get_indi 0).
      + intros ar. exists (get_pred 0 ar). apply H_rho2.
      + apply H. intros [ [ [|[ar [ [HF ]]]]]].
        * eapply toFOLForm_correct_2To1'. now apply TF. now apply HT.
        * eapply toFOLForm_correct_2To1'. now apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree.
          eapply close_sat_funcfree. now apply comprehension_form_funcfree.
          intros x ar'. apply H_rho2. intros . now apply HC.
  Qed.


Completeness of derived deduction system

  Section DerivedCompleteness.

    Existing Instance FOL.falsity_on.

    Notation "T ⊩1 phi" := (FOL.tprv T ) (at level 61).

    Definition tprv2_derived A phi := toFOLTheory (A C) ⊩1 toFOLForm' .
    Notation "A ⊩2' phi" := (tprv2_derived A ) (at level 61).

    Hypothesis tprv1_sound : (T : FOL.form Prop) phi, T ⊩1 validFO T .
    Hypothesis tprv1_complete : T phi, validFO T T ⊩1 .

    Hypothesis Σp2_enumerable : enumerable__T Σp2.
    Hypothesis Σf2_enumerable : enumerable__T Σf2.
    Hypothesis Σp2_eq_dec : eq_dec Σp2.
    Hypothesis Σf2_eq_dec : eq_dec Σf2.

    Hypothesis tprv1_enumerable : enumerable__T Σf1 enumerable__T Σp1 T, enumerable T enumerable (FOL.tprv T).

    Lemma tprv2_derived_sound (T : SOL.form Prop) phi :
      funcfree ( psi, T funcfree ) T ⊩2' Henkin.validT T .
    Proof.
      intros ? ? H. now apply henkin_valid_iff_firstorder_valid, tprv1_sound, H.
    Qed.


    Lemma tprv2_derived_complete (T : SOL.form Prop) phi :
      funcfree ( psi, T funcfree ) Henkin.validT T T ⊩2' .
    Proof.
      intros ? ? H. now apply tprv1_complete, henkin_valid_iff_firstorder_valid, H.
    Qed.


    Lemma tprv2_derived_enumerable (T : SOL.form Prop) :
      enumerable T enumerable (tprv2_derived T).
    Proof.
      intros H. unfold tprv2_derived. apply enumerable_comp.
      - apply tprv1_enumerable, toFOLTheory_enumerable, enumerable_disj.
        now apply Sigma_f1_enumerable. now apply Sigma_p1_enumerable.
        apply H. now apply C_enumerable.
      - apply form_enumerable; trivial. apply enumT_binop. apply enumT_quantop.
      - apply FOL.dec_form. now apply Sigma_f1_eq_dec. now apply Sigma_p1_eq_dec.
        all: intros x y; unfold dec; decide equality.
    Qed.


  End DerivedCompleteness.

Deductive Reduction

Preliminaries


  Section ArityBoundedSubst.

    Context {Σf2' : SOL.funcs_signature}.
    Context {Σp2' : SOL.preds_signature}.

    Definition subst_all_below_ar_p (sigma : ar, predicate ar) ar :=
       n ar' if Compare_dec.lt_dec ar' ar then n ar' else var_pred n.

    Definition subst_all_from_ar_p (sigma : ar, predicate ar) ar :=
       n ar' if Compare_dec.lt_dec ar' ar then var_pred n else n ar'.

    Lemma subst_all_below_ar_bounded b phi sigma :
      arity_bounded_p b [subst_all_below_ar_p b]p = []p.
    Proof.
      intros B. eapply subst_ext_p_arity_bounded. apply B.
      intros x ar H. unfold subst_all_below_ar_p.
      now destruct Compare_dec.lt_dec; try lia.
    Qed.


    Lemma subst_all_from_ar_bounded b phi sigma :
      arity_bounded_p b [subst_all_from_ar_p b]p = .
    Proof.
      intros B. erewrite subst_id_p. eapply subst_ext_p_arity_bounded. apply B.
      intros x ar H. unfold subst_all_from_ar_p.
      now destruct Compare_dec.lt_dec; try lia.
    Qed.


  End ArityBoundedSubst.

Closing operation for predicate variables

  Section ClosePredicateAr.

    Context {Σf2' : SOL.funcs_signature}.
    Context {Σp2' : SOL.preds_signature}.

    Fixpoint close_p op phi n := match n with 0 | S n SOL.quant_pred op n (close_p op n) end.

    Lemma close_p_subst_i op phi sigma n :
      (close_p op n)[]i = close_p op ([]i) n.
    Proof.
      revert . induction n; intros ; cbn. reflexivity. now rewrite IHn.
    Qed.


    Lemma close_p_subst_f op phi sigma n :
      (close_p op n)[]f = close_p op ([]f) n.
    Proof.
      revert . induction n; intros ; cbn. reflexivity. now rewrite IHn.
    Qed.


    Definition all_up_p sigma : ar, predicate ar :=
       n ar match n with 0 var_pred 0 | S n ( n ar)[ ar]p end.

    Lemma close_p_subst_p op phi sigma n :
      (close_p op n)[]p = close_p op ([subst_all_below_ar_p (all_up_p ) n]p[subst_all_from_ar_p n]p) n.
    Proof.
      rewrite subst_comp_p. revert . induction n; intros .
      - apply subst_ext_p. intros n ar. unfold subst_all_below_ar_p, subst_all_from_ar_p.
        now destruct Compare_dec.lt_dec; try lia.
      - cbn. f_equal. rewrite IHn. f_equal. apply subst_ext_p. intros [] ar;
        unfold subst_all_from_ar_p, subst_all_below_ar_p;
        repeat (destruct Compare_dec.lt_dec, Compare_dec.lt_dec; try lia; try reflexivity; cbn).
        all: unfold up_p, scons, scons_pred, scons_ar, shift, shift_p;
        repeat (destruct PeanoNat.Nat.eq_dec as [|]; try lia; try easy; cbn).
        + destruct ; cbn; try easy. now destruct PeanoNat.Nat.eq_dec as [|]; try lia.
        + destruct ; repeat (destruct PeanoNat.Nat.eq_dec as [|]; try lia; try easy; cbn);
          destruct ; cbn; try reflexivity; repeat (try rewrite nat_eq_dec_same;
          try destruct PeanoNat.Nat.eq_dec as [|]; try destruct Compare_dec.lt_dec; try lia; try reflexivity; cbn).
        + destruct Compare_dec.lt_dec; try lia. destruct ; cbn; try easy. rewrite nat_eq_dec_same.
          cbn. now destruct Compare_dec.lt_dec.
        + destruct ; cbn; try reflexivity. now destruct PeanoNat.Nat.eq_dec; try lia.
    Qed.


    Lemma close_p_subst_p' op phi sigma n :
      (close_p op n)[]p = close_p op ([ x ar if Compare_dec.lt_dec ar n then match x with 0 var_pred 0 ar | S x ( x ar)[ ar]p end else x ar]p) n.
    Proof.
      rewrite close_p_subst_p, subst_comp_p. f_equal. apply subst_ext_p.
      intros [] ar; destruct Compare_dec.lt_dec; cbn; unfold subst_all_below_ar_p, subst_all_from_ar_p;
      repeat (destruct Compare_dec.lt_dec; try lia; try reflexivity; cbn).
      unfold shift, shift_p. destruct ; cbn; try reflexivity. rewrite nat_eq_dec_same; cbn.
      now destruct Compare_dec.lt_dec.
    Qed.


    Lemma close_p_subst_p_bounded op b phi sigma :
      (arity_bounded_p b ) (close_p op b)[]p = close_p op ([all_up_p ]p) b.
    Proof.
      intros B. rewrite close_p_subst_p. f_equal. rewrite subst_all_from_ar_bounded.
      apply subst_all_below_ar_bounded. apply B. apply arity_bounded_p_subst_p, B.
    Qed.


    Lemma close_p_bounded_indi n b op phi :
      bounded_indi b bounded_indi b (close_p op n).
    Proof.
      now induction n.
    Qed.


    Lemma close_p_bounded_pred m ar b op phi :
      bounded_pred ar b bounded_pred ar b (close_p op m).
    Proof.
      revert b. induction m; intros b H; cbn.
      - exact H.
      - destruct (PeanoNat.Nat.eq_dec ar m).
        + left. split. easy. apply IHm. eapply bounded_pred_up. 2: apply H. lia.
        + right. split. easy. now apply IHm.
    Qed.


    Lemma close_p_bounded_pred_2 m ar b op phi :
      ar < m bounded_pred ar (S b) bounded_pred ar b (close_p op m).
    Proof.
      revert b. induction m; intros b ; cbn.
      - lia.
      - destruct (PeanoNat.Nat.eq_dec ar m).
        + left. split. easy. apply close_p_bounded_pred, .
        + right. split. easy. apply IHm. lia. apply .
    Qed.


    Lemma close_p_arity_bounded ar phi op n :
      arity_bounded_p ar arity_bounded_p ar (close_p op n).
    Proof.
      now induction n.
    Qed.


    Lemma close_p_find_arity_bound_p op phi n :
      find_arity_bound_p (close_p op n) = find_arity_bound_p .
    Proof.
      now induction n.
    Qed.


    (* Deduction *)

    Definition shift_p_all : ar, predicate ar := n ar var_pred (S n).

    Definition subst_first_p_all (P : ar, predicate ar) : ar, predicate ar :=
       n ar match n with 0 P ar | S n var_pred n end.

    Notation "⇑" := shift_p_all.
    Notation "P ,," := (subst_first_p_all P) (at level 4, format "P ,,").

    Lemma close_p_AllI {p' : peirce} A phi n :
      List.map (subst_p (subst_all_below_ar_p n)) A ⊢2 A ⊢2 close_p All n.
    Proof.
      revert A. induction n; intros A H; cbn.
      - enough (List.map (subst_p (subst_all_below_ar_p 0)) A = A) as by apply H.
        clear H. induction A as [| A IH]; cbn. reflexivity. f_equal. rewrite subst_id_p.
        now apply subst_ext_p. apply IH.
      - apply AllI_p. apply IHn. rewrite List.map_map.
        enough (List.map (subst_form_p ( n) >> subst_p (subst_all_below_ar_p n)) A = List.map (subst_p (subst_all_below_ar_p (S n))) A) as by apply H.
        apply List.map_ext. intros . change (subst_form_p ( n) ) with ([ n]p).
        rewrite subst_comp_p. apply subst_ext_p. intros n' ar. unfold subst_all_below_ar_p, shift, shift_p.
        now destruct Compare_dec.lt_dec, PeanoNat.Nat.eq_dec; cbn; destruct Compare_dec.lt_dec; try lia.
    Qed.


    Lemma close_p_AllI_nameless' {p' : peirce} phi A b n :
      arity_bounded_p n
       ( ar, ar < n bounded_pred_L ar b A)
       ( ar, ar < n bounded_pred ar b )
       A ⊢2 [(@var_pred _ b),,]p
       A ⊢2 close_p All n.
    Proof.
      intros B . erewrite subst_all_below_ar_bounded. 2: apply B. clear B.
      revert . induction n; intros H; cbn.
      - enough ( = [subst_all_below_ar_p (@var_pred _ b),, 0]p) as by apply H.
        rewrite subst_id_p at 1. apply subst_ext_p. intros n ar'. unfold subst_all_below_ar_p.
        now destruct Compare_dec.lt_dec; try lia.
      - apply AllI_p, nameless_equiv_all_p' with (:=b). apply . lia. apply close_p_bounded_pred.
        eapply bounded_pred_up. 2: apply . lia. lia. rewrite close_p_subst_p'. apply IHn.
        + intros ar . apply . lia. exact .
        + intros ar . apply bounded_pred_subst_p. 2: apply ; lia.
          intros []; destruct Compare_dec.lt_dec; try easy. destruct ; cbn;
          unfold subst_all_below_ar_p, shift, shift_p;
          now repeat (destruct PeanoNat.Nat.eq_dec; try lia; cbn).
        + rewrite subst_comp_p. erewrite subst_ext_p. apply H.
          intros [] ar; cbn; unfold subst_all_below_ar_p, shift, shift_p;
          repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [|]; cbn; try lia; try reflexivity).
          destruct ; cbn; repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [|]; cbn; try lia; try reflexivity).
    Qed.


    Lemma close_p_AllI_nameless {p' : peirce} phi A n :
      arity_bounded_p n { x | A ⊢2 [(@var_pred _ x),,]p A ⊢2 close_p All n }.
    Proof.
      intros B. enough { b | ar, ar < n bounded_pred_L ar b A bounded_pred ar b } as [x H].
      { exists x. apply close_p_AllI_nameless'. apply B. apply H. apply H. }
      clear B. induction n.
      - exists 0. intros ar H; lia.
      - destruct IHn as [b H]. destruct (find_bounded_pred_L n (List.cons A)) as [b' ].
        exists (max b b'). intros ar . assert (ar < n ar = n) as [| ] by lia.
        + split. intros . all: eapply bounded_pred_up; [| apply H]; try lia; easy.
        + split. intros . all: eapply bounded_pred_up; [| apply ]; try lia; firstorder.
    Qed.


    Lemma close_p_AllE phi {p' : peirce} A n P :
      arity_bounded_p n A ⊢2 close_p All n A ⊢2 [P,,]p.
    Proof.
      intros B. erewrite subst_all_below_ar_bounded. 2: apply B.
      clear B. induction n in |-*; cbn; intros H.
      - erewrite subst_ext_p, subst_id_p. apply H. reflexivity.
      - apply AllE_p with ( := P n) in H. rewrite close_p_subst_p' in H.
        apply IHn in H. rewrite subst_comp_p in H. erewrite subst_ext_p. apply H.
        intros [] ar; cbn; unfold subst_all_below_ar_p;
        repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn);
        destruct P; try reflexivity; cbn;
        destruct ; cbn; unfold shift, shift_p; repeat (try destruct Compare_dec.lt_dec;
        try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn).
    Qed.


    Lemma close_p_ExE_nameless' {p' : peirce} phi psi A b n :
      ( ar, ar < n bounded_pred_L ar b A)
       ( ar, ar < n bounded_pred ar b )
       ( ar, ar < n bounded_pred ar b )
       A ⊢2 close_p Ex n
       [subst_all_below_ar_p (@var_pred _ b),, n]p :: A ⊢2
       A ⊢2 .
    Proof.
      induction n in A, |-*; intros ; cbn in *.
      - eapply IE. apply II, . enough ( = [subst_all_below_ar_p (@var_pred _ b),, 0]p) as by apply .
        rewrite subst_id_p at 1. apply subst_ext_p. intros n ar'. unfold subst_all_below_ar_p.
        now destruct Compare_dec.lt_dec; try lia.
      - eapply ExE_p. apply . eapply nameless_equiv_ex_p' with (:=b).
        + apply . lia.
        + apply . lia.
        + eapply bounded_pred_up. 2: apply close_p_bounded_pred, . lia. lia.
        + eapply IHn. 4: rewrite close_p_subst_p' with ( := (var_pred b n)..).
          * intros ar H [|]. apply bounded_pred_subst_p.
            now intros []; cbn; destruct PeanoNat.Nat.eq_dec; try lia.
            apply close_p_bounded_pred, . lia. apply . lia. easy.
          * intros ar H. apply bounded_pred_subst_p. intros []; destruct Compare_dec.lt_dec; try lia.
            reflexivity. now destruct ; cbn; destruct PeanoNat.Nat.eq_dec; try lia; unfold shift, shift_p; cbn;
            destruct PeanoNat.Nat.eq_dec; try lia. apply . lia.
          * intros. apply . lia.
          * apply Ctx. now left.
          * rewrite subst_comp_p. erewrite subst_ext_p with ( := subst_all_below_ar_p (@var_pred _ b),, (S n)).
            eapply Weak. 2: apply . clear -; firstorder.
            intros [|] ar; unfold subst_all_below_ar_p, shift, shift_p; destruct Compare_dec.lt_dec; cbn;
            repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn).
            destruct ; cbn; repeat (destruct PeanoNat.Nat.eq_dec; try lia; cbn);
            now destruct Compare_dec.lt_dec; try lia.
    Qed.


    Lemma close_p_ExE_nameless {p' : peirce} phi psi A n :
      arity_bounded_p n A ⊢2 close_p Ex n { x | [(@var_pred _ x),,]p :: A ⊢2 A ⊢2 }.
    Proof.
      intros B. enough { b | ( ar, ar < n ( phi, List.In A bounded_pred ar b ) bounded_pred ar b bounded_pred ar b ) } as [x H].
      { exists x. erewrite subst_all_below_ar_bounded. 2: apply B. apply close_p_ExE_nameless'; firstorder. }
      clear B. induction n.
      - exists 0. intros ar H; lia.
      - destruct IHn as [b H]. destruct (find_bounded_pred_L n (List.cons (List.cons A))) as [b' ].
        exists (max b b'). intros ar . assert (ar < n ar = n) as [| ] by lia.
        + repeat split. intros . all: eapply bounded_pred_up; [| apply H]; try lia; easy.
        + repeat split. intros . all: eapply bounded_pred_up; [| apply ]; try lia; firstorder.
    Qed.


    Lemma close_p_ExI {p' : peirce} A phi n P :
      arity_bounded_p n A ⊢2 [P,,]p A ⊢2 close_p Ex n.
    Proof.
      intros B. erewrite subst_all_below_ar_bounded. 2: apply B.
      clear B. induction n in |-*; cbn; intros H.
      - erewrite subst_id_p, subst_ext_p. apply H. intros n ar. unfold subst_all_below_ar_p.
        now destruct Compare_dec.lt_dec; try lia.
      - apply ExI_p with (:=P n). rewrite close_p_subst_p'. apply IHn.
        erewrite subst_comp_p, subst_ext_p. apply H.
        intros [] ar; cbn; unfold subst_all_below_ar_p;
        repeat (try destruct Compare_dec.lt_dec; try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn);
        destruct P; cbn; try reflexivity. now destruct Compare_dec.lt_dec.
        all: destruct ; cbn; unfold shift, shift_p; repeat (try destruct Compare_dec.lt_dec;
        try destruct PeanoNat.Nat.eq_dec as [|]; try lia; try reflexivity; cbn).
    Qed.


  End ClosePredicateAr.

  Notation "⇑" := shift_p_all.
  Notation "P ,," := (subst_first_p_all P) (at level 4, format "P ,,").

Add falsity symbol to signature

  Inductive ExtendedPreds :=
    | OldPred : SOL.preds ExtendedPreds
    | FalsePred : ExtendedPreds.

  Instance Σp2' : SOL.preds_signature := {|
    SOL.preds := ExtendedPreds ;
    SOL.ar_preds P := match P with OldPred P SOL.ar_preds P | FalsePred ar ar end
  |}.

Removal of Falsity Symbols


  Fixpoint removeFalsePred (phi : @SOL.form Σf2 Σp2' _) : @SOL.form Σf2 Σp2 _ := match with
    | SOL.atom (pred (OldPred p)) v SOL.atom (pred p) v
    | SOL.atom (pred (FalsePred ar)) v SOL.fal
    | SOL.atom (var_pred x ar) v SOL.atom (var_pred x ar) v
    | SOL.fal SOL.fal
    | SOL.bin op SOL.bin op (removeFalsePred ) (removeFalsePred )
    | SOL.quant_indi op SOL.quant_indi op (removeFalsePred )
    | SOL.quant_func op ar SOL.quant_func op ar (removeFalsePred )
    | SOL.quant_pred op ar SOL.quant_pred op ar (removeFalsePred )
  end.

  Lemma removeFalsePred_subst_i phi sigma :
    (removeFalsePred )[]i = removeFalsePred ([]i).
  Proof.
    induction in |- *; cbn; try congruence. now destruct p as [|[]].
  Qed.


  Lemma removeFalsePred_subst_f phi sigma :
    (removeFalsePred )[]f = removeFalsePred ([]f).
  Proof.
    induction in |- *; cbn; try congruence. now destruct p as [|[]].
  Qed.


  Lemma removeFalsePred_subst_p phi sigma sigma' :
    ( n ar, ( x, n ar = var_pred x n ar = var_pred x)
                P (e : ar_preds P = ar), n ar = Util.cast _ e (pred P) n ar = Util.cast _ e (pred (OldPred P)))
     (removeFalsePred )[]p = removeFalsePred ([]p).
  Proof.
    induction in , |- *; cbn; intros H.
    - reflexivity.
    - destruct p as [|[]]; cbn; try reflexivity. now destruct (H n ar) as [[x [ ]]|[P [ [ ]]]].
    - erewrite , . reflexivity. apply H. apply H.
    - erewrite IHphi. reflexivity. apply H.
    - erewrite IHphi. reflexivity. apply H.
    - erewrite IHphi. reflexivity. intros [] ar; cbn.
      + destruct PeanoNat.Nat.eq_dec as [|]. left. now exists 0. edestruct H as [[x [ ]]|[P [ [ ]]]].
        * left. exists x; cbn. unfold shift, shift_p. now destruct PeanoNat.Nat.eq_dec.
        * right. now exists P, eq_refl.
      + destruct PeanoNat.Nat.eq_dec as [|]; edestruct H as [[x [ ]]|[P [ [ ]]]].
        * left. exists (S x). cbn; unfold shift, shift_p; now destruct PeanoNat.Nat.eq_dec.
        * right. now exists P, eq_refl.
        * left. exists x. cbn; unfold shift, shift_p; now destruct PeanoNat.Nat.eq_dec.
        * right. now exists P, eq_refl.
  Qed.


  Lemma removeFalsePred_forall_n n phi :
    removeFalsePred (forall_n n ) = forall_n n (removeFalsePred ).
  Proof.
    induction n; cbn; congruence.
  Qed.


  Lemma removeFalsePred_close_p op phi n :
    removeFalsePred (close_p op n) = close_p op (removeFalsePred ) n.
  Proof.
    induction n; cbn. reflexivity. now rewrite IHn.
  Qed.


  Lemma removeFalsePred_arity_bounded_p phi n :
    arity_bounded_p n arity_bounded_p n (removeFalsePred ).
  Proof.
    induction . 2: now destruct p as [|[]]. all: firstorder.
  Qed.


  Lemma removeFalsePred_funcfree phi :
    funcfree funcfree (removeFalsePred ).
  Proof.
    intros F. induction ; cbn; firstorder. now destruct p as [|[]]; cbn.
  Qed.


  Lemma replace_FalsePred_subst {p' : peirce} (phi : @SOL.form Σf2 Σp2' _) ar n :
    List.nil ⊢2 (forall_n ar (p$n (tabulate ar var_indi) <--> )) --> (removeFalsePred [(@pred Σp2' (FalsePred ar))..]p <--> (removeFalsePred )[(var_pred n ar)..]p).
  Proof.
    enough ( sigma1 sigma2 n m,
                  m ar = pred (FalsePred ar)
               m ar = var_pred n ar
               ( x ar', x m ar' ar y, x ar' = var_pred y x ar' = var_pred y)
               List.nil ⊢2 (forall_n ar (p$n (tabulate ar var_indi) <--> )) --> (removeFalsePred []p <--> (removeFalsePred )[]p)) as X.
    { apply X with (m:=0); cbn -[PeanoNat.Nat.eq_dec].
      - now rewrite nat_eq_dec_same.
      - now rewrite nat_eq_dec_same.
      - intros x ar' [].
        + destruct x; try lia; cbn. destruct PeanoNat.Nat.eq_dec as [|]; now eexists.
        + exists x. destruct x; cbn; now destruct PeanoNat.Nat.eq_dec as [|]. }
    induction ; cbn; intros n' m ; apply II.
    - apply CI; apply II; apply Ctx; now left.
    - destruct p as [|[]]; cbn. 2,3: apply CI; apply II; apply Ctx; now left.
      specialize ( ). destruct (PeanoNat.Nat.eq_dec m) as [|].
      + destruct (PeanoNat.Nat.eq_dec ar) as [|].
        * rewrite , .
          Existing Instance Σp2. (* TODO: Better way to locally force the usage of Σp2 ? *)
          assert (forall_n ar (p$n' (tabulate ar var_indi) <--> ) :: List.nil ⊢2forall_n ar (p$n' (tabulate ar var_indi) <--> )) as H by now apply Ctx.
          eapply prv_forall_n in H. cbn in H. rewrite tabulate_var_indi_subst in H.
          apply prv_equiv_symmetry, H.
        * destruct as [? [ ]]. lia. apply CI; apply II; apply Ctx; now left.
      + destruct as [? [ ]]. lia. apply CI; apply II; apply Ctx; now left.
    - apply prv_equiv_bin; apply switch_imp. eapply ; eassumption. eapply ; eassumption.
    - apply prv_equiv_quant_i. cbn. setoid_rewrite comprehension_subst_i with ( := ).
      eapply switch_imp, IHphi; eassumption.
    - apply prv_equiv_quant_f. cbn. setoid_rewrite comprehension_subst_f with ( := ).
      eapply switch_imp, IHphi; eassumption.
    - apply prv_equiv_quant_p. cbn. destruct (PeanoNat.Nat.eq_dec ar) as [|].
      + setoid_rewrite forall_n_subst_p. cbn. unfold shift, shift_p. rewrite nat_eq_dec_same.
        apply switch_imp. eapply IHphi with (m := S m); cbn. now rewrite nat_eq_dec_same, .
        rewrite nat_eq_dec_same, ; cbn; unfold shift, shift_p; now rewrite nat_eq_dec_same.
        intros x ar' [].
        * destruct x; cbn; destruct PeanoNat.Nat.eq_dec as [|]. now exists 0.
          all: edestruct as [? [ ]]; try lia; cbn; unfold shift, shift_p;
          destruct PeanoNat.Nat.eq_dec; try lia; now eexists.
        * destruct x; cbn; destruct PeanoNat.Nat.eq_dec; try lia; edestruct as [? [ ]]; try lia;
          cbn; unfold shift, shift_p; destruct PeanoNat.Nat.eq_dec; try lia; now eexists.
      + setoid_rewrite forall_n_subst_p. cbn. unfold shift, shift_p. destruct PeanoNat.Nat.eq_dec; try lia.
        apply switch_imp. eapply IHphi with (m := m); cbn. destruct m; cbn; destruct PeanoNat.Nat.eq_dec; try lia;
        now rewrite . destruct m; cbn; destruct PeanoNat.Nat.eq_dec; try lia; rewrite ; cbn;
        unfold shift, shift_p; now destruct PeanoNat.Nat.eq_dec.
        intros x ar' [].
        * destruct x; cbn; destruct PeanoNat.Nat.eq_dec as [|]. now exists 0.
          all: edestruct as [? [ ]]; try lia; cbn; unfold shift, shift_p;
          destruct PeanoNat.Nat.eq_dec; try lia; now eexists.
        * destruct x; cbn; destruct PeanoNat.Nat.eq_dec as [|]; try lia. now exists 0.
          all: edestruct as [? [ ]]; try lia; cbn; unfold shift, shift_p;
          destruct PeanoNat.Nat.eq_dec; try lia; now eexists.
  Qed.


  Lemma prv_removeFalsePred {p' : peirce} A (phi : @SOL.form Σf2 Σp2' _) :
    A ⊢2 (List.map removeFalsePred A) ⊢2 (removeFalsePred ).
  Proof.
    induction 1; 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.
    - apply DI1, IHprv.
    - apply DI2, IHprv.
    - eapply DE. apply . apply . apply .
    - apply Peirce.
    - apply AllI_i. rewrite List.map_map in *. erewrite List.map_ext. apply IHprv.
      intros ?. apply removeFalsePred_subst_i.
    - apply AllI_f. rewrite List.map_map in *. erewrite List.map_ext. apply IHprv.
      intros ?. apply removeFalsePred_subst_f.
    - apply AllI_p. rewrite List.map_map in *. erewrite List.map_ext. apply IHprv.
      intros ?. apply removeFalsePred_subst_p. intros n ar'. left. destruct (PeanoNat.Nat.eq_dec ar ar').
      all: eexists; unfold shift, shift_p; now destruct PeanoNat.Nat.eq_dec.
    - rewrite removeFalsePred_subst_i. eapply AllE_i, IHprv.
    - rewrite removeFalsePred_subst_f. eapply AllE_f, IHprv.
    - destruct P as [|[]].
      + erewrite removeFalsePred_subst_p. eapply AllE_p with (P:=var_pred n), IHprv.
        intros [] ar'; cbn; left; destruct (PeanoNat.Nat.eq_dec ar ar') as [|]; eexists; split; reflexivity.
      + erewrite removeFalsePred_subst_p. eapply AllE_p with (P:=pred ), IHprv.
        intros [] ar; cbn -[PeanoNat.Nat.eq_dec]; destruct PeanoNat.Nat.eq_dec as [|].
        right. now exists , eq_refl. all: left; now eexists.
      + eapply ExE_p with (ar := n). apply Comp with (:=). easy.
        destruct (find_bounded_pred_L n ((removeFalsePred [(@pred Σp2' (FalsePred n))..]p :: (forall_n n (p$0 (tabulate n var_indi) <--> [ n]p)) :: List.map removeFalsePred A))) as [b Hb].
        eapply nameless_equiv_ex_p' with ( := b).
        * intros ? ?. apply Hb. auto.
        * apply Hb. auto.
        * eapply bounded_pred_up. 2: apply Hb. lia. firstorder.
        * eapply IE. eapply CE2. apply switch_imp. eapply Weak; revgoals.
          rewrite forall_n_subst_p; cbn. destruct PeanoNat.Nat.eq_dec as [[]|]; try easy.
          eapply replace_FalsePred_subst. firstorder.
          eapply AllE_p in IHprv. eapply Weak. 2: apply IHprv. firstorder.
    - eapply ExI_i. rewrite removeFalsePred_subst_i. apply IHprv.
    - eapply ExI_f. rewrite removeFalsePred_subst_f. apply IHprv.
    - destruct P as [|[]].
      + eapply ExI_p. erewrite removeFalsePred_subst_p. apply IHprv.
        intros [] ar'; cbn; left; destruct (PeanoNat.Nat.eq_dec ar ar') as [|]; eexists; split; reflexivity.
      + eapply ExI_p. erewrite removeFalsePred_subst_p. apply IHprv.
        intros [] ar; cbn -[PeanoNat.Nat.eq_dec]; destruct PeanoNat.Nat.eq_dec as [|].
        right. now exists , eq_refl. all: left; now eexists.
      + eapply ExE_p with (ar := n). eapply Comp with (:=). easy.
        destruct (find_bounded_pred_L n ((removeFalsePred ) :: (forall_n n (p$0 (tabulate n var_indi) <--> [ n]p) :: (List.map removeFalsePred A)))) as [b Hb].
        eapply nameless_equiv_ex_p' with ( := b).
        * intros ? ?. apply Hb. auto.
        * cbn. left. split. reflexivity. eapply bounded_pred_up. 2: apply Hb. lia. firstorder.
        * eapply bounded_pred_up. 2: apply Hb. lia. firstorder.
        * eapply ExI_p. eapply IE. eapply CE1. apply switch_imp. eapply Weak; revgoals.
          rewrite forall_n_subst_p; cbn. destruct PeanoNat.Nat.eq_dec as [[]|]; try easy.
          eapply replace_FalsePred_subst with (:=b). firstorder.
          eapply Weak. 2: apply IHprv. firstorder.
    - eapply ExE_i. apply . rewrite removeFalsePred_subst_i. rewrite List.map_map in *.
      erewrite List.map_ext. apply . intros ?. apply removeFalsePred_subst_i.
    - eapply ExE_f. apply . rewrite removeFalsePred_subst_f. rewrite List.map_map in *.
      erewrite List.map_ext. apply . intros ?. apply removeFalsePred_subst_f.
    - eapply ExE_p. apply . erewrite removeFalsePred_subst_p. rewrite List.map_map in *.
      erewrite List.map_ext. apply . intros ?. eapply removeFalsePred_subst_p.
      all: intros n ar'; left; destruct (PeanoNat.Nat.eq_dec ar ar'); eexists; unfold shift, shift_p;
      destruct PeanoNat.Nat.eq_dec; try lia; split; reflexivity.
    - rewrite removeFalsePred_forall_n. cbn. erewrite removeFalsePred_subst_p. apply Comp.
      now apply removeFalsePred_funcfree. intros n ar'. left.
      destruct (PeanoNat.Nat.eq_dec ar ar'); eexists; unfold shift, shift_p;
      destruct PeanoNat.Nat.eq_dec; try lia; split; reflexivity.
  Qed.


Backwards Translation Function


  Existing Instance Σp2'.

  Fixpoint toSOLTerm (t : FOL.term) := match t with
    | FOL.var x SOL.var_indi x
    | FOL.func (NormalSym f) v SOL.func (sym f) (Vector.map toSOLTerm v)
  end.

  Fixpoint toSOLForm {ff : falsity_flag} (phi : FOL.form) : @SOL.form Σf2 Σp2' _ := match with
    | FOL.atom (NormalPred p) v SOL.atom (@pred Σp2' (OldPred p)) (Vector.map toSOLTerm v)
    | FOL.atom (PredApp ar) v match Vector.hd v with
                                  | FOL.var x SOL.atom (var_pred x) (Vector.tl (Vector.map toSOLTerm v))
                                  | _ SOL.atom (@pred Σp2' (FalsePred _)) (Vector.tl (Vector.map toSOLTerm v))
                                end
    | FOL.falsity SOL.fal
    | FOL.bin op SOL.bin (toSOLBinop op) (toSOLForm ) (toSOLForm )
    | FOL.quant op (close_p (toSOLQuantop op) (quant_indi (toSOLQuantop op) (toSOLForm )) (find_arity_bound_p (toSOLForm )))
  end.

  Definition toSOLSub_i (sigma : FOL.term) := n toSOLTerm ( n).
  Definition toSOLSub_p (sigma : FOL.term) := n ar match n with FOL.var x var_pred x ar | _ pred (FalsePred _) end.

Substitutions

  Lemma toSOLTerm_subst {ff: falsity_flag} t sigma :
    (toSOLTerm t)[toSOLSub_i ]i = toSOLTerm (FOL.subst_term t).
  Proof.
    induction t using FOL_term_ind; cbn.
    - reflexivity.
    - destruct F; cbn; f_equal. rewrite !Vector.map_map. apply VectorLib.map_ext_forall, IH.
  Qed.


  Lemma toSOLForm_subst {ff: falsity_flag} phi sigma :
    (toSOLForm )[toSOLSub_p ]p[toSOLSub_i ]i = toSOLForm (`[]).
  Proof.
    revert ; induction ; intros ; cbn.
    - reflexivity.
    - destruct P; cbn.
      + f_equal. rewrite !Vector.map_map. apply map_ext_forall, Forall_in. intros t' H.
        apply toSOLTerm_subst.
      + depelim t; destruct h; cbn; unfold toSOLSub_p. destruct ( ).
        all: f_equal; rewrite !Vector.map_map; eapply VectorLib.map_ext_in; intros t' H;
        apply toSOLTerm_subst.
    - f_equal; firstorder.
    - f_equal. rewrite IHphi. rewrite close_p_subst_p_bounded, close_p_subst_i. 2: cbn; apply find_arity_bound_p_correct.
      cbn. f_equal. erewrite subst_ext_i, subst_ext_p. reflexivity.
      + intros [] ar; cbn. reflexivity. unfold toSOLSub_p, shift, shift_p, up, ">>'", FOL.scons.
        destruct ; cbn. now rewrite nat_eq_dec_same. reflexivity.
      + intros []; cbn. reflexivity. now setoid_rewrite toSOLTerm_subst.
      + now rewrite find_arity_bound_p_subst_i, find_arity_bound_p_subst_p.
  Qed.


Boundedness

  Hypothesis Σf2_eq_dec : f1 f2 : Σf2, = .
  Hypothesis Σp2_eq_dec : p1 p2 : Σp2, = .

  Lemma toSOLTerm_bounded_indi {ff : falsity_flag} t b :
    bounded_t b t bounded_indi_term b (toSOLTerm t).
  Proof.
    intros H. induction t using FOL_term_ind; cbn.
    - now inversion H.
    - destruct F; cbn. rewrite Forall_map. eapply Forall_ext_Forall. apply IH.
      apply Forall_in. intros t . inversion H. apply inj_pairT2 in as .
      apply . now apply In_compat. decide equality.
  Qed.


  Lemma toSOLForm_bounded_indi {ff : falsity_flag} phi b :
    bounded b bounded_indi b (toSOLForm ).
  Proof.
    revert b. induction ; intros b' H; cbn.
    - easy.
    - inversion H. apply inj_pairT2 in as . 2: decide equality; lia.
      destruct P; cbn. 2: depelim t; destruct h; cbn.
      all: apply Forall_in; intros ? [t' [ ]]%In_map_iff; apply toSOLTerm_bounded_indi;
      apply . now apply In_compat. all: constructor; now apply In_compat.
    - inversion H. apply inj_pairT2 in as , as . split. now apply .
      now apply . all: decide equality.
    - inversion H. apply inj_pairT2 in as . 2: decide equality.
      now apply close_p_bounded_indi, IHphi.
  Qed.


  Lemma toSOLForm_bounded_pred {ff : falsity_flag} phi b :
    bounded b ar, bounded_pred ar b (toSOLForm ).
  Proof.
    revert b. induction ; intros b' H ar; cbn.
    - easy.
    - destruct P; cbn. easy. depelim t; destruct h; cbn. left. inversion H.
      apply inj_pairT2 in as . specialize ( (FOL.var ) ltac:(constructor)). now inversion .
      decide equality. lia. easy.
    - inversion H. apply inj_pairT2 in as , as . split. now apply .
      now apply . all: decide equality.
    - inversion H. apply inj_pairT2 in as . 2: decide equality.
      destruct (Compare_dec.lt_dec ar (find_arity_bound_p (toSOLForm ))) as [|].
      + apply close_p_bounded_pred_2. easy. apply IHphi, .
      + eapply bounded_pred_arity_bound. apply close_p_arity_bounded, find_arity_bound_p_correct.
        cbn. lia.
  Qed.


Translation of Derivations

Translate first-order derivation into second-order derivation

  Lemma prv1_to_prv2_AllI {ff : falsity_flag} {p' : peirce} A phi :
    List.map toSOLForm (List.map (subst_form ↑') A) ⊢2 toSOLForm List.map toSOLForm A ⊢2 toSOLForm (∀' ).
  Proof.
    destruct (find_bounded_L ( :: A)) as [x Hx].
    intros H. apply subst_Weak_p with ( := toSOLSub_p (var x)..') in H.
    apply subst_Weak_i with ( := toSOLSub_i (var x)..') in H.
    erewrite !List.map_map, toSOLForm_subst, List.map_ext with (g := toSOLForm) in H; revgoals.
    { intros . setoid_rewrite toSOLForm_subst. now rewrite subst_shift. }
    cbn. eapply close_p_AllI_nameless' with (b := x).
    - cbn. apply find_arity_bound_p_correct.
    - intros ar ? [ [ ]]%List.in_map_iff. apply toSOLForm_bounded_pred. apply Hx; auto.
    - intros ar . apply toSOLForm_bounded_pred. apply Hx; auto.
    - cbn; eapply AllI_i, nameless_equiv_all_i' with (n := x).
      + intros ? [ [ ]]%List.in_map_iff. apply toSOLForm_bounded_indi. apply Hx; auto.
      + apply bounded_indi_subst_p. eapply bounded_indi_up. 2: apply toSOLForm_bounded_indi, Hx; auto. lia.
      + erewrite subst_ext_p, subst_ext_i, toSOLForm_subst. apply H. now intros []. now intros [].
    - now intros [].
  Qed.


  Lemma prv1_to_prv2_AllE {ff : falsity_flag} {p' : peirce} A phi (t : FOL.term) :
    List.map toSOLForm A ⊢2 toSOLForm (∀' ) List.map toSOLForm A ⊢2 toSOLForm `[t..'].
  Proof.
    cbn. intros H. apply close_p_AllE with (P := ar match t with FOL.var x var_pred x | _ @pred Σp2' (FalsePred ar) end) in H.
    cbn in H. eapply AllE_i with ( := toSOLTerm t) in H. rewrite toSOLForm_subst.
    erewrite subst_ext_i, subst_ext_p. apply H.
    - intros [] ar; cbn. now destruct t. reflexivity.
    - now intros [].
    - cbn. apply find_arity_bound_p_correct.
  Qed.


  Lemma prv1_to_prv2_ExI {ff : falsity_flag} {p' : peirce} A phi (t : FOL.term) :
    List.map toSOLForm A ⊢2 toSOLForm `[t..'] List.map toSOLForm A ⊢2 toSOLForm (∃' ).
  Proof.
    cbn. intros H. apply close_p_ExI with (P := ar match t with FOL.var x var_pred x | _ @pred Σp2' (FalsePred ar) end); cbn.
    apply find_arity_bound_p_correct. apply ExI_i with ( := toSOLTerm t).
    rewrite toSOLForm_subst in H. erewrite subst_ext_i, subst_ext_p_arity_bounded.
    apply H.
    + apply find_arity_bound_p_correct.
    + intros [] ar ; unfold toSOLSub_p, subst_all_below_ar_p; cbn. now destruct t. reflexivity.
    + now intros [].
  Qed.


  Lemma prv1_to_prv2_ExE {ff : falsity_flag} {p' : peirce} A phi psi :
    List.map toSOLForm A ⊢2 toSOLForm (∃' ) List.map toSOLForm ( :: List.map (subst_form ↑') A) ⊢2 toSOLForm `[↑'] List.map toSOLForm A ⊢2 toSOLForm .
  Proof.
    intros . apply subst_Weak_p with ( := toSOLSub_p (var (proj1_sig (find_bounded_L (::::A))))..') in .
    apply subst_Weak_i with ( := toSOLSub_i (var (proj1_sig (find_bounded_L (::::A))))..') in . cbn in .
    erewrite !List.map_map, toSOLForm_subst, subst_shift, List.map_ext with (g := toSOLForm) in ; revgoals.
    { intros . setoid_rewrite toSOLForm_subst. now rewrite subst_shift. }
    setoid_rewrite toSOLForm_subst in .
    cbn in . eapply close_p_ExE_nameless' with (b := proj1_sig (find_bounded_L ( :: :: A))). 4: apply .
    + intros ar ? [ [ ]]%List.in_map_iff. apply toSOLForm_bounded_pred.
      destruct find_bounded_L as [b ]; cbn. apply . firstorder.
    + intros ar . apply toSOLForm_bounded_pred. destruct find_bounded_L as [b ]; cbn.
      apply . firstorder.
    + intros ar . apply toSOLForm_bounded_pred. destruct find_bounded_L as [b ]; cbn.
      apply . firstorder.
    + cbn. eapply ExE_i. apply Ctx. now left. eapply nameless_equiv_ex_i' with (n := proj1_sig (find_bounded_L ( :: :: A))).
      * intros ? [|[ [ ]]%List.in_map_iff].
        -- apply bounded_indi_subst_p. destruct find_bounded_L as [b ]; cbn in *.
           eapply bounded_indi_up. 2: apply toSOLForm_bounded_indi, . lia. firstorder.
        -- destruct find_bounded_L as [b ]; cbn in *. apply toSOLForm_bounded_indi, . firstorder.
      * destruct find_bounded_L as [b ]; cbn in *. apply toSOLForm_bounded_indi, . firstorder.
      * apply bounded_indi_subst_p. destruct find_bounded_L as [b ]; cbn in *.
        eapply bounded_indi_up. 2: apply toSOLForm_bounded_indi, . lia. firstorder.
      * rewrite toSOLForm_subst in . erewrite subst_ext_p_arity_bounded, subst_ext_i.
        eapply Weak. 2: apply . intros ? [|]. now left. firstorder.
        -- now intros [].
        -- apply find_arity_bound_p_correct.
        -- now intros [] ar H; unfold subst_all_below_ar_p; destruct Compare_dec.lt_dec; try lia.
    + now intros [].
  Qed.


  Lemma prv1_to_prv2 {ff : falsity_flag} {p' : peirce} phi A :
    A ⊢1 (List.map toSOLForm A) ⊢2 toSOLForm .
  Proof.
    intros H. induction H.
    - apply II, IHprv.
    - eapply IE. apply . apply .
    - apply prv1_to_prv2_AllI, IHprv.
    - apply prv1_to_prv2_AllE, IHprv.
    - eapply prv1_to_prv2_ExI, IHprv.
    - eapply prv1_to_prv2_ExE. apply . apply .
    - eapply Exp, IHprv.
    - now apply Ctx, List.in_map.
    - apply CI. apply . apply .
    - eapply CE1, IHprv.
    - eapply CE2, IHprv.
    - eapply DI1, IHprv.
    - eapply DI2, IHprv.
    - eapply DE. apply . apply . apply .
  Qed.


Forwards-Backwards Equivalence

Properties of combined fowrards- and backwards-translation

  Lemma toSOLFOLForm_find_arity_bound_p pos_i pos_p pos_i' pos_p' phi :
    find_arity_bound_p (toSOLForm (toFOLForm pos_i pos_p )) = find_arity_bound_p (toSOLForm (toFOLForm pos_i' pos_p' )).
  Proof.
    induction in pos_i, pos_p, pos_i', pos_p' |- *; cbn.
    - reflexivity.
    - now destruct p.
    - now erewrite , .
    - rewrite !close_p_find_arity_bound_p; cbn. apply IHphi.
    - reflexivity.
    - rewrite !close_p_find_arity_bound_p; cbn. apply IHphi.
  Qed.


The pos functions can be moved into a substitution

  Lemma toSOLFOLTerm_pos_i_to_subst t pos_i :
    funcfreeTerm t
     toSOLTerm (toFOLTerm pos_i t) = (toSOLTerm (toFOLTerm ( n n) t))[pos_i >> var_indi]i.
  Proof.
    intros F. induction t; cbn in *.
    - reflexivity.
    - now exfalso.
    - f_equal. rewrite !Vector.map_map. eapply map_ext_forall, Forall_ext_Forall.
      apply IH. apply F.
  Qed.


  Lemma toSOLFOLForm_pos_i_to_subst phi pos_i pos_p :
    funcfree
     toSOLForm (toFOLForm pos_i pos_p ) = (toSOLForm (toFOLForm ( n n) pos_p ))[pos_i >> var_indi]i.
  Proof.
    induction in pos_i, pos_p |-*; cbn; intros F.
    - reflexivity.
    - destruct p; cbn; f_equal; rewrite !Vector.map_map; eapply map_ext_in; intros t H;
      apply toSOLFOLTerm_pos_i_to_subst; eapply Forall_in in F; try apply F; easy.
    - now rewrite , .
    - rewrite close_p_subst_i; cbn. f_equal. f_equal. 2: apply toSOLFOLForm_find_arity_bound_p.
      rewrite IHphi, IHphi with (pos_i := pcons ( n n)); try easy.
      rewrite subst_comp_i. apply subst_ext_i. now intros [].
    - reflexivity.
    - rewrite close_p_subst_i; cbn. f_equal. f_equal. 2: apply toSOLFOLForm_find_arity_bound_p.
      rewrite IHphi, IHphi with (pos_i := pshift ( n n)); try easy.
      rewrite subst_comp_i. apply subst_ext_i. now intros [].
  Qed.


  Lemma toSOLFOLForm_pos_p_to_subst phi pos_i pos_p :
    funcfree
     toSOLForm (toFOLForm pos_i pos_p ) = (toSOLForm (toFOLForm pos_i ( n _ n) ))[ x ar var_pred (pos_p x ar)]p.
  Proof.
    induction in pos_i, pos_p |-*; cbn; intros F.
    - reflexivity.
    - now destruct p.
    - now rewrite , .
    - rewrite close_p_subst_p_bounded; cbn. 2: apply find_arity_bound_p_correct.
      f_equal. f_equal. 2: apply toSOLFOLForm_find_arity_bound_p.
      rewrite IHphi, IHphi with (pos_p := pshift' ( n _ n)); try easy.
      rewrite subst_comp_p. eapply subst_ext_p. intros n ar; cbn. unfold shift, shift_p.
      now rewrite nat_eq_dec_same.
    - reflexivity.
    - rewrite close_p_subst_p_bounded; cbn. 2: apply find_arity_bound_p_correct.
      f_equal. f_equal. 2: apply toSOLFOLForm_find_arity_bound_p.
      rewrite IHphi, IHphi with (pos_p := pcons' n ( n _ n)); try easy.
      rewrite subst_comp_p. eapply subst_ext_p.
      intros [] ar; cbn; destruct PeanoNat.Nat.eq_dec as [|]; cbn; try reflexivity;
      unfold shift, shift_p; now rewrite nat_eq_dec_same.
  Qed.


This allows us to 'undo' pshift and pcons

  Lemma toSOLFOLForm_pshift_subst_i phi pos_i pos_p t :
    funcfree
     (toSOLForm (toFOLForm (pshift pos_i) pos_p ))[t..]i = toSOLForm (toFOLForm pos_i pos_p ).
  Proof.
    intros F. rewrite toSOLFOLForm_pos_i_to_subst, toSOLFOLForm_pos_i_to_subst with (pos_i := pos_i); try easy.
    rewrite subst_comp_i. apply subst_ext_i. now intros [].
  Qed.


  Lemma toSOLFOLForm_pshift_subst_p phi pos_i pos_p P :
    funcfree
     (toSOLForm (toFOLForm pos_i (pshift' pos_p) ))[P,,]p = toSOLForm (toFOLForm pos_i pos_p ).
  Proof.
    intros F. rewrite toSOLFOLForm_pos_p_to_subst, toSOLFOLForm_pos_p_to_subst with (pos_p := pos_p); try easy.
    rewrite subst_comp_p. apply subst_ext_p. now intros [] ar.
  Qed.


  Lemma toSOLFOLForm_pcons_subst_p phi pos_i pos_p x n :
    funcfree
     ( n ar, pos_p n ar = n)
     (toSOLForm (toFOLForm pos_i (pcons' n pos_p) ))[(@var_pred _ x),,]p = (toSOLForm (toFOLForm pos_i pos_p ))[(var_pred x n)..]p.
  Proof.
    intros F. revert pos_p. enough ( pos_p, ( x ar, pos_p x ar = x) (toSOLForm (toFOLForm pos_i (pcons' n pos_p) ))[(@var_pred _ x),,]p = (toSOLForm (toFOLForm pos_i pos_p ))[(var_pred x n)..]p) as X.
    { intros pos_p H. erewrite toFOLForm_ext_p with (pos_p' := pcons' n ( x _ x)), toFOLForm_ext_p with (pos_p:=pos_p).
      apply X. reflexivity. intros ? ? _; apply H. intros [] ar; cbn; destruct PeanoNat.Nat.eq_dec. reflexivity.
      all: rewrite H; try easy. }
    intros pos_p Hp. rewrite toSOLFOLForm_pos_p_to_subst, toSOLFOLForm_pos_p_to_subst with (pos_p := pos_p); try easy.
    rewrite !subst_comp_p. apply subst_ext_p. intros [] ar; cbn;
    destruct PeanoNat.Nat.eq_dec as [|]; cbn; rewrite !Hp; cbn;
    try rewrite nat_eq_dec_same; try destruct PeanoNat.Nat.eq_dec; try lia; reflexivity.
  Qed.


⊢2 proves the translation equivalent to the intitial formula

  Lemma toSOLFOLTerm_id pos_i t :
    funcfreeTerm t
     ( n, pos_i n = n)
     toSOLTerm (toFOLTerm pos_i t) = t.
  Proof.
    intros F H. induction t; cbn.
    - rewrite H. reflexivity.
    - now exfalso.
    - f_equal. rewrite Vector.map_map, Vector.map_id.
      eapply map_ext_forall, Forall_ext_Forall. apply IH. apply F.
  Qed.


  Lemma toSOLFOLForm_equiv {p' : peirce} phi pos_i pos_p :
    funcfree
     ( n, pos_i n = n)
     ( n ar, pos_p n ar = n)
     List.nil ⊢2 (removeFalsePred (toSOLForm (toFOLForm pos_i pos_p ))) <--> .
  Proof.
    revert pos_i pos_p.
    enough ( pos_i pos_p, funcfree ( n, pos_i n = n) ( n ar, pos_p n ar = n) List.nil ⊢2 (removeFalsePred (toSOLForm (toFOLForm pos_i pos_p ))) <--> ) as X.
    { intros pos_i pos_p F Hi Hp. erewrite toFOLForm_ext_i, toFOLForm_ext_p; trivial. now apply X. }
    intros pos_i pos_p. induction in pos_i, pos_p |-*; intros F Hi Hp; cbn.
    - now apply CI; apply II; apply Ctx.
    - destruct p; cbn.
      + rewrite Hp. rewrite Vector.map_map. erewrite VectorLib.map_ext_in, Vector.map_id.
        now apply CI; apply II; apply Ctx. intros t H. apply toSOLFOLTerm_id.
        eapply Forall_in in F. apply F. easy. apply Hi.
      + rewrite Vector.map_map. erewrite VectorLib.map_ext_in, Vector.map_id.
        now apply CI; apply II; apply Ctx. intros t H. apply toSOLFOLTerm_id.
        eapply Forall_in in F. apply F. easy. apply Hi.
    - rewrite toSOLBinop_toFOLBinop. apply prv_equiv_bin.
      apply ; firstorder. apply ; firstorder.
    - rewrite removeFalsePred_close_p; destruct q; cbn.
      + apply CI.
        * apply II. eapply IE. eapply CE1. eapply Weak with (A := List.nil). easy.
          apply prv_equiv_quant_i. eapply IHphi with (pos_i := pcons pos_i) (pos_p := pos_p); try easy.
          intros []; cbn. reflexivity. now rewrite Hi.
          erewrite toSOLFOLForm_pshift_subst_p with (pos_p := pos_p) (P := @var_pred _ 0), removeFalsePred_subst_p with ( := (@var_pred _ 0),,); try easy.
          change (i (removeFalsePred (toSOLForm (toFOLForm (pcons pos_i) (pshift' pos_p) )))[(@var_pred _ 0),,]p) with ((i (removeFalsePred (toSOLForm (toFOLForm (pcons pos_i) (pshift' pos_p) ))))[(@var_pred _ 0),,]p).
          eapply close_p_AllE; revgoals. now apply Ctx. apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct.
          intros [] ar; left; now eexists.
        * apply II. edestruct (@close_p_AllI_nameless _ Σp2) as [x X]. 2: apply X; clear X.
          apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct. cbn.
          rewrite removeFalsePred_subst_p with ( := (@var_pred _ x),,), toSOLFOLForm_pshift_subst_p; try easy.
          eapply IE. eapply CE2. eapply Weak with (A := List.nil). easy. apply prv_equiv_quant_i, IHphi; try easy.
          intros []; cbn. reflexivity. now rewrite Hi. now apply Ctx. intros [] ar; left; now eexists.
      + apply CI.
        * apply II. eapply IE. eapply CE1. eapply Weak with (A := List.nil). easy.
          apply prv_equiv_quant_i. eapply IHphi with (pos_i := pcons pos_i) (pos_p := pos_p); try easy.
          intros []; cbn. reflexivity. now rewrite Hi.
          edestruct (@close_p_ExE_nameless _ Σp2) as [x X]; revgoals. apply X; clear X.
          erewrite toSOLFOLForm_pshift_subst_p with (pos_p := pos_p) (P := @var_pred _ x), removeFalsePred_subst_p with ( := (@var_pred _ x),,); try easy.
          change (i (removeFalsePred (toSOLForm (toFOLForm (pcons pos_i) (pshift' pos_p) )))[(@var_pred _ x),,]p) with ((i (removeFalsePred (toSOLForm (toFOLForm (pcons pos_i) (pshift' pos_p) ))))[(@var_pred _ x),,]p).
          apply Ctx; now left. intros [] ar; left; now eexists. now apply Ctx.
          apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct.
        * apply II. apply close_p_ExI with (P := @var_pred _ 0).
          apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct. cbn.
          rewrite removeFalsePred_subst_p with ( := (@var_pred _ 0),,), toSOLFOLForm_pshift_subst_p; try easy.
          eapply IE. eapply CE2. eapply Weak with (A := List.nil). easy. apply prv_equiv_quant_i, IHphi; try easy.
          intros []; cbn. reflexivity. now rewrite Hi. now apply Ctx. intros [] ar; left; now eexists.
    - now exfalso.
    - rewrite removeFalsePred_close_p; destruct q; cbn.
      + apply CI.
        * apply II. apply AllI_p. edestruct (@nameless_equiv_all_p _ Σp2) as [x ].
          eapply IE. eapply CE1. eapply Weak with (A := List.nil). easy.
          apply prv_equiv_subst_p, IHphi with (pos_i := pos_i) (pos_p := pos_p); try easy.
          rewrite removeFalsePred_subst_p with ( := (var_pred x n)..).
          rewrite toSOLFOLForm_pcons_subst_p, toSOLFOLForm_pshift_subst_i with (pos_i := pos_i) (t := var_indi 0); try easy.
          rewrite removeFalsePred_subst_p with ( := (@var_pred _ x),,), removeFalsePred_subst_i, subst_switch_i_p.
          apply AllE_i. change (i (removeFalsePred (toSOLForm (toFOLForm (pshift pos_i) (pcons' n pos_p) )))[(@var_pred _ x),,]p) with ((removeFalsePred (i (toSOLForm (toFOLForm (pshift pos_i) (pcons' n pos_p) ))))[(@var_pred _ x),,]p).
          eapply close_p_AllE; revgoals. now apply Ctx.
          cbn. apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct.
          intros [] ar; left; now eexists. intros [] ar; left; cbn; destruct PeanoNat.Nat.eq_dec as [|]; now eexists.
        * apply II. edestruct (@close_p_AllI_nameless _ Σp2) as [x X]. 2: apply X; clear X.
          apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct. cbn.
          rewrite removeFalsePred_subst_p with ( := (@var_pred _ x),,), toSOLFOLForm_pcons_subst_p; try easy.
          apply AllI_i. edestruct (@nameless_equiv_all_i _ Σp2) as [y ].
          rewrite removeFalsePred_subst_i, subst_switch_i_p, toSOLFOLForm_pshift_subst_i; try easy.
          rewrite removeFalsePred_subst_p with ( := (var_pred x n)..).
          eapply IE. eapply CE2. eapply Weak with (A := List.nil). easy. apply prv_equiv_subst_p, IHphi; try easy.
          now apply AllE_p, Ctx. intros [] ar; left; cbn; destruct PeanoNat.Nat.eq_dec as [|]; now eexists.
          intros [] ar; left; now eexists.
      + apply CI.
        * apply II. edestruct (@close_p_ExE_nameless _ Σp2) as [x X]. 3: apply X; clear X. 2: now apply Ctx.
          cbn. apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct.
          eapply ExE_i. apply Ctx; cbn; now left. edestruct (@nameless_equiv_ex_i _ Σp2) as [y ].
          apply ExI_p with (P := var_pred x).
          eapply IE. eapply CE1. eapply Weak with (A := List.nil). easy. apply prv_equiv_subst_p, IHphi; try easy.
          rewrite removeFalsePred_subst_p with ( := (var_pred x n)..) ( := (var_pred x n)..).
          rewrite toSOLFOLForm_pcons_subst_p, toSOLFOLForm_pshift_subst_i with (pos_i := pos_i) (t := y); try easy.
          rewrite removeFalsePred_subst_p with ( := (@var_pred _ x),,), removeFalsePred_subst_i, subst_switch_i_p.
          now apply Ctx. intros [] ar; left; now eexists.
          intros [] ar; left; cbn; destruct PeanoNat.Nat.eq_dec as [|]; now eexists.
        * apply II. eapply ExE_p. now apply Ctx. edestruct (@nameless_equiv_ex_p _ Σp2) as [x ].
          apply close_p_ExI with (P := @var_pred _ x); cbn. apply removeFalsePred_arity_bounded_p, find_arity_bound_p_correct.
          apply ExI_i with (t := var_indi 0).
          rewrite subst_switch_i_p, removeFalsePred_subst_i, removeFalsePred_subst_p with ( := (@var_pred _ x),,).
          rewrite toSOLFOLForm_pshift_subst_i, toSOLFOLForm_pcons_subst_p; try easy.
          rewrite removeFalsePred_subst_p with ( := (var_pred x n)..).
          eapply IE. eapply CE2. eapply Weak with (A := List.nil). easy. apply prv_equiv_subst_p, IHphi; try easy.
          now apply Ctx. intros [] ar; left; cbn; destruct PeanoNat.Nat.eq_dec as [|]; now eexists.
          intros [] ar; left; now eexists.
  Qed.


  Definition initial_pos_i_inv n := n.
  Definition initial_pos_p_inv n := ( n).

  Lemma initial_pos_i_inv_correct :
     n, initial_pos_i_inv (initial_pos_i n) = n.
  Proof.
    intros n. unfold initial_pos_i_inv, initial_pos_i. now rewrite pi2_correct.
  Qed.


  Lemma initial_pos_p_inv_correct :
     n ar, initial_pos_p_inv (initial_pos_p n ar) = n.
  Proof.
    intros n ar. unfold initial_pos_p_inv, initial_pos_p. now rewrite pi2_correct, pi1_correct.
  Qed.


  Lemma initial_pos_i_inv_subst phi :
    [initial_pos_i >> var_indi]i[initial_pos_i_inv >> var_indi]i = .
  Proof.
    rewrite subst_comp_i, subst_id_i. apply subst_ext_i. intros n; cbn.
    now rewrite initial_pos_i_inv_correct.
  Qed.


  Lemma initial_pos_p_inv_subst phi :
    [ x ar var_pred (initial_pos_p x ar)]p[ x ar var_pred (initial_pos_p_inv x)]p = .
  Proof.
    rewrite subst_comp_p, subst_id_p. apply subst_ext_p. intros n ar; cbn.
    now rewrite initial_pos_p_inv_correct.
  Qed.


  Definition toSOLForm' {ff : falsity_flag} phi := (toSOLForm )[ x ar var_pred (initial_pos_p_inv x)]p[initial_pos_i_inv >> var_indi]i.

  Lemma toSOLFOLForm'_correct phi :
    funcfree toSOLForm' (toFOLForm' ) = toSOLForm (toFOLForm ( n n) ( n ar n) ).
  Proof.
    intros F. unfold toFOLForm', toSOLForm'.
    rewrite toSOLFOLForm_pos_p_to_subst, toSOLFOLForm_pos_i_to_subst; trivial.
    now rewrite initial_pos_p_inv_subst, initial_pos_i_inv_subst.
  Qed.


  Lemma toSOLFOLForm_equiv' {p' : peirce} phi :
    funcfree List.nil ⊢2 (removeFalsePred (toSOLForm' (toFOLForm' ))) <--> .
  Proof.
    intros F. unfold toFOLForm', toSOLForm'.
    rewrite toSOLFOLForm_pos_p_to_subst, toSOLFOLForm_pos_i_to_subst; trivial.
    rewrite initial_pos_p_inv_subst, initial_pos_i_inv_subst. now apply toSOLFOLForm_equiv.
  Qed.


  Lemma prv1_to_prv2' {ff : falsity_flag} {p' : peirce} phi A :
    A ⊢1 List.map removeFalsePred (List.map toSOLForm' A) ⊢2 removeFalsePred (toSOLForm' ).
  Proof.
    intros H. apply prv_removeFalsePred. unfold toSOLForm'.
    rewrite List.map_map. apply subst_Weak_i. easy.
    rewrite List.map_map. apply subst_Weak_p.
    now apply prv1_to_prv2.
  Qed.


Final Provability Reduction


  Existing Instance Σp2.

  Definition {ff : falsity_flag} (T : FOL.form Prop) phi := A, ( psi, List.In A T ) A ⊢1 .
  Definition {p' : peirce} (T : SOL.form Prop) phi := A, ( psi, List.In A T ) A ⊢2 .

  Notation "T ⊩1 phi" := ( T ) (at level 61).
  Notation "T ⊩2 phi" := ( T ) (at level 61).

  Lemma prv_ext {p' : peirce} phi A1 A2 :
     ⊢2 ( psi, List.In ⊢2 ) ⊢2 .
  Proof.
    induction in |-*; cbn; intros .
    - eapply Weak. 2: apply . easy.
    - eapply IE. apply .
      + apply II, .
      + intros ? ?. apply . auto.
      + apply . auto.
  Qed.


  Lemma tprv_ext {p' : peirce} phi (T1 T2 : form Prop) :
     ⊩2 ( psi, ⊩2 ) ⊩2 .
  Proof.
    intros [A [ ]] . revert A . induction A in , |-*; intros .
    - now exists List.nil.
    - enough ( ⊩2 a --> ) as [ X].
      { destruct ( a) as []. now apply . exists (List.app ). split.
        - intros ? [|]%List.in_app_iff. now apply X. now apply H.
        - eapply IE; eapply Weak. 2: apply X. apply List.incl_appl, List.incl_refl.
          2: apply H. apply List.incl_appr, List.incl_refl. }
      apply (IHA _ ).
      + intros ? ?. apply . auto.
      + now apply II.
      + apply .
  Qed.


  Lemma prv_closed_comprehension {p' : peirce} ar phi :
    funcfree List.nil ⊢2 close All (comprehension_form ar ).
  Proof.
    intros F. unfold close, close_indi. destruct find_bounded_indi as [n B]; cbn.
    clear B. induction n; cbn.
    - enough ( m, List.nil ⊢2 close_pred'' m All (comprehension_form ar )) by easy.
      induction m; cbn. apply Comp. apply F. unfold close_pred'. destruct find_bounded_pred as [k B]; cbn.
      clear B. induction k; cbn. easy. now apply AllI_p.
    - now apply AllI_i.
  Qed.


  Lemma prv_if_firstorder_prv {p' : peirce} (T : SOL.form Prop) phi :
    funcfree ( psi, T funcfree ) toFOLTheory (T C) ⊩1 (toFOLForm' ) T ⊩2 .
  Proof.
    intros F TF.
    intros [A [HT H%prv1_to_prv2']]. apply tprv_ext with ( := T C).
    apply tprv_ext with ( := phi psi, = removeFalsePred (toSOLForm' (toFOLForm' )) (T C) ).
    + exists (List.map removeFalsePred (List.map toSOLForm' A)). split.
      * intros [ [ [ [ ]]%List.in_map_iff]]%List.in_map_iff.
        destruct (HT ) as [ [ [|]]]. easy. all: exists ; auto.
      * eapply IE. eapply CE1, Weak. 2: apply toSOLFOLForm_equiv'. all: easy.
    + intros ? [ [ [|[? [? [? ]]]]]]. exists (List.cons List.nil). split.
      * intros ? [|[]]. auto.
      * eapply IE. eapply CE2, Weak. 2: apply toSOLFOLForm_equiv'. easy.
        now apply TF. now apply Ctx.
      * exists List.nil. split. easy. eapply IE. eapply CE2, toSOLFOLForm_equiv'.
        now apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree.
        now apply prv_closed_comprehension.
    + intros [|[? [? [? ]]]].
      * exists (List.cons List.nil). split. intros ? [|[]]. auto. now apply Ctx.
      * exists List.nil. split. easy. now apply prv_closed_comprehension.
  Qed.


Consequences of Reduction

Completeness


  Section Completeness.

    Hypothesis prv1_complete : {ff : falsity_flag} T phi, validFO T T ⊩1 .

    Theorem Completeness {p' : peirce} (T : SOL.form Prop) phi :
      funcfree ( psi, T funcfree ) Henkin.validT T T ⊩2 .
    Proof.
      intros F TF H.
      apply prv_if_firstorder_prv; trivial.
      apply prv1_complete, henkin_valid_iff_firstorder_valid; trivial.
    Qed.


    Existing Instance intu.

    Lemma first_order_prv_if_prv_I (T : SOL.form Prop) phi :
      funcfree ( psi, T funcfree ) T ⊩2 toFOLTheory (T C) ⊩1 (toFOLForm' ).
    Proof.
      intros F TF. intros H.
      apply prv1_complete, henkin_valid_iff_firstorder_valid; trivial.
      now apply Deduction.HenkinSoundnessIT.
    Qed.


    Theorem prv_iff_firstorder_prv_I (T : SOL.form Prop) phi :
      funcfree ( psi, T funcfree ) toFOLTheory (T C) ⊩1 (toFOLForm' ) T ⊩2 .
    Proof.
      intros F TF. split.
      - now apply prv_if_firstorder_prv.
      - now apply first_order_prv_if_prv_I.
    Qed.


    Existing Instance class.

    Lemma first_order_prv_if_prv_C (T : SOL.form Prop) phi :
      LEM funcfree ( psi, T funcfree ) T ⊩2 toFOLTheory (T C) ⊩1 (toFOLForm' ).
    Proof.
      intros lem F TF. intros H.
      apply prv1_complete, henkin_valid_iff_firstorder_valid; trivial.
      now apply Deduction.HenkinSoundnessCT.
    Qed.


    Theorem prv_iff_firstorder_prv_C (T : SOL.form Prop) phi :
      LEM funcfree ( psi, T funcfree ) toFOLTheory (T C) ⊩1 (toFOLForm' ) T ⊩2 .
    Proof.
      intros lem F TF. split.
      - now apply prv_if_firstorder_prv.
      - now apply first_order_prv_if_prv_C.
    Qed.


  End Completeness.

Compactness


  Existing Instance FOL.falsity_on.

  Definition has_henkin_model_with P (T : form Prop) :=
     D (I : interp D) funcs preds,
      P D henkin_interp I funcs preds
       ( rho, ( x ar, preds ar (get_pred x ar)) ( ar phi, funcfree Henkin.sat funcs preds (comprehension_form ar )))
       rho, henkin_env funcs preds
           phi, T Henkin.sat funcs preds .

  Definition has_firstorder_model_with (P : Type Prop) (T : FOL.form Prop) :=
       D I rho, P D phi, T @FOL.sat _ _ D I _ .

  Definition has_henkin_model := has_henkin_model_with ( _ True).
  Definition has_firstorder_model := has_firstorder_model_with ( _ True).

  Lemma has_firstorder_model_with_ext (T T' : FOL.form Prop) P :
    ( phi, T' T ) has_firstorder_model_with P T has_firstorder_model_with P T'.
  Proof.
    intros HT [D [I [ [ ]]]]. exists D, I, . split. easy. intros . apply , HT, .
  Qed.


  Lemma has_henkin_model_with_ext (T T' : form Prop) (P P' : Type Prop) :
    ( phi, T' T ) ( D, P D P' D) has_henkin_model_with P T has_henkin_model_with P' T'.
  Proof.
    intros HT HP [D [I [funcs [preds [HDP [HI [HCompr [ [Hrho ]]]]]]]]].
    exists D, I, funcs, preds. split. now apply HP. split. easy. split. easy.
    exists . split. easy. intros . apply , HT, .
  Qed.


  Lemma has_henkin_model_compr T P :
    has_henkin_model_with P T has_henkin_model_with P (T C).
  Proof.
    intros [D [I [funcs [preds [HP [HI [HCompr [ [Hrho H]]]]]]]]].
    exists D, I, funcs, preds. split. easy. split. easy. split. easy.
    exists . split. easy. intros [|[? [? [? ]]]].
    - now apply H.
    - apply close_sat_funcfree. now apply comprehension_form_funcfree.
      apply Hrho. intros . now apply HCompr.
  Qed.


  Lemma theory_has_firstorder_model_if_theory_has_henkin_model (T : form Prop) (P P' : Type Prop) :
    ( phi, T funcfree )
     ( D preds, P D P' ( D preds) : Prop)
     has_henkin_model_with P T
     has_firstorder_model_with P' (toFOLTheory T).
  Proof.
    intros TF HP [D [I [funcs [preds [HDP [HI [HCompr [ [Hrho ]]]]]]]]].
    do 3 eexists. split. apply (HP D). apply HDP. intros [ [ ]].
    unshelve eapply toFOLForm_correct_2To1 with ( := ) ( := toFOLEnv _ funcs preds Hrho) (funcs := funcs) (preds := preds).
    - exact (get_indi 0).
    - intros ar. exists (get_pred 0 ar). apply Hrho.
    - now apply TF.
    - intros n. unfold initial_pos_i, toFOLEnv. now rewrite unembed_embed.
    - intros n ar. unfold initial_pos_p, toFOLEnv. rewrite unembed_embed, pi1_correct, pi2_correct.
      cbn. now rewrite nat_eq_dec_same.
    - now apply .
  Qed.


  Lemma theory_has_henkin_model_if_theory_has_firstorder_model (T : form Prop) (P : Type Prop) :
    ( phi, T funcfree )
     has_firstorder_model_with P (toFOLTheory (T C))
     has_henkin_model_with P T.
  Proof.
    intros TF [D [I [ [HDP ]]]]. exists ( D). do 3 eexists. split.
    easy. split; revgoals. split; revgoals.
    exists (toSOLEnv _ ). split; revgoals. intros .
    eapply toFOLForm_correct_1To2. 4: apply ( (toFOLForm' )).
    - now apply TF.
    - reflexivity.
    - reflexivity.
    - eexists. split. reflexivity. now left.
    - apply toSOLEnv_henkin_env.
    - intros ar F. eapply close_sat_funcfree with ( := toSOLEnv _ ).
      apply comprehension_form_funcfree, F. cbn. unfold preds. eexists. reflexivity.
      eapply toFOLForm_correct_1To2.
      4: apply ( (toFOLForm' (close All (comprehension_form ar )))).
      + apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree, F.
      + reflexivity.
      + reflexivity.
      + eexists. split. reflexivity. right. eexists. eexists. split. apply F. reflexivity.
      + apply .
    - eapply constructed_henkin_interp_correct with ( := toSOLEnv _ ).
      + intros x ar. eexists. cbn. reflexivity.
      + intros [? [? [F ]]]. eapply toFOLForm_correct_1To2. 4: apply .
        * apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree, F.
        * reflexivity.
        * cbn. reflexivity.
        * eexists. split. reflexivity. right. eexists. eexists. split. apply F. reflexivity.
  Qed.


  Section CompactnessByCompleteness.

    Hypothesis prv1_complete : {ff : falsity_flag} T phi, validFO T T ⊩1 .

    Theorem Compactness_by_Completeness {p : peirce} :
      LEM (T : form Prop), ( phi, T funcfree ) has_henkin_model T A, ( phi, List.In A T ) has_henkin_model ( phi List.In A).
    Proof.
      intros lem T TF. split.
      - intros A . eapply has_henkin_model_with_ext. 3: apply . easy. easy.
      - intros . enough ( T ) as HT.
        { edestruct lem as [X|H]. apply X. exfalso. apply HT.
          apply Completeness; cbn; trivial. intros D I funcs preds HI HC Hrho .
          apply H. exists D, I, funcs, preds. split. easy. split. easy. split. easy.
          exists . split. easy. easy. }
        intros [A [ ]]. destruct p.
        + apply HenkinSoundnessC in ; trivial.
          destruct ( A) as [D [I [funcs [preds [HDP [HI [HCompr [ [Hrho ]]]]]]]]]; trivial.
          eapply ; eauto.
        + apply HenkinSoundnessI in .
          destruct ( A) as [D [I [funcs [preds [HDP [HI [HCompr [ [Hrho ]]]]]]]]]; trivial.
          eapply ; eauto.
    Qed.


  End CompactnessByCompleteness.

  Section CompactnessByReduction.

    Lemma theory_decompose (T1 T2 : form Prop) A :
      ( phi, List.In A ( ) ) B1 B2, ( phi, List.In List.In A ) ( phi, List.In List.In A ) ( phi, List.In A List.In List.In ).
    Proof.
      intros H. induction A; cbn.
      - exists List.nil, List.nil. firstorder.
      - destruct IHA as [ [ [ [ ]]]]. firstorder. destruct (H a) as [|]; trivial.
        + exists (List.cons a ), . split. 2: split.
          * clear - . intros [|]; firstorder.
          * clear -. firstorder.
          * clear -. intros ? [|]; firstorder.
        + exists , (List.cons a ). split. 2: split.
          * clear -. firstorder.
          * clear - . intros [|]; firstorder.
          * clear -. intros ? [|]; firstorder.
    Qed.


    Hypothesis FOL_compact :
       (T : FOL.form Prop), has_firstorder_model T A, ( phi, List.In A T ) has_firstorder_model ( phi List.In A).

    Theorem Compactness :
       (T : form Prop), ( phi, T funcfree ) has_henkin_model T A, ( phi, List.In A T ) has_henkin_model ( phi List.In A).
    Proof.
      intros T TF. split.
      - intros [D [I [funcs [preds [_ [HI [HCompr [ [Hrho ]]]]]]]]] A .
        exists D, I, funcs, preds. split. easy. split. easy. split. easy. exists .
        split. easy. intros . apply , , .
      - intros . apply theory_has_henkin_model_if_theory_has_firstorder_model; trivial.
        apply FOL_compact. intros A .
        assert ( B, A = List.map toFOLForm' B phi, List.In B T C ) as [B [ HB]].
        { clear -. induction A; cbn. now exists List.nil.
          destruct IHA as [B [ ]]; firstorder. destruct ( a) as [ [ ]]; trivial.
          exists (List.cons B). split. reflexivity. intros [|]. easy. now apply . }
        destruct (theory_decompose T C B) as [BT [BC [ [ ]]]]; trivial.
        apply has_firstorder_model_with_ext with (T := toFOLTheory ( phi List.In B)).
        intros ? [? [ ?]]%List.in_map_iff. eexists. split. reflexivity. easy.
        eapply theory_has_firstorder_model_if_theory_has_henkin_model with (P := _ True).
        { intros [[]% | [? [? [? [? ]]]]%]%. now apply TF.
          now apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree. }
        easy. destruct ( BT) as [D [I [funcs [preds [_ [HI [HCompr [ [Hrho ]]]]]]]]]. apply .
        exists D, I, funcs, preds. split. easy. split. easy. split. easy. exists . split. easy.
        intros [|[ [? [? [ ]]]]%]%.
        + now apply .
        + apply close_sat_funcfree. now apply comprehension_form_funcfree.
          apply Hrho. intros . now apply HCompr.
    Qed.


  End CompactnessByReduction.

Löwenheim-Skolem


  Section LöwenheimSkolem.

    Definition injects X Y := f : X Y, x x', f x = f x' x = x'.
    Definition infinite X := injects X.
    Definition same_cardinality X Y := injects X Y injects Y X.

    Hypothesis FOL_LöwenheimSkolem :
       T, has_firstorder_model_with infinite T X, infinite X has_firstorder_model_with (same_cardinality X) T.

    Theorem LöwenheimSkolem (T : form Prop) :
      ( phi, T funcfree ) has_henkin_model_with infinite T X, infinite X has_henkin_model_with (same_cardinality X) T.
    Proof.
      intros TF H X HX.
      apply theory_has_henkin_model_if_theory_has_firstorder_model; trivial.
      apply FOL_LöwenheimSkolem; trivial.
      apply theory_has_firstorder_model_if_theory_has_henkin_model with (P := infinite).
      - intros [|[? [? [? ]]]]. now apply TF.
        now apply close_indi_funcfree, close_pred_funcfree, comprehension_form_funcfree.
      - intros D preds [f Hf]. exists ( n fromIndi D preds (f n)).
        intros x x' . apply Hf. congruence.
      - apply has_henkin_model_compr. apply H.
    Qed.


  End LöwenheimSkolem.

End Signature.