proposition: Lemma PA2_model_sat_iff_model_sat (phi : @form PA2_funcs_signature PA2_preds_signature _) : (exists M rho, (M, rho) ⊨ PA2 /\ (M, rho) ⊨ phi) <-> (exists M' rho, (M', rho) ⊨ (∃f(0) ∃f(1) ∃f(2) ∃f(2) ∃p(2) (embed_form 0 0 0 0 (PA2_form ∧ phi)))).
proof: Proof. split. - intros [M [rho H]]. pose (I' := @B_I Σf' Σp' _ (fun f _ => @i_f _ _ _ (M_interp M) Zero ([])) (fun P _ => True )). pose (M' := {| M_domain := M_domain M ; M_interp := I' |}). exists M', rho. 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 rho). + cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]]. + split. now apply -> PA2_Model_sat_PA2_form. apply H. - intros [M' [rho [fO [fS [fM [fA [pE H]]]]]]]; cbn -[embed_form] in H. pose (I := @B_I PA2_funcs_signature PA2_preds_signature _ (fun f => match f with Zero => fO | Succ => fS | Plus => fA | Mult => fM end) (fun P => match P with Eq => pE end )). pose (M := {| M_domain := M_domain M' ; M_interp := I |}). exists M, rho. eapply (embed_form_correct rho) in H. + split. apply PA2_Model_sat_PA2_form, H. apply H. + split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]]. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec