Second-Order Peano Arithmetic


Require Import SOL.
Require Import FullSyntax.
Require Import Subst.
Require Import Tarski.
Require Import Vector.
Import VectorNotations.
Require Import VectorLib.
Require Import Decidable Enumerable.
Require Import Util.
Import SubstNotations.

Require Import Equations.Equations Equations.Prop.DepElim.
Derive Signature for Vector.t.
Derive Signature for function.
Derive Signature for predicate.
Require Import Lia.
Require Import PeanoNat.

Inductive PA_funcs : Type := Zero | Succ | Plus | Mult.
Definition PA_funcs_ar (f : PA_funcs ) :=
  match f with
  | Zero 0
  | Succ 1
  | Plus 2
  | Mult 2
  end.

Inductive PA_preds : Type := Eq : PA_preds.
Definition PA_preds_ar (P : PA_preds) := match P with Eq 2 end.

Instance PA_funcs_signature : funcs_signature :=
{| syms := PA_funcs ; ar_syms := PA_funcs_ar |}.

Instance PA_preds_signature : preds_signature :=
{| preds := PA_preds ; ar_preds := PA_preds_ar |}.

Arguments Vector.cons {_} _ {_} _, _ _ _ _.
Definition zero := func (sym Zero) ([]).
Notation "'σ' x" := (func (sym Succ) ([x])) (at level 37).
Notation "x '⊕' y" := (func (sym Plus) ([x ; y])) (at level 39).
Notation "x '⊗' y" := (func (sym Mult) ([x ; y])) (at level 38).
Notation "x '==' y" := (atom (pred Eq) ([x ; y])) (at level 40).

With concrete instances for functions and predicates we get a real equality decider.

Instance PA_funcs_signature_eq_dec :
  Decidable.eq_dec PA_funcs_signature.
Proof.
  intros x y. unfold dec. decide equality.
Qed.


Instance PA_preds_signature_eq_dec :
  Decidable.eq_dec PA_preds_signature.
Proof.
  intros [] []. now left.
Qed.


Definition L_PA_funcs (n : ) := List.cons Zero (List.cons Succ (List.cons Plus (List.cons Mult List.nil))).
Definition L_PA_preds (n : ) := List.cons Eq List.nil.

Instance PA_funcs_enum :
  list_enumerator__T L_PA_funcs PA_funcs.
Proof.
  intros []; exists 0; firstorder.
Qed.


Instance PA_preds_enum :
  list_enumerator__T L_PA_preds PA_preds.
Proof.
  intros []; exists 0; firstorder.
Qed.


Lemma PA_form_enumerable :
  enumerable__T form.
Proof.
  apply form_enumerable.
  - apply list_enumerable__T_enumerable. exists L_PA_funcs. apply PA_funcs_enum.
  - apply list_enumerable__T_enumerable. exists L_PA_preds. apply PA_preds_enum.
  - apply enumT_binop.
  - apply enumT_quantop.
Qed.


Axioms


Section Model.

  Definition ax_eq_refl := i $0 == $0.
  Definition ax_eq_symm := i i $1 == $0 --> $0 == $1.
  Definition ax_eq_trans := i i i $2 == $1 --> $1 == $0 --> $2 == $0.
  Definition ax_zero_succ := i zero == σ $0 --> fal.
  Definition ax_succ_inj := i i σ $1 == σ $0 --> $1 == $0.
  Definition ax_add_zero := i zero $0 == $0.
  Definition ax_add_rec := i i (σ $0) $1 == σ ($0 $1).
  Definition ax_mul_zero := i zero $0 == zero.
  Definition ax_mul_rec := i i σ $1 $0 == $0 $1 $0.
  Definition ax_ind := p(1) p$0 ([zero]) --> (i p$0 ([$0]) --> p$0 ([σ $0])) --> i p$0 ([$0]).

  Import List ListNotations.
  Definition PA_L := [ ax_eq_refl ; ax_eq_symm ; ax_zero_succ ; ax_succ_inj ; ax_add_zero ; ax_add_rec ; ax_mul_zero ; ax_mul_rec ; ax_ind ].
  Definition PA phi := In PA_L.
  Import VectorNotations.

  Lemma PA_enumerable :
    enumerable PA.
  Proof.
    exists ( n nth n (map Some PA_L) None). intros . split.
    - intros H. repeat destruct H as [|H].
      now exists 0. now exists 1. now exists 2. now exists 3. now exists 4.
      now exists 5. now exists 6. now exists 7. now exists 8. easy.
    - intros [n H]. assert ( x y : form, Some x = Some y x = y) as Some_inj by congruence.
      do 9 try destruct n as [|n]; try apply Some_inj in H as . 1-9: firstorder.
      destruct n; cbn in H; congruence.
  Qed.


  Definition empty_PA_env M : env (M_domain M) := n i_f (M_domain M) Zero ([]) , n ar v i_f (M_domain M) Zero ([]), n ar v True .

  Variable PA_M : Model_of PA.

  Notation "'izero'" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Zero ([])).
  Notation "'iσ' x" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Succ ([x])) (at level 37).
  Notation "x 'i⊕' y" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Plus ([x ; y])) (at level 39).
  Notation "x 'i⊗' y" := (@i_f _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Mult ([x ; y])) (at level 38).
  Notation "x 'i==' y" := (@i_P _ _ (M_domain (M_model PA_M)) (M_interp (M_model PA_M)) Eq ([x ; y])) (at level 40).

  Lemma eq_reflexive x :
    x i== x.
  Proof. revert x. apply (M_correct PA_M ax_eq_refl ltac:(firstorder) (empty_PA_env _)). Qed.

  Lemma eq_symm x y :
    x i== y y i== x.
  Proof. apply (M_correct PA_M ax_eq_symm ltac:(firstorder) (empty_PA_env _)). Qed.

  Lemma zero_succ' x :
    izero i== iσ x False.
  Proof. apply (M_correct PA_M ax_zero_succ ltac:(firstorder) (empty_PA_env _)). Qed.

  Lemma succ_inj' x y :
    iσ x i== iσ y x i== y.
  Proof. apply (M_correct PA_M ax_succ_inj ltac:(firstorder) (empty_PA_env _)). Qed.

Simplify induction axiom by removing the vector
  Lemma induction (P : M_domain PA_M Prop) :
    P izero ( x, P x P (iσ x)) x, P x.
  Proof.
    pose (P' := v : vec _ 1 P (Vector.hd v)).
    change (P' ([izero]) ( x, P' ([x]) P' ([iσ x])) x, P' ([x])).
    apply (M_correct PA_M ax_ind ltac:(firstorder) (empty_PA_env _)).
  Qed.


  Lemma case_analysis x :
    x = izero x', x = iσ x'.
  Proof.
    revert x. apply induction.
    - now left.
    - intros x _. right. now exists x.
  Qed.


  Lemma eq_sem x y :
    x i== y x = y.
  Proof.
    split.
    - revert x y. apply (induction ( x y, x i== y x = y)).
      + intros y H. destruct (case_analysis y) as [|[y' ]].
        * reflexivity.
        * now apply zero_succ' in H.
      + intros x IH y H. destruct (case_analysis y) as [|[y' ]].
        * now apply eq_symm, zero_succ' in H.
        * rewrite (IH y'). reflexivity. now apply succ_inj'.
    - intros . apply eq_reflexive.
  Qed.


  Lemma zero_succ x :
    izero = iσ x False.
  Proof. intros H%eq_sem. now apply (zero_succ' x). Qed.

  Lemma succ_inj x y :
    iσ x = iσ y x = y.
  Proof. intros H%eq_sem. now apply eq_sem, (succ_inj' x y). Qed.

  Lemma add_zero x :
    izero i x = x.
  Proof. apply eq_sem, (M_correct PA_M ax_add_zero ltac:(firstorder) (empty_PA_env _)). Qed.

  Lemma add_rec x y :
    iσ x i y = iσ (x i y).
  Proof. apply eq_sem, (M_correct PA_M ax_add_rec ltac:(firstorder) (empty_PA_env _)). Qed.

  Lemma mul_zero x :
    izero i x = izero.
  Proof. apply eq_sem, (M_correct PA_M ax_mul_zero ltac:(firstorder) (empty_PA_env _)). Qed.

  Lemma mul_rec x y :
    iσ x i y = y i (x i y).
  Proof. apply eq_sem, (M_correct PA_M ax_mul_rec ltac:(firstorder) (empty_PA_env _)). Qed.

Convert from nat to this model

  Fixpoint to_domain n : M_domain PA_M := match n with
    | 0 izero
    | S n iσ (to_domain n)
  end.

  Lemma to_domain_add x y :
    to_domain (x + y) = to_domain x i to_domain y.
  Proof.
    revert y. induction x; intros; cbn.
    - symmetry. apply add_zero.
    - rewrite add_rec. now repeat f_equal.
  Qed.


  Lemma to_domain_mul x y :
    to_domain (x * y) = to_domain x i to_domain y.
  Proof.
    revert y. induction x; intros; cbn.
    - symmetry. apply mul_zero.
    - rewrite mul_rec. rewrite to_domain_add. now repeat f_equal.
  Qed.


  Lemma to_domain_injective x x' :
    to_domain x = to_domain x' x = x'.
  Proof.
    revert x'. induction x; destruct x'.
    - reflexivity.
    - now intros H%zero_succ.
    - intros H. symmetry in H. now apply zero_succ in H.
    - intros H%succ_inj. now rewrite (IHx x').
  Qed.


End Model.

Standard Model


Section StandardModel.

  Definition std_interp_f (f : syms) : vec (ar_syms f) :=
    match f with
      | Zero _ 0
      | Succ v S (Vector.hd v)
      | Plus v Vector.hd v + Vector.hd (Vector.tl v)
      | Mult v Vector.hd v * Vector.hd (Vector.tl v)
    end.

  Definition std_interp_P (P : preds) : vec (ar_preds P) Prop :=
    match P with
      | Eq v Vector.hd v = Vector.hd (Vector.tl v)
    end.

  Instance I_nat : interp := {| i_f := std_interp_f ; i_P := std_interp_P |}.

  Definition Standard_Model : Model := {|
    M_domain := ;
    M_interp := I_nat
  |}.

  (* Automatically turns into relational interpretation via coercion *)
  Definition Standard_Model_p : Model_p := {|
    M_p_domain := ;
    M_p_interp := I_nat
  |}.

  Lemma std_model_correct :
     phi, PA Standard_Model .
  Proof.
    intros H. repeat try destruct H as [|H]; hnf; cbn; try congruence.
    intros P H IH n. induction n; auto. easy.
  Qed.


  Lemma std_model_p_correct :
     phi, PA Standard_Model_p p .
  Proof.
    intros H . repeat destruct H as [|H]; cbn.
    - intros d. now exists [d;d].
    - intros ? ? [v [[ [ _]] ?]]. repeat depelim v. now exists [;h].
    - intros d [v [[[] [[v' [[]]] []]]]]. repeat depelim v. repeat depelim v'. lia.
    - intros ? ? [ [[[ [[]]] [[ [[] ]] ?]] ?]]. repeat depelim . repeat depelim . repeat depelim .
      cbn in *. exists [;]. cbn. split. easy. lia.
    - intros d. exists [d;d]. repeat split; cbn. exists [0;d]. repeat split; trivial. exact [].
    - intros . exists [S + ; S ( + )]. repeat split.
      + exists [S ;]. repeat split. now exists [].
      + exists [ + ]. repeat split. now exists [;].
    - intros d. exists [0;0]. repeat split. 2: exact []. exists [0;d]. repeat split. exact [].
    - intros . exists [S * ; + ( * )]. repeat split.
      + exists [S ;]. repeat split. now exists [].
      + exists [; * ]. repeat split. now exists [;].
    - intros P [ [[[_ [_ ]] _] ]] d. repeat depelim ; cbn in *.
      rewrite in . induction d as [|d [ [[ _] IH]]].
      + now exists [0].
      + repeat depelim . exists [S ]. repeat split. destruct ( ) as [ [[[ [[ _] ?]] ?] ?]]. now exists [].
        repeat depelim . repeat depelim . cbn in *. congruence.
    - now exfalso.
  Qed.


  Definition Standard_PA_Model : Model_of PA := {|
    M_model := Standard_Model ;
    M_correct := std_model_correct ;
  |}.

  Definition Standard_PA_Model_p : Model_p_of PA := {|
    M_p_model := Standard_Model_p ;
    M_p_correct := std_model_p_correct ;
  |}.

End StandardModel.

Signature Embedding

We can embed the PA signature into the formula and translate to an arbitrary signature.

Section EmbedSignature.

  Definition Σf := PA_funcs_signature.
  Definition Σp := PA_preds_signature.
  Context {Σf' : funcs_signature}.
  Context {Σp' : preds_signature}.
  Context {D : Type}.
  Context {I : @interp Σf Σp D}.
  Context {I' : @interp Σf' Σp' D}.

  (* We assume that the PA functions and predicates are inside the
     environment at

        xO = Position of zero
        xS = Position of succ
        xA = Position of add
        xA + 1 = Position of mul

     Replace function and predicate symbols with the corresponding
     variable and shift the existing variables. 
  *)


  Fixpoint embed_term xO xS xA (t : @term Σf) : @term Σf' := match t with
    | var_indi x var_indi x
    | func (sym Zero) v func (@var_func _ xO 0) (Vector.map (embed_term xO xS xA) v)
    | func (sym Succ) v func (@var_func _ xS 1) (Vector.map (embed_term xO xS xA) v)
    | func (sym Plus) v func (@var_func _ xA 2) (Vector.map (embed_term xO xS xA) v)
    | func (sym Mult) v func (@var_func _ (S xA) 2) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x 0) v if Compare_dec.le_lt_dec xO x then func (@var_func _ (S x) 0) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 0) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x 1) v if Compare_dec.le_lt_dec xS x then func (@var_func _ (S x) 1) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 1) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x 2) v if Compare_dec.le_lt_dec xA x then func (@var_func _ (S (S x)) 2) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 2) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x ar) v func (@var_func _ x ar) (Vector.map (embed_term xO xS xA) v)
  end.

  Fixpoint embed_form xO xS xA xEq (phi : @form Σf Σp _) : @form Σf' Σp' _ := match with
    | fal fal
    | atom (pred Eq) v atom (@var_pred _ xEq 2) (Vector.map (embed_term xO xS xA) v)
    | atom (@var_pred _ x 2) v if Compare_dec.le_lt_dec xEq x then atom (@var_pred _ (S x) 2) (Vector.map (embed_term xO xS xA) v) else atom (@var_pred _ x 2) (Vector.map (embed_term xO xS xA) v)
    | atom (@var_pred _ x ar) v atom (@var_pred _ x ar) (Vector.map (embed_term xO xS xA) v)
    | bin op bin op (embed_form xO xS xA xEq ) (embed_form xO xS xA xEq )
    | quant_indi op quant_indi op (embed_form xO xS xA xEq )
    | quant_func op 0 quant_func op 0 (embed_form (S xO) xS xA xEq )
    | quant_func op 1 quant_func op 1 (embed_form xO (S xS) xA xEq )
    | quant_func op 2 quant_func op 2 (embed_form xO xS (S xA) xEq )
    | quant_func op ar quant_func op ar (embed_form xO xS xA xEq )
    | quant_pred op 2 quant_pred op 2 (embed_form xO xS xA (S xEq) )
    | quant_pred op ar quant_pred op ar (embed_form xO xS xA xEq )
  end.

  Definition pred n := match n with 0 0 | S n n end.

  (* Predicate that states that rho' contains the PA signature inserted at
      positions xO, xS, xA and xEq, and matches up with rho. *)

  Definition env_contains_PA (rho rho' : env D) xO xS xA xEq :=
    ( n, get_indi n = get_indi n)
    ( n ar, get_func n ar = match ar with
        | 0 match Compare_dec.lt_eq_lt_dec n xO with inleft (left _) get_func n 0 | inleft (right _) @i_f _ _ D I Zero | inright _ get_func (pred n) 0 end
        | 1 match Compare_dec.lt_eq_lt_dec n xS with inleft (left _) get_func n 1 | inleft (right _) @i_f _ _ D I Succ | inright _ get_func (pred n) 1 end
        | 2 if Nat.eq_dec n xA then @i_f _ _ D I Plus else match Compare_dec.lt_eq_lt_dec n (S xA) with inleft (left _) get_func n 2 | inleft (right _) @i_f _ _ D I Mult | inright _ get_func (pred (pred n)) 2 end
        | ar get_func n ar
      end)
    ( n ar, get_pred n ar = match ar with
        | 2 match Compare_dec.lt_eq_lt_dec n xEq with inleft (left _) get_pred n 2 | inleft (right _) @i_P _ _ D I Eq | inright _ get_pred (pred n) 2 end
        | ar get_pred n ar
      end).

  Local Arguments Nat.eq_dec : simpl never.
  Local Arguments Compare_dec.lt_eq_lt_dec : simpl never.

  Ltac solve_env E :=
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia; cbn; try rewrite E;
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia;
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia; cbn; try rewrite E;
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia.

  Lemma env_contains_PA_scons_i rho rho' xO xS xA xEq d :
    env_contains_PA xO xS xA xEq env_contains_PA d .: get_indi , get_func , get_pred d .: get_indi , get_func , get_pred xO xS xA xEq.
  Proof.
    intros E. split. 2: apply E. intros []. reflexivity. apply E.
  Qed.


  Lemma env_contains_PA_scons_f {rho rho' xO xS xA xEq ar} (f : vec D ar D) :
    env_contains_PA xO xS xA xEq
    match ar with
      | 0 env_contains_PA get_indi , f .: get_func , get_pred get_indi , f .: get_func , get_pred (S xO) xS xA xEq
      | 1 env_contains_PA get_indi , f .: get_func , get_pred get_indi , f .: get_func , get_pred xO (S xS) xA xEq
      | 2 env_contains_PA get_indi , f .: get_func , get_pred get_indi , f .: get_func , get_pred xO xS (S xA) xEq
      | ar env_contains_PA get_indi , f .: get_func , get_pred get_indi , f .: get_func , get_pred xO xS xA xEq
    end.
  Proof.
    intros E. unfold scons, scons_env_func, scons_ar. destruct ar as [|[|[]]];
    split; try apply E; split; try apply E; destruct E as [_ [ _]];
    intros [|[|[]]] [|[|[]]]; solve_env ; reflexivity.
  Qed.


  Lemma env_contains_PA_scons_p {rho rho' xO xS xA xEq ar} (P : vec D ar Prop) :
    env_contains_PA xO xS xA xEq
    match ar with
      | 2 env_contains_PA get_indi , get_func , P .: get_pred get_indi , get_func , P .: get_pred xO xS xA (S xEq)
      | _ env_contains_PA get_indi , get_func , P .: get_pred get_indi , get_func , P .: get_pred xO xS xA xEq
    end.
  Proof.
    intros E. unfold scons, scons_env_func, scons_ar. destruct ar as [|[|[]]];
    split; try apply E; split; try apply E; destruct E as [_ [_ ]];
    intros [|[|[]]] [|[|[]]]; solve_env ; reflexivity.
  Qed.


  Lemma embed_term_correct rho rho' xO xS xA xEq t :
    env_contains_PA xO xS xA xEq @eval Σf Σp D I t = @eval Σf' Σp' D I' (embed_term xO xS xA t).
  Proof.
    intros E. induction t; cbn.
    - apply E.
    - destruct E as [_ [ _]]. apply map_ext_forall in IH. destruct ar as [|[|[]]];
      try destruct Compare_dec.le_lt_dec; cbn; rewrite ;
      try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
      try destruct Nat.eq_dec; try lia; now rewrite map_map, IH.
    - destruct E as [_ [ _]]. apply map_ext_forall in IH. destruct f; cbn in *;
      rewrite ; destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
      try destruct Nat.eq_dec; try lia; now rewrite map_map, IH.
  Qed.


  Lemma embed_form_correct rho rho' xO xS xA xEq phi :
    env_contains_PA xO xS xA xEq @sat Σf Σp D I @sat Σf' Σp' D I' (embed_form xO xS xA xEq ).
  Proof.
    revert xO xS xA xEq. induction ; intros xO xS xA xEq E; cbn.
    - reflexivity.
    - assert (map (@eval Σf Σp D I ) v = map ( t @eval Σf' Σp' D I' (embed_term xO xS xA t)) v) as Hv'.
      { clear p. induction v. reflexivity. cbn; f_equal.
        apply (embed_term_correct _ _ _ _ _ _ _ E). apply IHv. }
      destruct E as [_ [_ ]]. destruct p; cbn.
      + destruct ar as [|[|[]]];
        try destruct Compare_dec.le_lt_dec; cbn; rewrite ;
        try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
        now rewrite map_map, Hv'.
      + destruct P; cbn in *. rewrite .
        destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia.
        now rewrite map_map, Hv'.
    - specialize ( xO xS xA xEq E);
      specialize ( xO xS xA xEq E).
      destruct b; tauto.
    - destruct q.
      + split; intros H d; eapply IHphi. 2,4: apply (H d). all: now apply env_contains_PA_scons_i.
      + split; intros [d H]; exists d; eapply IHphi. 2,4: apply H. all: now apply env_contains_PA_scons_i.
    - destruct q; destruct n as [|[|[]]]; split.
      1-8: intros H f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA_scons_f f).
      all: intros [f H]; exists f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA_scons_f f).
    - destruct q; destruct n as [|[|[]]]; split.
      1-8: intros H P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA_scons_p P).
      all: intros [P H]; exists P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA_scons_p P).
  Qed.


End EmbedSignature.

Section EmbedSignatureFuncfree.

  Context {Σf' : funcs_signature}.
  Context {Σp' : preds_signature}.
  Context {D : Type}.
  Context {I : @interp_p Σf Σp D}.
  Context {I' : @interp Σf' Σp' D}.

  Definition sshift k : term :=
     n match n with 0 $0 | S n $(1 + k + n) end.

  Fixpoint embed_term_funcfree (t : @term Σf) : @form Σf' Σp' _ := match t with
    | var_indi x p(1) atom (var_pred 0) ([var_indi 0]) --> atom (var_pred 0) ([var_indi (S x)])
    | func (sym Zero) v atom (var_pred 0) ([var_indi 0])
    | func (sym Succ) v let v' := Vector.map embed_term_funcfree v in
                              i (Vector.hd v')[sshift 1]i
                                 atom (var_pred 0) ([i$1 ; i$0])
    | func (sym Plus) v let v' := Vector.map embed_term_funcfree v in
                              i (Vector.hd v')[sshift 1]i
                                 i (Vector.hd (Vector.tl v'))[sshift 2]i
                                     atom (var_pred 0) ([i$2 ; i$1 ; i$0])
    | func (sym Mult) v let v' := Vector.map embed_term_funcfree v in
                              i (Vector.hd v')[sshift 1]i
                                 i (Vector.hd (Vector.tl v'))[sshift 2]i
                                     atom (var_pred 1) ([i$2 ; i$1 ; i$0])
    | func (var_func _) _ atom (var_pred 0) (Vector.nil _)
  end.

  Fixpoint embed_form_funcfree (phi : @form Σf Σp _) : @form Σf' Σp' _ := match with
    | fal fal
    | atom (SOL.pred Eq) v i embed_term_funcfree (Vector.hd v)
                               i (embed_term_funcfree (Vector.hd (Vector.tl v)))[sshift 1]i
                                   atom (var_pred 1) ([i$1 ; i$0])
    | atom (var_pred _) _ atom (var_pred 0) (Vector.nil _)
    | bin op bin op (embed_form_funcfree ) (embed_form_funcfree )
    | quant_indi op quant_indi op (embed_form_funcfree )
    | quant_func op ar quant_func op ar (embed_form_funcfree )
    | quant_pred op ar quant_pred op ar (embed_form_funcfree )
  end.

  Lemma embed_term_funcfree_funcfree t :
    funcfree (embed_term_funcfree t).
  Proof.
    induction t; try easy. destruct f; repeat depelim v; cbn in *; repeat split;
    apply funcfree_subst_i; try apply IH; now intros [].
  Qed.


  Lemma sat_sshift1' rho_i rho_f rho_p x y (phi : @form Σf' Σp' _) :
    funcfree ⟨⟨y .: x .: rho_i, rho_f, rho_p⟩⟩ p [sshift 1]i ⟨⟨y .: rho_i, rho_f, rho_p⟩⟩ p .
  Proof.
    intros F. setoid_rewrite sat_p_comp_i; trivial. erewrite sat_p_ext.
    split; eauto. intros n. split. 2: easy. now destruct n. intros []; eexists; reflexivity.
  Qed.


  Lemma sat_sshift2' rho_i rho_f rho_p x y z (phi : @form Σf' Σp' _) :
    funcfree ⟨⟨z .: y .: x .: rho_i, rho_f, rho_p⟩⟩ p [sshift 2]i ⟨⟨z .: rho_i, rho_f, rho_p⟩⟩ p .
  Proof.
    intros F. setoid_rewrite sat_p_comp_i; trivial. erewrite sat_p_ext.
    split; eauto. intros n. split. 2: easy. now destruct n. intros []; eexists; reflexivity.
  Qed.


  Lemma sat_sshift1 rho_i rho_f rho_p x y (phi : @form Σf' Σp' _) :
    funcfree y .: x .: rho_i, rho_f, rho_p [sshift 1]i y .: rho_i, rho_f, rho_p .
  Proof.
    intros F. setoid_rewrite sat_comp_i; trivial. erewrite sat_ext.
    split; eauto. intros n. split. 2: easy. now destruct n.
  Qed.


  Lemma sat_sshift2 rho_i rho_f rho_p z x y (phi : @form Σf' Σp' _) :
    funcfree z .: y .: x .: rho_i, rho_f, rho_p [sshift 2]i z .: rho_i, rho_f, rho_p .
  Proof.
    intros F. setoid_rewrite sat_comp_i; trivial. erewrite sat_ext.
    split; eauto. intros n. split. 2: easy. now destruct n.
  Qed.


  Definition P_zero := v proj1_sig (@i_f_p _ _ D I Zero) (Vector.tl v) (Vector.hd v).
  Definition P_succ := v proj1_sig (@i_f_p _ _ D I Succ) (Vector.tl v) (Vector.hd v).
  Definition P_plus := v proj1_sig (@i_f_p _ _ D I Plus) (Vector.tl v) (Vector.hd v).
  Definition P_mult := v proj1_sig (@i_f_p _ _ D I Mult) (Vector.tl v) (Vector.hd v).
  Definition P_eq := v @i_P_p _ _ D I Eq v.

  Lemma embed_term_funcfree_correct rho rho_f rho_p t :
    first_order_term t d, @eval_p Σf Σp D I t d sat Σf' Σp' D I' d .: get_indi_p , rho_f, P_zero .: P_succ .: P_plus .: P_mult .: P_eq .: rho_p (embed_term_funcfree t).
  Proof.
    intros F. induction t; intros d; cbn.
    - split. now intros . intros H. now apply (H ( v Vector.hd v = d)).
    - now exfalso.
    - destruct f; repeat depelim v; cbn in *.
      + split.
        * intros [v' [? ?]]. now repeat depelim v'.
        * intros H. now exists ([]).
      + split.
        * intros [v' [[? ?] ?]]. repeat depelim v'; cbn in *. exists . split.
          apply sat_sshift1. apply embed_term_funcfree_funcfree. now apply IH. easy.
        * intros [ H]. exists ([]). repeat split. apply IH; try easy.
          eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply H. easy.
      + split.
        * intros [v' [[? ?] ?]]. repeat depelim v'; cbn in *.
          exists . split. apply sat_sshift1. apply embed_term_funcfree_funcfree. now apply IH.
          exists . split. apply sat_sshift2. apply embed_term_funcfree_funcfree. now apply IH. easy.
        * intros [ [ [ [ ?]]]]. exists ([ ; ]). repeat split; try easy; apply IH; try easy.
          eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply .
          eapply sat_sshift2. apply embed_term_funcfree_funcfree. apply .
      + split.
        * intros [v' [[? ?] ?]]. repeat depelim v'; cbn in *.
          exists . split. apply sat_sshift1. apply embed_term_funcfree_funcfree. now apply IH.
          exists . split. apply sat_sshift2. apply embed_term_funcfree_funcfree. now apply IH. easy.
        * intros [ [ [ [ ?]]]]. exists ([ ; ]). repeat split; try easy; apply IH; try easy.
          eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply .
          eapply sat_sshift2. apply embed_term_funcfree_funcfree. apply .
  Qed.


  Lemma embed_form_funcfree_correct rho rho_f rho_p phi :
    first_order p get_indi_p , rho_f, P_zero .: P_succ .: P_plus .: P_mult .: P_eq .: rho_p embed_form_funcfree .
  Proof.
    induction in |-*; cbn; intros F.
    - reflexivity.
    - destruct p. now exfalso. destruct P. repeat depelim v; cbn in *. split.
      + intros [v' [[? [? ?]] ?]]. repeat depelim v'; cbn in *.
        exists . split. now apply embed_term_funcfree_correct.
        exists . split. apply sat_sshift1. apply embed_term_funcfree_funcfree.
        now apply embed_term_funcfree_correct. easy.
      + intros [ [ [ [ ?]]]]. exists ([ ; ]). repeat split; try easy.
        all: eapply embed_term_funcfree_correct; try easy. apply .
        eapply sat_sshift1. apply embed_term_funcfree_funcfree. apply .
    - destruct F as [ ]. specialize ( ); specialize ( ).
      destruct b; tauto.
    - destruct q; split; cbn.
      + intros H d. specialize (H d). apply IHphi in H. apply H. easy.
      + intros H d. apply IHphi. easy. apply H.
      + intros [d H]. exists d. apply IHphi in H. apply H. easy.
      + intros [d H]. exists d. apply IHphi. easy. apply H.
    - now exfalso.
    - now exfalso.
  Qed.


End EmbedSignatureFuncfree.

Now we can translate satisfiability and validity for arbitrary models over arbitrary signatures to PA models.

Section PAValidSatTranslation.

  Context `{Σf' : funcs_signature}.
  Context `{Σp' : preds_signature}.

  (* Encode axioms into formula *)
  Definition PA_form :=
    ax_eq_refl ax_eq_symm ax_zero_succ ax_succ_inj ax_add_zero ax_add_rec ax_mul_zero ax_mul_rec ax_ind.

  Lemma PA_Model_sat_PA_form (M_PA : Model_of PA) :
    M_PA PA_form.
  Proof.
    repeat split; apply (M_correct M_PA); repeat (try (left; reflexivity); try right).
  Qed.


  Lemma PA_model_valid_iff_model_valid (phi : @form PA_funcs_signature PA_preds_signature _) :
    ( M_PA : Model_of PA, M_PA ) ( M' : @Model Σf' Σp', M' (f(0) f(1) f(2) f(2) p(2) (embed_form 0 0 0 0 (PA_form --> )))).
  Proof.
    split.
    - intros H M' fO fS fM fA pE.
      pose (I := @B_I PA_funcs_signature PA_preds_signature _
                    ( f match f with Zero fO | Succ fS | Plus fA | Mult fM end)
                    ( P match P with Eq pE end )).
      pose (M := {| M_domain := M_domain M' ; M_interp := I |}).
      eapply (embed_form_correct ).
      + cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
      + intros H_PA. assert ( psi, PA M ) as M_correct.
        { intros . repeat try destruct as [|]; intros ; try easy; apply H_PA. }
        apply (H {| M_model := M ; M_correct := M_correct |}).
    - intros H M .
      pose (I' := {| i_f _ _ := @i_f _ _ _ (M_interp M) Zero ([]) ; i_P _ _ := True |} ).
      pose (M' := {| M_domain := M_domain M ; M_interp := I' |}).
      pose (zero' := @i_f _ _ _ (M_interp M) Zero); pose (succ := @i_f _ _ _ (M_interp M) Succ); pose (plus := @i_f _ _ _ (M_interp M) Plus); pose (mult := @i_f _ _ _ (M_interp M) Mult); pose (equal := @i_P _ _ _ (M_interp M) Eq).
      specialize (H M' zero' succ mult plus equal).
      eapply embed_form_correct in H. apply H. apply PA_Model_sat_PA_form. clear H. cbn.
      split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
  Qed.


  Lemma PA_model_sat_iff_model_sat (phi : @form PA_funcs_signature PA_preds_signature _) :
    ( (M_PA : Model_of PA) rho, (M_PA, ) ) ( (M' : @Model Σf' Σp') rho, (M', ) (f(0) f(1) f(2) f(2) p(2) (embed_form 0 0 0 0 (PA_form )))).
  Proof.
    split.
    - intros [M [ H]].
      pose (I' := @B_I Σf' Σp' _ ( f _ @i_f _ _ _ (M_interp M) Zero ([])) ( P _ True )).
      pose (M' := {| M_domain := M_domain M ; M_interp := I' |}).
      exists M', .
      exists (@i_f _ _ _ (M_interp M) Zero), (@i_f _ _ _ (M_interp M) Succ), (@i_f _ _ _ (M_interp M) Mult), (@i_f _ _ _ (M_interp M) Plus), (@i_P _ _ _ (M_interp M) Eq).
      eapply (embed_form_correct ).
      + cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
      + split. repeat try split; apply (M_correct M); clear; firstorder. apply H.
    - intros [M' [ [fO [fS [fM [fA [pE H]]]]]]]; cbn -[embed_form] in H.
      pose (I := @B_I PA_funcs_signature PA_preds_signature _
                    ( f match f with Zero fO | Succ fS | Plus fA | Mult fM end)
                    ( P match P with Eq pE end )).
      assert ( psi, PA {| M_domain := M_domain M' ; M_interp := I |} ) as M_correct.
      { intros . repeat try destruct as [|]; intros; try easy; apply H. }
      pose (M := {| M_model := {| M_domain := M_domain M' ; M_interp := I |} ; M_correct := M_correct |}).
      exists M, . eapply (embed_form_correct ) in H. apply H.
      split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
  Qed.


  Definition embed_PA phi := f(0) f(1) f(2) f(2) p(2) (@embed_form Σf' Σp' 0 0 0 0 (PA_form --> )).

  Lemma PA_sat_iff_empty_theory_sat (phi : @form PA_funcs_signature PA_preds_signature _) :
    PA ( _ False) embed_PA .
  Proof.
    split.
    - intros H M. now apply PA_model_valid_iff_model_valid.
    - intros H M. apply PA_model_valid_iff_model_valid. intros M'.
      apply (H {| M_model := M' ; M_correct := ( _ (f : False) match f with end) |}).
  Qed.


End PAValidSatTranslation.

Section PAValidSatTranslation_Funcfree.

  Context `{Σf' : funcs_signature}.
  Context `{Σp' : preds_signature}.

  (* Encode axioms into formula *)
  Definition PA_form_embedded :=
    @embed_form_funcfree Σf' Σp' (ax_eq_refl ax_eq_symm ax_zero_succ ax_succ_inj ax_add_zero ax_add_rec ax_mul_zero ax_mul_rec)
     p(1) (i p$1 ([$0]) p$0 ([$0])) --> (i p$0 ([$0]) --> (i p$0 ([$0 ; $1]) p$0 ([$0]))) --> i p$0 ([$0]).

  Definition total_functional0 x := (i p$x ([$0])) (i i p$x ([$1]) --> p$x ([$0]) --> p(1) p$0 ([$1]) --> p$0 ([$0])).
  Definition total_functional1 x := (i i p$x ([$0 ; $1])) (i i i p$x ([$1 ; $2]) --> p$x ([$0 ; $2]) --> p(1) p$0 ([$1]) --> p$0 ([$0])).
  Definition total_functional2 x := (i i i p$x ([$0 ; $1 ; $2])) (i i i i p$x ([$1 ; $2 ; $3]) --> p$x ([$0 ; $2 ; $3]) --> p(1) p$0 ([$1]) --> p$0 ([$0])).

  Definition all_total_functional := total_functional0 0 total_functional1 0 total_functional2 0 total_functional2 1.

  Lemma total_functional0_correct (M : Model) rho x :
    functional ( v d get_pred x 1 (Vector.cons _ d _ v)) total ( v d get_pred x 1 (Vector.cons _ d _ v)) (M, ) (total_functional0 x).
  Proof.
    intros [HF HT]. cbn. split.
    - intros. apply HT.
    - intros ? ?. now rewrite (HF ([]) ).
  Qed.


  Lemma total_functional1_correct (M : Model) rho x :
    functional ( v d get_pred x 2 (Vector.cons _ d _ v)) total ( v d get_pred x 2 (Vector.cons _ d _ v)) (M, ) (total_functional1 x).
  Proof.
    intros [HF HT]. cbn. split.
    - intros. apply HT.
    - intros a ? ?. now rewrite (HF ([a]) ).
  Qed.


  Lemma total_functional2_correct (M : Model) rho x :
    functional ( v d get_pred x 3 (Vector.cons _ d _ v)) total ( v d get_pred x 3 (Vector.cons _ d _ v)) (M, ) (total_functional2 x).
  Proof.
    intros [HF HT]. cbn. split.
    - intros. apply HT.
    - intros ? ?. now rewrite (HF ([ ; ]) ).
  Qed.


  Lemma PA_model_valid_iff_model_valid_funcfree (phi : @form PA_funcs_signature PA_preds_signature _) :
    first_order ( M_PA : Model_p_of PA, M_PA p ) ( M' : Model, M' (p(2) p(3) p(3) p(2) p(1) all_total_functional --> PA_form_embedded --> (embed_form_funcfree ))).
  Proof.
    intros FO. split.
    - intros H M' PE PM P_A PS PO H_PA. cbn [get_indi get_func get_pred] in *.
      assert (functional ( v d PO (Vector.cons d v)) total ( v d PO (Vector.cons d v))) as HPO.
      { destruct as [[[[HF HT] _] _] _]. split. intros v y y' . depelim v. now apply (HT y y' ( v y = Vector.hd v)). intros v. depelim v. apply HF. }
      assert (functional ( v d PS (Vector.cons d v)) total ( v d PS (Vector.cons d v))) as HPS.
      { destruct as [[[_ [HF HT]] _] _]. split. intros v y y' . repeat depelim v. now apply (HT h y y' ( v y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
      assert (functional ( v d P_A (Vector.cons d v)) total ( v d P_A (Vector.cons d v))) as HPA.
      { destruct as [[[_ _] [HF HT]] _]. split. intros v y y' . repeat depelim v. now apply (HT h y y' ( v y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
      assert (functional ( v d PM (Vector.cons d v)) total ( v d PM (Vector.cons d v))) as HPM.
      { destruct as [[[_ _] _] [HF HT]]. split. intros v y y' . repeat depelim v. now apply (HT h y y' ( v y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
      Existing Instance PA_funcs_signature.
      Existing Instance PA_preds_signature.
      pose (I := {| i_f_p f := match f with Zero exist _ ( v d PO (Vector.cons d v)) HPO | Succ exist _ ( v d PS (Vector.cons d v)) HPS | Plus exist _ ( v d P_A (Vector.cons d v)) HPA | Mult exist _ ( v d PM (Vector.cons d v)) HPM end ;
                    i_P_p P := match P with Eq PE end |}).
      pose (M := {| M_p_domain := M_domain M' ; M_p_interp := I |}).
      destruct as [rho_i rho_f rho_p]. cbn [get_indi get_func get_pred] in *.
      eapply sat_ext.
      2: apply (embed_form_funcfree_correct ⟨⟨rho_i, _ _ default_func_p _ (rho_i 0), rho_p⟩⟩); trivial.
      + intros n. split. reflexivity. intros ar. split. reflexivity.
        destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
        repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
        all: now repeat depelim v.
      + assert ( psi, PA M p ) as M_correct.
        { destruct H_PA as [H_PA1 H_PA2]. eapply sat_ext in H_PA1. eapply (embed_form_funcfree_correct ⟨⟨rho_i, _ _ default_func_p _ (rho_i 0), rho_p⟩⟩) in H_PA1.
          * intros . repeat destruct as [|]; try easy; try apply H_PA1.
            cbn. cbn in H_PA2. intros P [ [[[ [? ?]] ?] ?]] H_IH d.
            repeat depelim . repeat depelim . exists ([d]). repeat split.
            apply H_PA2. now exists h. intros d' ?. destruct (H_IH d') as [ [[[ [[ ?] ?]] ?] ?]].
            now exists ([d']). repeat depelim . repeat depelim . now exists .
          * easy.
          * intros n. split. reflexivity. intros ar. split. reflexivity.
            destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
            repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
            all: now repeat depelim v. }
        apply (H {| M_p_model := M ; M_p_correct := M_correct |}).
    - intros H M .
      Existing Instance Σf'. Existing Instance Σp'.
      pose (I' := {| i_f _ _ := get_indi_p 0 ; i_P _ _ := True |} ).
      pose (M' := {| M_domain := M_p_domain M ; M_interp := I' |}).
      pose (zero' := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Zero) (tl v) (hd v)); pose (succ := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Succ) (tl v) (hd v)); pose (plus := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Plus) (tl v) (hd v)); pose (mult := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Mult) (tl v) (hd v)); pose (equal := @i_P_p _ _ _ (M_p_interp M) Eq).
      pose ( := get_indi_p , _ _ _ get_indi_p 0, _ _ _ True).
      specialize (H M' equal mult plus succ zero'); change ((M', get_indi , get_func , zero' .: succ .: plus .: mult .: equal .: get_pred ) (all_total_functional --> PA_form_embedded --> embed_form_funcfree )) in H.
      eapply embed_form_funcfree_correct in H. apply H. easy.
      + change ((M', get_indi , get_func , zero' .: succ .: plus .: mult .: equal .: get_pred ) (all_total_functional)).
        split. split. split.
        * apply total_functional0_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Zero).
        * apply total_functional1_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Succ).
        * apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Plus).
        * apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Mult).
      + split.
        * eapply embed_form_funcfree_correct. easy. repeat split; apply (M_p_correct M); clear; firstorder.
        * cbn. intros P [ [? ?]] IH d. edestruct (M_p_correct M ax_ind ltac:(clear;firstorder) P) as [v ].
          -- exists []. cbn. repeat split; trivial. now exists [].
          -- cbn. intros [v' [[ ?] ?]]. repeat depelim v'. destruct (IH h) as [dS [? ?]]; trivial.
             exists [dS]. repeat split; trivial. now exists [h].
          -- cbn in . instantiate (1 := hd ([d])) in . repeat depelim v. cbn in .
             now destruct as [[ ?] ?].
  Qed.


  Lemma PA_model_sat_iff_model_sat_funcfree (phi : @form PA_funcs_signature PA_preds_signature _) :
    first_order ( (M_PA : Model_p_of PA) rho, (M_PA, ) p ) ( (M' : Model) rho, (M', ) (p(2) p(3) p(3) p(2) p(1) all_total_functional PA_form_embedded (embed_form_funcfree ))).
  Proof.
    intros FO. split.
    - intros [M [ H]].
      pose (I' := {| i_f _ _ := get_indi_p 0 ; i_P _ _ := True |} ).
      pose (M' := {| M_domain := M_p_domain M ; M_interp := I' |}).
      pose ( := get_indi_p , _ _ _ get_indi_p 0, _ _ _ True).
      exists M', .
      pose (zero' := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Zero) (tl v) (hd v)); pose (succ := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Succ) (tl v) (hd v)); pose (plus := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Plus) (tl v) (hd v)); pose (mult := v proj1_sig (@i_f_p _ _ _ (M_p_interp M) Mult) (tl v) (hd v)); pose (equal := @i_P_p _ _ _ (M_p_interp M) Eq).
      exists equal, mult, plus, succ, zero'; change ((M', get_indi , get_func , zero' .: succ .: plus .: mult .: equal .: get_pred ) ((all_total_functional PA_form_embedded) embed_form_funcfree )).
      split. split.
      + split. split. split.
        * apply total_functional0_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Zero).
        * apply total_functional1_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Succ).
        * apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Plus).
        * apply total_functional2_correct; now destruct (@i_f_p _ _ _ (M_p_interp M) Mult).
      + split.
        * eapply embed_form_funcfree_correct. easy. repeat split; apply (M_p_correct M); clear; firstorder.
        * cbn. intros P [ [? ?]] IH d. edestruct (M_p_correct M ax_ind ltac:(clear;firstorder) P) as [v ].
          -- exists []. cbn. repeat split; trivial. now exists [].
          -- cbn. intros [v' [[ ?] ?]]. repeat depelim v'. destruct (IH h) as [dS [? ?]]; trivial.
             exists [dS]. repeat split; trivial. now exists [h].
          -- cbn in . instantiate (1 := hd ([d])) in . repeat depelim v. cbn in .
             now destruct as [[ ?] ?].
      + now eapply embed_form_funcfree_correct.
    - intros [M' [ [PE [PM [P_A [PS [PO H]]]]]]]. cbn [get_indi get_func get_pred] in *.
      destruct H as [[HTF H_PA] H].
      assert (functional ( v d PO (Vector.cons d v)) total ( v d PO (Vector.cons d v))) as HPO.
      { destruct HTF as [[[[HF HT] _] _] _]. split. intros v y y' . depelim v. now apply (HT y y' ( v y = Vector.hd v)). intros v. depelim v. apply HF. }
      assert (functional ( v d PS (Vector.cons d v)) total ( v d PS (Vector.cons d v))) as HPS.
      { destruct HTF as [[[_ [HF HT]] _] _]. split. intros v y y' . repeat depelim v. now apply (HT h y y' ( v y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
      assert (functional ( v d P_A (Vector.cons d v)) total ( v d P_A (Vector.cons d v))) as HPA.
      { destruct HTF as [[[_ _] [HF HT]] _]. split. intros v y y' . repeat depelim v. now apply (HT h y y' ( v y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
      assert (functional ( v d PM (Vector.cons d v)) total ( v d PM (Vector.cons d v))) as HPM.
      { destruct HTF as [[[_ _] _] [HF HT]]. split. intros v y y' . repeat depelim v. now apply (HT h y y' ( v y = Vector.hd v)). intros v. repeat depelim v. apply HF. }
      Existing Instance PA_funcs_signature.
      Existing Instance PA_preds_signature.
      pose (I := {| i_f_p f := match f with Zero exist _ ( v d PO (Vector.cons d v)) HPO | Succ exist _ ( v d PS (Vector.cons d v)) HPS | Plus exist _ ( v d P_A (Vector.cons d v)) HPA | Mult exist _ ( v d PM (Vector.cons d v)) HPM end ;
                    i_P_p P := match P with Eq PE end |}).
      pose (M := {| M_p_domain := M_domain M' ; M_p_interp := I |}).
      destruct as [rho_i rho_f rho_p]. cbn [get_indi get_func get_pred] in *.
      assert ( psi, PA M p ) as M_correct.
      { destruct H_PA as [H_PA1 H_PA2]. eapply sat_ext in H_PA1. eapply (embed_form_funcfree_correct ⟨⟨rho_i, _ _ default_func_p _ (rho_i 0), rho_p⟩⟩) in H_PA1.
        * intros . repeat destruct as [|]; try easy; try apply H_PA1.
          cbn. cbn in H_PA2. intros P [ [[[ [? ?]] ?] ?]] H_IH d.
          repeat depelim . repeat depelim . exists ([d]). repeat split.
          apply H_PA2. now exists h. intros d' ?. destruct (H_IH d') as [ [[[ [[ ?] ?]] ?] ?]].
          now exists ([d']). repeat depelim . repeat depelim . now exists .
        * easy.
        * intros n. split. reflexivity. intros ar. split. reflexivity.
          destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
          repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
          all: now repeat depelim v. }
      exists {| M_p_model := M ; M_p_correct := M_correct |}.
      eapply sat_ext in H.
      eapply (embed_form_funcfree_correct ⟨⟨rho_i, _ _ default_func_p _ (rho_i 0), rho_p⟩⟩) in H; trivial.
      + eexists. apply H.
      + intros n. split. reflexivity. intros ar. split. reflexivity.
        destruct n as [|[|[]]]; destruct ar as [|[|[]]]; cbn -[PeanoNat.Nat.eq_dec];
        repeat (try rewrite nat_eq_dec_same; try destruct Nat.eq_dec as [e|]; try lia; try destruct e); try reflexivity.
        all: now repeat depelim v.
  Qed.


  Definition embed_PA_funcfree phi := (p(2) p(3) p(3) p(2) p(1) all_total_functional --> PA_form_embedded --> (embed_form_funcfree )).

  Lemma PA_sat_iff_empty_theory_sat_funcfree (phi : @form PA_funcs_signature PA_preds_signature _) :
    first_order PA p ( _ False) embed_PA_funcfree .
  Proof.
    intros FO. split.
    - intros H M. now apply PA_model_valid_iff_model_valid_funcfree.
    - intros H M. apply PA_model_valid_iff_model_valid_funcfree. easy. intros M'.
      apply (H {| M_model := M' ; M_correct := ( _ (f : False) match f with end) |}).
  Qed.


End PAValidSatTranslation_Funcfree.

Categoricity


Section Categoricity.

  Variable : Model_of PA.
  Variable : Model_of PA.

Abbreviations
  Notation D1 := (M_domain (M_model )).
  Notation D2 := (M_domain (M_model )).
  Notation I1 := (M_interp (M_model )).
  Notation I2 := (M_interp (M_model )).
  Notation eq1_sem := (eq_sem ).
  Notation eq2_sem := (eq_sem ).

  Notation "'O1'" := (@i_f _ _ D1 I1 Zero ([])).
  Notation "'O2'" := (@i_f _ _ D2 I2 Zero ([])).
  Notation "'S1' x" := (@i_f _ _ D1 I1 Succ ([x])) (at level 37).
  Notation "'S2' x" := (@i_f _ _ D2 I2 Succ ([x])) (at level 37).
  Notation "x 'i⊕1' y" := (@i_f _ _ D1 I1 Plus ([x ; y])) (at level 39).
  Notation "x 'i⊕2' y" := (@i_f _ _ D2 I2 Plus ([x ; y])) (at level 39).
  Notation "x 'i⊗1' y" := (@i_f _ _ D1 I1 Mult ([x ; y])) (at level 38).
  Notation "x 'i⊗2' y" := (@i_f _ _ D2 I2 Mult ([x ; y])) (at level 38).
  Notation "x '=1=' y" := (@i_P _ _ D1 I1 Eq ([x ; y])) (at level 40).
  Notation "x '=2=' y" := (@i_P _ _ D2 I2 Eq ([x ; y])) (at level 40).

Definition of isomorphism
  Inductive F : D1 D2 Prop :=
    | F_O : F
    | F_S : x y, F x y F ( x) ( y).

  Lemma F_inv1 x :
    F ( x) False.
  Proof.
    intros H. inversion H.
    + now apply (zero_succ x).
    + now apply (zero_succ y).
  Qed.


  Lemma F_inv2 y :
    F ( y) False.
  Proof.
    intros H. inversion H.
    + now apply (zero_succ y).
    + now apply (zero_succ x).
  Qed.


  Lemma F_inv3 y :
    F y y = .
  Proof.
    destruct (case_analysis y) as [|[y' ]].
    - easy.
    - now intros H%F_inv2.
  Qed.


  Lemma F_inv4 x :
    F x x = .
  Proof.
    destruct (case_analysis x) as [|[x' ]].
    - easy.
    - now intros H%F_inv1.
  Qed.


  Lemma F_inv5 :
     x y, F ( x) y y', y = y'.
  Proof.
    intros x y. destruct (case_analysis y) as [|[y' ]].
    - now intros H%F_inv1.
    - intros _. now exists y'.
  Qed.


  Lemma F_inv6 :
     x y, F x ( y) x', x = x'.
  Proof.
    intros x y. destruct (case_analysis x) as [|[x' ]].
    - now intros H%F_inv2.
    - intros _. now exists x'.
  Qed.


  Lemma F_inv7 x y :
    F ( x) ( y) F x y.
  Proof.
    intros H. inversion H.
    + exfalso. now apply (zero_succ x).
    + apply (succ_inj ) in as .
      apply (succ_inj ) in as .
      exact .
  Qed.


  Lemma F_total :
     x, y, F x y.
  Proof.
    apply (induction ).
    - exists . exact F_O.
    - intros x [y IH]. exists ( y). now apply F_S.
  Qed.


  Lemma F_surjective :
     y, x, F x y.
  Proof.
    apply (induction ).
    - exists . exact F_O.
    - intros y [x IH]. exists ( x). now apply F_S.
  Qed.


  Lemma F_functional :
     x y y', F x y F x y' y = y'.
  Proof.
    apply (induction ( x y y', F x y F x y' y = y')).
    - intros y y' . now rewrite (F_inv3 y), (F_inv3 y').
    - intros x IH y y' .
      destruct (F_inv5 x y ) as [z ], (F_inv5 x y' ) as [z' ].
      apply F_inv7 in ; apply F_inv7 in . now rewrite (IH z z').
  Qed.


  Lemma F_injective :
     x x' y, F x y F x' y x = x'.
  Proof.
    intros x x' y. revert y x x'.
    apply (induction ( y x x', F x y F x' y x = x')).
    - intros x x'' . now rewrite (F_inv4 x), (F_inv4 x'').
    - intros y IH x x' .
      destruct (F_inv6 x y ) as [z ], (F_inv6 x' y ) as [z' ].
      apply F_inv7 in ; apply F_inv7 in . now rewrite (IH z z').
  Qed.


  Lemma F_add :
     x x' y y', F x y F x' y' F (x i⊕1 x') (y i⊕2 y').
  Proof.
    apply (induction ( x x' y y', F x y F x' y' F (x i⊕1 x') (y i⊕2 y'))).
    - intros x' y y' . rewrite (F_inv3 y ).
      now rewrite (add_zero ), (add_zero ).
    - intros x'' IH x' y y' . destruct (F_inv5 x'' y ) as [y'' ].
      rewrite (add_rec ), (add_rec ).
      apply F_S, IH. now apply F_inv7. exact .
  Qed.


  Lemma F_mul :
     x x' y y', F x y F x' y' F (x i⊗1 x') (y i⊗2 y').
  Proof.
    apply (induction ( x x' y y', F x y F x' y' F (x i⊗1 x') (y i⊗2 y'))).
    - intros x' y y' . rewrite (F_inv3 y ).
      rewrite (mul_zero ), (mul_zero ).
      exact F_O.
    - intros x'' IH x' y y' . destruct (F_inv5 x'' y ) as [y'' ].
      rewrite (mul_rec ), (mul_rec ).
      apply F_add. exact . apply IH. now apply F_inv7. exact .
  Qed.


  Lemma F_eq :
     x x' y y', F x y F x' y' (x =1= x' y =2= y').
  Proof.
    apply (induction ( x x' y y', F x y F x' y' (x =1= x' y =2= y'))).
    - intros x' y y' . split.
      + intros %eq1_sem. rewrite in . rewrite (F_inv3 y ).
        rewrite (F_inv3 y' ). now apply eq2_sem.
      + intros %eq2_sem. rewrite in . rewrite (F_inv3 y ) in .
      rewrite (F_inv4 x' ). now apply eq1_sem.
    - intros x IH x' y y' . split.
      + intros %eq1_sem. rewrite in .
        destruct (F_inv5 x y ) as [z ]. destruct (F_inv5 x y' ) as [z' ].
        enough (z =2= z') as %eq2_sem by now apply eq2_sem.
        apply (IH x). now apply F_inv7. now apply F_inv7. now apply eq1_sem.
      + intros %eq2_sem. rewrite in .
        destruct (F_inv5 x y ) as [z ]. destruct (F_inv6 x' z ) as [x'' ].
        enough (x =1= x'') as %eq1_sem by now apply eq1_sem.
        apply (IH x'' z z). now apply F_inv7. now apply F_inv7. now apply eq2_sem.
  Qed.


F describes an isomorphism between D1 and D2.

  Class Iso T1 T2 := { iso : Prop }.
  Notation "rho ≈ sigma" := (iso ) (at level 30).

  Instance Iso_indi : Iso D1 D2 := {|
    iso := F
  |}.
  Instance Iso_vec ar : Iso (vec D1 ar) (vec D2 ar) := {|
    iso v1 v2 := @VectorLib.Forall2 _ _ F ar
  |}.
  Instance Iso_func {ar} : Iso (vec D1 ar D1) (vec D2 ar D2) := {|
    iso f1 f2 := v1 v2, F ( ) ( )
  |}.
  Instance Iso_pred {ar} : Iso (vec D1 ar Prop) (vec D2 ar Prop) := {|
    iso P1 P2 := v1 v2, ( )
  |}.
  Instance Iso_func_p {ar} : Iso (func_p D1 ar) (func_p D2 ar) := {|
    iso f1 f2 := v1 v2, x y, (proj1_sig x : Prop) (proj1_sig y : Prop) F x y
  |}.

  Instance Iso_env : Iso (env D1) (env D2) := {|
    iso rho1 rho2 := n,
         get_indi n get_indi n
        ar, get_func n ar get_func n ar
                   get_pred n ar get_pred n ar
  |}.
  Instance Iso_env_p : Iso (env_p D1) (env_p D2) := {|
    iso rho1 rho2 := n,
         get_indi_p n get_indi_p n
        ar, get_func_p n ar get_func_p n ar
                   get_pred_p n ar get_pred_p n ar
  |}.

  Lemma iso_env_i rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p x y :
    rho1_i, rho1_f, rho1_p rho2_i, rho2_f, rho2_p x y x .: rho1_i, rho1_f, rho1_p y .: rho2_i, rho2_f, rho2_p.
  Proof.
    intros . split. destruct n; firstorder. apply .
  Qed.


  Lemma iso_env_f rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p ar (f1 : vec D1 ar D1) f2 :
    rho1_i, rho1_f, rho1_p rho2_i, rho2_f, rho2_p rho1_i, .: rho1_f, rho1_p rho2_i, .: rho2_f, rho2_p.
  Proof.
    intros . split. apply . intros ar'. split. 2: apply .
    destruct n; cbn; destruct (PeanoNat.Nat.eq_dec ar ar') as [|].
    apply . all: apply .
  Qed.


  Lemma iso_env_p rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p ar (P1 : vec D1 ar Prop) P2 :
    rho1_i, rho1_f, rho1_p rho2_i, rho2_f, rho2_p rho1_i, rho1_f, .: rho1_p rho2_i, rho2_f, .: rho2_p.
  Proof.
    intros . split. apply . intros ar'. split. apply .
    destruct n; cbn; destruct (PeanoNat.Nat.eq_dec ar ar') as [|].
    apply . all: apply .
  Qed.


  Lemma iso_env_p_i rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p x y :
    ⟨⟨rho1_i, rho1_f, rho1_p⟩⟩ ⟨⟨rho2_i, rho2_f, rho2_p⟩⟩ x y ⟨⟨x .: rho1_i, rho1_f, rho1_p⟩⟩ ⟨⟨y .: rho2_i, rho2_f, rho2_p⟩⟩.
  Proof.
    intros . split. destruct n; firstorder. apply .
  Qed.


  Lemma iso_env_p_f rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p ar (f1 : func_p D1 ar) f2 :
    ⟨⟨rho1_i, rho1_f, rho1_p⟩⟩ ⟨⟨rho2_i, rho2_f, rho2_p⟩⟩ ⟨⟨rho1_i, .: rho1_f, rho1_p⟩⟩ ⟨⟨rho2_i, .: rho2_f, rho2_p⟩⟩.
  Proof.
    intros . split. apply . intros ar'. split. 2: apply .
    destruct n; cbn; destruct (PeanoNat.Nat.eq_dec ar ar') as [|].
    apply . all: apply .
  Qed.


  Lemma iso_env_p_p rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p ar (P1 : vec D1 ar Prop) P2 :
    ⟨⟨rho1_i, rho1_f, rho1_p⟩⟩ ⟨⟨rho2_i, rho2_f, rho2_p⟩⟩ ⟨⟨rho1_i, rho1_f, .: rho1_p⟩⟩ ⟨⟨rho2_i, rho2_f, .: rho2_p⟩⟩.
  Proof.
    intros . split. apply . intros ar'. split. apply .
    destruct n; cbn; destruct (PeanoNat.Nat.eq_dec ar ar') as [|].
    apply . all: apply .
  Qed.


  Lemma iso_vec_eq1 ar (v1 v1' : vec D1 ar) v2 :
     = .
  Proof.
    intros . induction ; dependent elimination .
    reflexivity. f_equal. eapply F_injective. apply . apply .
    eapply . apply . apply .
  Qed.


  Lemma iso_vec_eq2 ar (v1 : vec D1 ar) v2 v2' :
     = .
  Proof.
    intros . induction ; dependent elimination ; dependent elimination .
    reflexivity. f_equal. eapply F_functional. apply . apply .
    eapply . apply . apply .
  Qed.


Alternative characterization of f1 ≈ f2
  Lemma iso_func_p_char ar (f1 : func_p D1 ar) f2 :
     x y, F x y v1 v2, (proj1_sig x proj1_sig y).
  Proof.
    destruct as [ [f1_functional f1_total]];
    destruct as [ [f2_functional f2_total]]; cbn.
    split.
    - intros H x y . split.
      + intros . destruct (f2_total ) as [y' ].
        enough (y = y') by congruence. eapply F_functional.
        apply . eapply H. apply . easy. easy.
      + intros . destruct (f1_total ) as [x' ].
        enough (x = x') by congruence. eapply F_injective.
        apply . eapply H. apply . easy. easy.
    - intros H x y . destruct (F_total x) as [y' ].
      enough (y = y') by congruence. eapply f2_functional.
      apply . eapply H. apply . apply . exact .
  Qed.


We can translate predicates along this isomorphism

  Lemma P1_to_P2 ar (P1 : vec D1 ar Prop) :
    { P2 | }.
  Proof.
    exists ( v v', VectorLib.Forall2 F v' v v').
    intros . split.
    - intros v' . induction v'; dependent elimination .
      + exact .
      + assert (h = ) as . { apply eq1_sem. eapply F_eq. apply . apply . now apply eq2_sem. }
        assert (v' = ) as . { eapply IHv'. apply . reflexivity. apply . }
        exact .
    - firstorder.
  Qed.


  Lemma P2_to_P1 ar (P2 : vec D2 ar Prop) :
    { P1 | }.
  Proof.
    exists ( v v', VectorLib.Forall2 F v v' v').
    intros . split.
    - firstorder.
    - intros v' . induction v'; dependent elimination .
      + exact .
      + dependent elimination .
        assert (h = ) as . { apply eq2_sem. eapply F_eq. apply . apply . now apply eq1_sem. }
        assert (v' = ) as . { eapply IHv'. apply . reflexivity. apply . }
        exact .
  Qed.


Vectors and functions can not be computationally translated because of the elim restriction. But we can prove existential versions.

  Lemma v1_to_v2_ex ar (v1 : vec D1 ar) :
     v2, .
  Proof.
    induction .
    - now exists [].
    - destruct as [ IH]. destruct (F_total h) as [y H].
      now exists (y::).
  Qed.


  Lemma v2_to_v1_ex ar (v2 : vec D2 ar) :
     v1, .
  Proof.
    induction .
    - now exists [].
    - destruct as [ IH]. destruct (F_surjective h) as [x H].
      now exists (x::).
  Qed.


The isomorphism also respects evaluation of terms under isomorphic environments

  Lemma F_term rho1 rho2 t :
     F (eval D1 t) (eval D2 t).
  Proof.
    revert t. apply (term_ind ( t F (eval D1 t) (eval D2 t))); intros.
    - apply H.
    - apply H, Forall2_Forall. induction v. easy.
      split. now apply IH. apply IHv, IH.
    - destruct f; repeat depelim v; cbn in *.
      + exact F_O.
      + apply F_S. now apply IH.
      + apply F_add; now apply IH.
      + apply F_mul; now apply IH.
  Qed.


A similar result holds for satisfiablility of formulas, but as we are not able to computationally translate functions along the isomorphism, we must restrict to formulas without function quantificaion. To make our lives easier for the incompleteness proof, we restrict even further to only first-order formulas

  Definition iso_env_funcfree (rho1 : env D1) rho2 := n, get_indi n get_indi n ar, get_pred n ar get_pred n ar.
  Notation "rho ≈FF sigma" := (iso_env_funcfree ) (at level 30).

  Lemma iso_env_funcfree_i rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p x y :
    rho1_i, rho1_f, rho1_p FF rho2_i, rho2_f, rho2_p x y x .: rho1_i, rho1_f, rho1_p FF y .: rho2_i, rho2_f, rho2_p.
  Proof.
    intros n. split. destruct n; firstorder. apply .
  Qed.


  Lemma iso_env_funcfree_p rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p ar (P1 : vec D1 ar Prop) P2 :
    rho1_i, rho1_f, rho1_p FF rho2_i, rho2_f, rho2_p rho1_i, rho1_f, .: rho1_p FF rho2_i, rho2_f, .: rho2_p.
  Proof.
    intros n. split. apply . intros ar'. destruct n; cbn;
    destruct Nat.eq_dec as [|]. apply . all: apply .
  Qed.


  Lemma F_term_funcfree rho1 rho2 t :
     FF funcfreeTerm t F (eval D1 t) (eval D2 t).
  Proof.
    induction t; intros.
    - apply H.
    - easy.
    - destruct f; repeat depelim v; cbn in *.
      + exact F_O.
      + apply F_S. now apply IH.
      + apply F_add; now apply IH.
      + apply F_mul; now apply IH.
  Qed.


  Theorem sat_iff_funcfree rho1 rho2 phi :
     FF funcfree .
  Proof.
    revert . induction ; intros H F; cbn.
    - easy.
    - destruct p; cbn.
      + apply H. induction v; cbn. easy. split. apply F_term_funcfree. apply H.
        apply F. apply IHv, F.
      + destruct P; repeat depelim v; cbn in *. now apply F_eq; apply F_term_funcfree.
    - destruct F as [ ].
      specialize ( H ); specialize ( H ).
      destruct b; tauto.
    - destruct q; split.
      + intros y. destruct (F_surjective y).
        eapply IHphi. 2: easy. 2: apply . apply iso_env_funcfree_i; eauto.
      + intros x. destruct (F_total x).
        eapply IHphi. 2: easy. 2: apply . apply iso_env_funcfree_i; eauto.
      + intros [x ]. destruct (F_total x) as [y]. exists y.
        eapply IHphi. 2: easy. 2: apply . apply iso_env_funcfree_i; eauto.
      + intros [y ]. destruct (F_surjective y) as [x]. exists x.
        eapply IHphi. 2: easy. 2: apply . apply iso_env_funcfree_i; eauto.
    - easy.
    - destruct q; split.
      + intros . destruct (P2_to_P1 _ ) as [ ].
        eapply IHphi. 3: apply . apply iso_env_funcfree_p; eauto. easy.
      + intros . destruct (P1_to_P2 _ ) as [ ].
        eapply IHphi. 3: apply . apply iso_env_funcfree_p; eauto. easy.
      + intros [ ]. destruct (P1_to_P2 _ ) as [ ]. exists .
        eapply IHphi. 3: apply . apply iso_env_funcfree_p; eauto. easy.
      + intros [ ]. destruct (P2_to_P1 _ ) as [ ]. exists .
        eapply IHphi. 3: apply . apply iso_env_funcfree_p; eauto. easy.
  Qed.


First-order version with bounded enviroment isomorphism. We use this later to refute compactness.

  Lemma F_term_firstorder_bounded rho1 rho2 t :
    first_order_term t ( n, bounded_indi_term n t F (get_indi n) (get_indi n))
     F (eval D1 t) (eval D2 t).
  Proof.
    intros FO H. induction t; cbn.
    - apply H. cbn. lia.
    - easy.
    - destruct f; repeat depelim v; cbn in *.
      + exact F_O.
      + apply F_S. apply IH. easy. intros. now apply H.
      + apply F_add; apply IH; try easy; intros; now apply H.
      + apply F_mul; apply IH; try easy; intros; now apply H.
  Qed.


  Theorem sat_iff_firstorder_bounded rho1 rho2 phi :
    first_order ( n, bounded_indi n F (get_indi n) (get_indi n))
     .
  Proof.
    revert . induction ; intros F H; cbn.
    - easy.
    - destruct p; cbn. easy. destruct P; repeat depelim v; cbn in *.
      apply F_eq; apply F_term_firstorder_bounded; try easy; intros n ;
      apply H; intros ; now apply .
    - destruct F as [ ].
      assert ( n : , bounded_indi n F (get_indi n) (get_indi n)) as by (clear -H; firstorder).
      assert ( n : , bounded_indi n F (get_indi n) (get_indi n)) as by (clear -H; firstorder).
      specialize ( ); specialize ( ).
      destruct b; tauto.
    - destruct q; split.
      + intros y. destruct (F_surjective y). eapply IHphi. easy. 2: apply . intros [] ?; eauto.
      + intros x. destruct (F_total x). eapply IHphi. easy. 2: apply . intros [] ?; eauto.
      + intros [x ]. destruct (F_total x) as [y]. exists y. eapply IHphi. easy. 2: apply . intros [] ?; eauto.
      + intros [y ]. destruct (F_surjective y) as [x]. exists x. eapply IHphi. easy. 2: apply . intros [] ?; eauto.
    - easy.
    - easy.
  Qed.


Alternatively, we get the full result if we switch to semantics where functions are interpreted as total, functional predicates. Then the propositional isomorphism suffices.

  Lemma f1_to_f2_p ar (f1 : func_p D1 ar) :
     f2, .
  Proof.
    destruct as [ [f1_functional f1_total]].
    pose ( v y := v' x, VectorLib.Forall2 F v' v F x y v' x).
    assert (functional ) as f2_functional. {
      intros y y' .
      destruct (v2_to_v1_ex ar ) as [ H].
      destruct (F_surjective y) as [x ]; destruct (F_surjective y') as [x' ].
      eapply eq2_sem, (F_eq _ _ _ _ ), eq1_sem, f1_functional.
      apply ( x H ). apply ( x' H ).
    }
    assert (total ) as f2_total. {
      intros . destruct (v2_to_v1_ex ar ) as [ H].
      destruct (f1_total ) as [x ].
      destruct (F_total x) as [y ].
      exists y. intros x' .
      rewrite (iso_vec_eq1 _ H ).
      enough (x' = x) by congruence. now apply (F_injective x' x y).
    }
    exists (exist _ (conj f2_functional f2_total)).
    apply iso_func_p_char. cbn.
    intros x y . split; intros .
    - intros x' . rewrite (iso_vec_eq1 _ ).
      enough (x' = x) by congruence. now apply (F_injective x' x y).
    - now apply .
  Qed.


  Lemma f2_to_f1_p ar (f2 : func_p D2 ar) :
     f1, .
  Proof.
    destruct as [ [f2_functional f2_total]].
    pose ( v x := v' y, VectorLib.Forall2 F v v' F x y v' y).
    assert (functional ) as f1_functional. {
      intros x x' .
      destruct (v1_to_v2_ex ar ) as [ H].
      destruct (F_total x) as [y ]; destruct (F_total x') as [y' ].
      eapply eq1_sem, (F_eq _ _ _ _ ), eq2_sem, f2_functional.
      apply ( y H ). apply ( y' H ).
    }
    assert (total ) as f1_total. {
      intros . destruct (v1_to_v2_ex ar ) as [ H].
      destruct (f2_total ) as [y ].
      destruct (F_surjective y) as [x ].
      exists x. intros y' .
      rewrite (iso_vec_eq2 _ H ).
      enough (y' = y) by congruence. now apply (F_functional x y' y).
    }
    exists (exist _ (conj f1_functional f1_total)).
    apply iso_func_p_char. cbn.
    intros x y . split; intros .
    - now apply .
    - intros y' . rewrite (iso_vec_eq2 _ ).
      enough (y' = y) by congruence. now apply (F_functional x y' y).
  Qed.


  Lemma F_term_p rho1 rho2 t x y :
     eval_p D1 t x eval_p D2 t y F x y.
  Proof.
    revert t x y. apply (term_ind ( t x y, eval_p D1 t x eval_p D2 t y F x y)).
    - intros n x y H . apply H.
    - intros ar n v IH x y H [ [ ]] [ [ ]].
      eapply H. 2: apply . 2: apply . clear .
      induction ; dependent elimination v; dependent elimination ; cbn.
      easy. split; cbn in , , IH. now apply IH. now apply ( ).
    - intros f v IH x y H. destruct f; repeat depelim v;
      intros [ [ ]] [ [ ]]; repeat depelim ; repeat depelim .
      + exact F_O.
      + apply F_S. apply IH. easy. apply . apply .
      + destruct IH as [ [ _]]. apply F_add.
        apply . apply H. apply . apply .
        apply . apply H. apply . apply .
      + destruct IH as [ [ _]]. apply F_mul.
        apply . apply H. apply . apply .
        apply . apply H. apply . apply .
  Qed.


  Lemma eval_p_iff rho1 rho2 t x y :
     F x y (eval_p D1 t x eval_p D2 t y).
  Proof.
    revert t x y. apply (term_ind ( t x y, F x y (eval_p D1 t x eval_p D2 t y))).
    - intros n x y H . cbn. split.
      + intros . eapply eq2_sem, F_eq. apply H. apply . now apply eq1_sem.
      + intros . eapply eq1_sem, F_eq. apply H. apply . now apply eq2_sem.
    - intros ar n v IH x y H . split.
      + intros [ [ ]].
        destruct (v1_to_v2_ex _ ) as [ ]. exists . split.
        * clear . induction v; dependent elimination ; dependent elimination .
          easy. split. eapply IH. apply H. apply . apply .
          eapply IHv. apply IH. apply . apply .
        * eapply iso_func_p_char. apply H. apply . apply . exact .
      + intros [ [ ]].
        destruct (v2_to_v1_ex _ ) as [ ]. exists . split.
        * clear . induction v; dependent elimination ; dependent elimination .
          easy. split. eapply IH. apply H. apply . apply .
          eapply IHv. apply IH. apply . apply .
        * eapply iso_func_p_char. apply H. apply . apply . exact .
    - intros f v IH x y . destruct f; repeat depelim v; split;
      intros [v' [ ]]; repeat depelim v'.
      + rewrite (F_inv3 y ). exists []. split; easy.
      + rewrite (F_inv4 x ). exists []. split; easy.
      + destruct (F_inv5 _ y ) as [y' ]. exists [y']. repeat split.
        eapply IH. apply . eapply F_inv7. apply . apply .
      + destruct (F_inv6 x _ ) as [x' ]. exists [x']. repeat split.
        eapply IH. apply . eapply F_inv7. apply . apply .
      + destruct (F_total ) as [ ]. destruct (F_total ) as [ ].
        exists [ ; ]. repeat split.
        * eapply IH. apply . apply . apply .
        * eapply IH. apply . apply . apply .
        * symmetry. eapply F_functional. apply . now apply F_add.
      + destruct (F_surjective ) as [ ]. destruct (F_surjective ) as [ ].
        exists [ ; ]. repeat split.
        * eapply IH. apply . apply . apply .
        * eapply IH. apply . apply . apply .
        * symmetry. eapply F_injective. apply . now apply F_add.
      + destruct (F_total ) as [ ]. destruct (F_total ) as [ ].
        exists [ ; ]. repeat split.
        * eapply IH. apply . apply . apply .
        * eapply IH. apply . apply . apply .
        * symmetry. eapply F_functional. apply . now apply F_mul.
      + destruct (F_surjective ) as [ ]. destruct (F_surjective ) as [ ].
        exists [ ; ]. repeat split.
        * eapply IH. apply . apply . apply .
        * eapply IH. apply . apply . apply .
        * symmetry. eapply F_injective. apply . now apply F_mul.
  Qed.


  Theorem sat_p_iff rho1 rho2 phi :
     p p .
  Proof.
    revert . induction ; intros; cbn.
    - easy.
    - destruct p; split.
      + intros [ [ ]]. destruct (v1_to_v2_ex _ ) as [ ].
        exists . split.
        * clear . induction v; dependent elimination ; dependent elimination .
          easy. split.
          -- eapply eval_p_iff. apply H. apply . apply .
          -- eapply IHv. 2: apply . apply .
        * eapply H. apply . exact .
      + intros [ [ ]]. destruct (v2_to_v1_ex _ ) as [ ].
        exists . split.
        * clear . induction v; dependent elimination ; dependent elimination .
          easy. split.
          -- eapply eval_p_iff. apply H. apply . apply .
          -- eapply IHv. 2: apply . apply .
        * eapply H. apply . exact .
      + destruct P. intros [ [ ]]. destruct (v1_to_v2_ex _ ) as [ ].
        exists . repeat depelim v; repeat depelim ; repeat depelim . split.
        * repeat split.
          -- eapply eval_p_iff. apply H. apply . apply .
          -- eapply eval_p_iff. apply H. apply . apply .
        * eapply F_eq. apply . apply . apply .
      + destruct P. intros [ [ ]]. destruct (v2_to_v1_ex _ ) as [ ].
        exists . repeat depelim v; repeat depelim ; repeat depelim . split.
        * repeat split.
          -- eapply eval_p_iff. apply H. apply . apply .
          -- eapply eval_p_iff. apply H. apply . apply .
        * eapply F_eq. apply . apply . apply .
    - specialize ( H); specialize ( H).
      destruct b; tauto.
    - destruct q; split.
      + intros y. destruct (F_surjective y).
        eapply IHphi. 2: apply . apply iso_env_p_i; eauto.
      + intros x. destruct (F_total x).
        eapply IHphi. 2: apply . apply iso_env_p_i; eauto.
      + intros [x ]. destruct (F_total x) as [y]. exists y.
        eapply IHphi. 2: apply . apply iso_env_p_i; eauto.
      + intros [y ]. destruct (F_surjective y) as [x]. exists x.
        eapply IHphi. 2: apply . apply iso_env_p_i; eauto.
    - destruct q; split.
      + intros .
        destruct (f2_to_f1_p n (exist _ (conj ))) as [[f [ ]] ].
        eapply IHphi. 2: apply ( f ). apply iso_env_p_f; cbn; eauto.
      + intros .
        destruct (f1_to_f2_p n (exist _ (conj ))) as [[f [ ]] ].
        eapply IHphi. 2: apply ( f ). apply iso_env_p_f; cbn; eauto.
      + intros [ [ [ ]]].
        destruct (f1_to_f2_p n (exist _ (conj ))) as [[ [ ]]].
        exists , , . eapply IHphi. 2: apply . apply iso_env_p_f; auto.
      + intros [ [ [ ]]].
        destruct (f2_to_f1_p n (exist _ (conj ))) as [[ [ ]]].
        exists , , . eapply IHphi. 2: apply . apply iso_env_p_f; auto.
    - destruct q; split.
      + intros . destruct (P2_to_P1 n ).
        eapply IHphi. 2: apply . apply iso_env_p_p; eauto.
      + intros . destruct (P1_to_P2 n ).
        eapply IHphi. 2: apply . apply iso_env_p_p; eauto.
      + intros [ ]. destruct (P1_to_P2 n ) as [].
        exists . eapply IHphi. 2: apply . apply iso_env_p_p; eauto.
      + intros [ ]. destruct (P2_to_P1 n ) as [ ].
        exists . eapply IHphi. 2: apply . apply iso_env_p_p; eauto.
  Qed.


To get the same result for the normal Tarski Semantics with functions, we need to assume that F is computational.

  Section ComputationalF.

    Hypothesis F_total_comp : x, { y | F x y }.
    Hypothesis F_surjective_comp : y, { x | F x y }.

Now we can transport vectors and functions

    Lemma v1_to_v2 ar (v1 : vec D1 ar) :
      { v2 | F }.
    Proof.
      induction .
      - now exists [].
      - destruct as [ IH]. destruct (F_total_comp h) as [x H].
        now exists (x::).
    Qed.


    Lemma v2_to_v1 ar (v2 : vec D2 ar) :
      { v1 | F }.
    Proof.
      induction .
      - now exists [].
      - destruct as [ IH]. destruct (F_surjective_comp h) as [x H].
        now exists (x::).
    Qed.


    Lemma f1_to_f2 ar (f1 : vec D1 ar D1) :
      { f2 | }.
    Proof.
      exists ( v2 proj1_sig (F_total_comp ( (proj1_sig (v2_to_v1 _ ))))).
      intros .
      destruct (v2_to_v1 ar ) as [ ]; cbn.
      destruct (F_total_comp ( )) as [x ]; cbn.
      enough ( = ) by congruence.
      clear . induction ; dependent elimination ; dependent elimination .
      - reflexivity.
      - f_equal.
        + eapply eq1_sem, F_eq. apply . apply . now apply eq2_sem.
        + eapply . apply . apply .
    Qed.


    Lemma f2_to_f1 ar (f2 : vec D2 ar D2) :
      { f1 | }.
    Proof.
      exists ( v1 proj1_sig (F_surjective_comp ( (proj1_sig (v1_to_v2 _ ))))).
      intros .
      destruct (v1_to_v2 ar ) as [ ]; cbn.
      destruct (F_surjective_comp ( )) as [y ]; cbn.
      enough ( = ) by congruence.
      clear . induction ; dependent elimination ; dependent elimination .
      - reflexivity.
      - f_equal.
        + eapply eq2_sem, F_eq. apply . apply . now apply eq1_sem.
        + eapply . apply . apply .
    Qed.


    Theorem sat_iff rho1 rho2 phi :
       .
    Proof.
      revert . induction ; intros; cbn.
      - easy.
      - destruct p.
        + apply H. apply Forall2_Forall. induction v; cbn.
          easy. split. now apply F_term. exact IHv.
        + destruct P; repeat depelim v; cbn.
          apply F_eq; apply F_term; exact H.
      - specialize ( H); specialize ( H).
        destruct b; tauto.
      - destruct q; split.
        + intros y. destruct (F_surjective y).
          eapply IHphi. 2: apply . apply iso_env_i; eauto.
        + intros x. destruct (F_total x).
          eapply IHphi. 2: apply . apply iso_env_i; eauto.
        + intros [x ]. destruct (F_total x) as [y]. exists y.
          eapply IHphi. 2: apply . apply iso_env_i; eauto.
        + intros [y ]. destruct (F_surjective y) as [x]. exists x.
          eapply IHphi. 2: apply . apply iso_env_i; eauto.
      - destruct q; split.
        + intros . destruct (f2_to_f1 n ).
          eapply IHphi. 2: apply . apply iso_env_f; eauto.
        + intros . destruct (f1_to_f2 n ).
          eapply IHphi. 2: apply . apply iso_env_f; eauto.
        + intros [ ]. edestruct (f1_to_f2 n ) as [].
          exists . eapply IHphi. 2: apply . apply iso_env_f; eauto.
        + intros [ ]. edestruct (f2_to_f1 n ) as [].
          exists . eapply IHphi. 2: apply . apply iso_env_f; eauto.
      - destruct q; split.
        + intros . destruct (P2_to_P1 n ).
          eapply IHphi. 2: apply . apply iso_env_p; eauto.
        + intros . edestruct (P1_to_P2 n ).
          eapply IHphi. 2: apply . apply iso_env_p; eauto.
        + intros [ ]. edestruct (P1_to_P2 n ) as [].
          exists . eapply IHphi. 2: apply . apply iso_env_p; eauto.
        + intros [ ]. edestruct (P2_to_P1 n ) as [ ].
          exists . eapply IHphi. 2: apply . apply iso_env_p; eauto.
    Qed.


  End ComputationalF.

If one side has a computational induction principle, we can translate from this side.

  Section ComputationalD1.

    Hypothesis : P : D1 Type, P ( x, P x P ( x)) x, P x.

    Lemma F_total_comp x :
      { y | F x y }.
    Proof.
      revert x. apply .
      - exists . exact F_O.
      - intros x [y IH]. exists ( y). now apply F_S.
    Qed.


    Lemma env1_to_env2_FO rho1 :
      { rho2 | FF }.
    Proof.
      exists n proj1_sig (F_total_comp (get_indi n)),
               n ar v ,
               n ar v proj1_sig (P1_to_P2 _ (get_pred n ar)) v .
      intros n. split. destruct n; cbn; now destruct F_total_comp.
      intros ar H. cbn. destruct P1_to_P2 as [? ]. now apply .
    Qed.


  End ComputationalD1.

  Section ComputationalD2.

    Hypothesis : P : D2 Type, P ( x, P x P ( x)) x, P x.

    Lemma F_surjective_comp y :
      { x | F x y }.
    Proof.
      revert y. apply .
      - exists . exact F_O.
      - intros y [x IH]. exists ( x). now apply F_S.
    Qed.


    Lemma env2_to_env1_FO rho2 :
      { rho1 | FF }.
    Proof.
      exists n proj1_sig (F_surjective_comp (get_indi n)),
               n ar v ,
               n ar v proj1_sig (P2_to_P1 _ (get_pred n ar)) v .
      intros n. split. destruct n; cbn; now destruct F_surjective_comp.
      intros ar H. cbn. destruct P2_to_P1 as [? ]. now apply .
    Qed.


  End ComputationalD2.

End Categoricity.

Consequence of categoricity we will use for incompleteness: If a closed formula holds in one model, it holds in all models.

Theorem PA_models_agree phi (M : Model_of PA) (rho : env (M_domain M)) :
  funcfree bounded_indi 0 ( ar, bounded_pred ar 0 ) sat _ M' : Model_of PA, M' .
Proof.
  intros F Bi Bp H M' .
  eapply sat_ext_closed_funcfree with ( := empty_PA_env _); try assumption.
  eapply sat_ext_closed_funcfree with ( := empty_PA_env _) in H; try assumption.
  eapply sat_iff_funcfree. 3: apply H.
  intros n. split. apply F_O. cbn. reflexivity. assumption.
Qed.


Theorem PA_models_agree_FO phi (M : Model_of PA) (rho : env (M_domain M)) :
  first_order bounded_indi 0 sat _ M' : Model_of PA, M' .
Proof.
  intros F B H M' .
  eapply sat_ext_closed_FO with ( := empty_PA_env _); try assumption.
  eapply sat_ext_closed_FO with ( := empty_PA_env _) in H; try assumption.
  eapply sat_iff_funcfree. 3: apply H.
  intros n. split. apply F_O. cbn. reflexivity. now apply firstorder_funcfree.
Qed.


Another interesting way of putting it using LEM:

Section LEM.

  Variable LEM : P, P P.

  Lemma PA_models_agree_LEM phi :
    funcfree bounded_indi 0 ( ar, bounded_pred ar 0 ) ( M : Model_of PA, M ) ( M : Model_of PA, M ¬ ).
  Proof.
    intros FO .
    destruct (LEM (Standard_PA_Model )) as [H|H].
    - left. now apply PA_models_agree with (M := Standard_PA_Model) ( := empty_PA_env _).
    - right. apply PA_models_agree with (M := Standard_PA_Model) ( := empty_PA_env _); try easy.
      intros . apply H. now apply PA_models_agree with (M := Standard_PA_Model) ( := empty_PA_env _).
  Qed.


End LEM.

Failure of Upward Löwenheim-Skolem


Section LoewenheimSkolem.

  Definition countably_infinite (X : Type) := R : X Prop,
       ( x, n, R x n) (* Total *)
     ( n, x, R x n) (* Surjective *)
     ( x n n', R x n R x n' n = n') (* Functional *)
     ( x x' n, R x n R x' n x = x') (* Injective *) .

  Theorem Upwards_Loewenheim_Skolem_Failure :
     M : Model_of PA, countably_infinite (M_domain M).
  Proof.
    intros M. exists (F M Standard_PA_Model). repeat split.
    - apply (F_total M Standard_PA_Model).
    - apply (F_surjective M Standard_PA_Model).
    - apply (F_functional M Standard_PA_Model).
    - apply (F_injective M Standard_PA_Model).
  Qed.


End LoewenheimSkolem.

Failure of Compactness


Require Import ListLib.

Section Compactness.

  Fixpoint num n := match n with 0 zero | S n σ (num n) end.

  Fixpoint greater_than n := match n with
    | 0 var_indi 0 == zero --> fal
    | S n (var_indi 0 == num (S n) --> fal) greater_than n
  end.

  Definition T phi := PA n, = greater_than n.

  Lemma num_injective n1 n2 :
    num = num = .
  Proof.
    revert . induction ; intros [] H; try now inversion H.
    erewrite . reflexivity. now inversion H.
  Qed.


  Lemma greater_than_injective n1 n2 :
    greater_than = greater_than = .
  Proof.
    revert . induction ; intros [] H; try now inversion H.
    erewrite . reflexivity. now inversion H.
  Qed.


  Lemma num_dec t:
    { n | t = num n } + ({ n | t = num n } False).
  Proof with try (right; intros [[] H]; now inversion H).
    induction t using term_rect... destruct f... all: repeat depelim v; cbn in *.
    - left. now exists 0.
    - destruct IH as [[IH|IH] _].
      + left. destruct IH as [n ]. now exists (S n).
      + right. intros [[] H]; cbn in H. now inversion H. apply IH. exists n.
        now inversion H.
  Qed.


  Lemma greater_than_dec phi :
    { n | = greater_than n } + ({ n | = greater_than n } False).
  Proof with try (right; intros [[] H]; now inversion H).
    induction ... destruct b...
    - destruct ... destruct b... destruct phi1_1... destruct p... destruct P.
      destruct phi1_2... repeat depelim v. destruct h... destruct n...
      destruct (num_dec ) as [[[|] ]|]...
      + destruct as [[ ]|].
        * decide ( = ) as [|]. left. now exists (S ). right.
          intros [[] ]; try now inversion . cbn in . inversion .
          apply num_injective in as . now apply greater_than_injective in as .
        * right. intros [[] H]; try now inversion H. apply . exists n. now inversion H.
      + right. intros [[] H]; try now inversion H. apply . exists (S n). now inversion H.
    - destruct ... destruct p... destruct P. destruct ... repeat depelim v.
      destruct h... destruct n... destruct ... destruct f... destruct f... repeat depelim v.
      left. now exists 0.
  Qed.


  Lemma T_decidable :
    decidable T.
  Proof.
    apply decidable_if. intros . apply or_dec. apply in_dec, form_eq_dec.
    destruct (greater_than_dec ) as [[n ]|H]. left. now exists n.
    right. intros [n ]. apply H. now exists n.
  Qed.


  Lemma greater_than_first_order n :
    first_order (greater_than n).
  Proof.
    induction n; cbn. easy. repeat split. clear IHn. now induction n. easy.
  Qed.


  Lemma greater_than_bounded n :
    bounded_indi 1 (greater_than n).
  Proof.
    induction n; cbn. lia. repeat split. lia. clear IHn. now induction n. easy.
  Qed.


  Lemma num_standard_model rho n :
    eval (I := M_interp Standard_Model) (num n) = n.
  Proof.
    induction n; cbn; auto.
  Qed.


  Lemma greater_than_standard_model rho n :
    (Standard_Model, ) (greater_than n) get_indi 0 > n.
  Proof.
    induction n; cbn in *.
    - split; lia.
    - split; cbn.
      + intros [ %IHn]. rewrite num_standard_model in . lia.
      + intros H. split. rewrite num_standard_model. lia. apply IHn. lia.
  Qed.


  Lemma find_greatest_in_list A :
    ( phi, List.In A T ) k, n, List.In (greater_than n) A k > n.
  Proof.
    intros HA. induction A as [| A IHA]; cbn. now exists 0. destruct IHA as [k IHA].
    auto. destruct (HA ) as [|[n ]]; trivial.
    - exists k. intros n [|].
      + cbn in H. unfold ax_eq_refl, ax_eq_symm, ax_zero_succ, ax_succ_inj, ax_add_zero, ax_add_rec, ax_mul_zero, ax_mul_rec, ax_ind in H.
        repeat (try destruct H as [|H]); try easy; destruct n; cbn in *; try congruence.
      + now apply IHA.
    - exists (max k (S n)). intros m [|].
      + apply greater_than_injective in H as . lia.
      + specialize (IHA _ H). lia.
  Qed.


  Lemma model_for_finite_subset A :
    ( phi, List.In A T ) (M : Model) rho, phi, List.In A (M, ) .
  Proof.
    intros HA. destruct (find_greatest_in_list A HA) as [k Hk].
    exists Standard_PA_Model, _ k, _ _ _ 0, _ _ _ True .
    intros H. pose (H' := H). apply HA in H' as [|[n ]].
    - now apply std_model_correct.
    - apply greater_than_standard_model. cbn. now apply Hk.
  Qed.


  Lemma no_model_for_T :
     (M : Model) rho, phi, T (M, ) .
  Proof.
    intros [M [ H]].
    assert ( phi, PA M ) as M_PA_sat.
    { intros . specialize (H (or_introl )).
      repeat destruct as [|]; eauto. easy. }
    pose (M_PA := {| M_model := M ; M_correct := M_PA_sat |}).
    destruct (F_surjective Standard_PA_Model M_PA (get_indi 0)) as [n Hn].
    specialize (H (greater_than n)).
    change ((M, ) (greater_than n)) with ((M_PA, ) (greater_than n)) in H.
    eapply sat_iff_firstorder_bounded with ( := _ n, _ _ _ 0, _ _ _ True ) in H.
    - apply greater_than_standard_model in H. cbn in H. lia.
    - apply greater_than_first_order.
    - intros [] ; cbn. apply Hn. exfalso. apply . eapply bounded_indi_up.
      2: apply greater_than_bounded. lia.
    - right. now exists n.
  Qed.


  Theorem Compactness_Failure :
     (( (M : Model) rho, phi, T (M, ) ) ( A, ( phi, List.In A T ) (M : Model) rho, phi, List.In A (M, ) )).
  Proof.
    intros H. apply no_model_for_T, H, model_for_finite_subset.
  Qed.


End Compactness.

Infinitary Incompleteness


Section InfinitaryIncompleteness.

  Variable prv : list form form Prop.
  Definition tprv (T : form Prop) phi := A, ( psi, List.In A T ) prv A .
  Notation "T ⊢ phi" := (prv T ) (at level 20).
  Notation "T ⊩ phi" := (tprv T ) (at level 20).

  Definition valid' (T : form Prop) phi :=
     M rho, ( a, T a (M, ) a) (M, ) .

  Hypothesis sound : T phi, T validT T .
  Hypothesis complete : T phi, decidable T validT T T .

  Definition LEM := P, P P.

Compatibility between different valdity formulations
  Lemma model_to_valid (T : form Prop) phi :
    ( M rho, ( a, T a (M, ) a) (M, ) ) validT T .
  Proof.
    intros H D I . apply (H {| M_domain := D ; M_interp := I |} ).
  Qed.


We can avoid the use of LEM since we want to show a negation
  Lemma xm_neg P :
    (P P False) False.
  Proof.
    tauto.
  Qed.


  Theorem InfinitaryIncompleteness :
    False.
  Proof.
    eapply xm_neg. intros X.
    apply Compactness_Failure. split.
    - intros [M [ ]] A . exists M, . intros . apply , , .
    - intros . enough ( T ) as HT.
      { destruct X as [X|H]. apply X. exfalso. apply HT.
        apply complete, model_to_valid. apply T_decidable. intros M . apply H. now exists M, . }
      intros [A [ ]]. assert (( phi List.In A) ) as %sound by now exists A.
      destruct ( A) as [M [ ]]; trivial. eapply . apply .
  Qed.


End InfinitaryIncompleteness.

Notation "'izero'" := (@i_f _ _ (M_domain _) (M_interp _) Zero ([])).
Notation "'iσ' x" := (@i_f _ _ (M_domain _) (M_interp _) Succ ([x])) (at level 37).
Notation "x 'i⊕' y" := (@i_f _ _ (M_domain _) (M_interp _) Plus ([x ; y])) (at level 39).
Notation "x 'i⊗' y" := (@i_f _ _ (M_domain _) (M_interp _) Mult ([x ; y])) (at level 38).
Notation "x 'i==' y" := (@i_P _ _ (M_domain _) (M_interp _) Eq ([x ; y])) (at level 40).

Notation "rho ≈ sigma" := (@iso _ _ _ ) (at level 30).
Notation "rho ≈FF sigma" := (@iso_env_funcfree _ _ ) (at level 30).