proposition: Theorem H10p_to_satisfiability Σf Σp e : H10p e <-> exists (M : @Model Σf Σp) rho, (M, rho) ⊨ (∃f(0) ∃f(1) ∃f(2) ∃f(2) ∃p(2) (embed_form 0 0 0 0 (PA2_form ∧ encode_problem e))).
proof: Proof. split. - intros H. apply PA2_model_sat_iff_model_sat. exists Standard_Model, (empty_PA2_env _). split. intros ? ?. now apply std_model_correct. now apply H10p_to_PA2_standard_model_sat. - intros [M [rho H]]. edestruct PA2_model_sat_iff_model_sat as [_ H1]. destruct H1 as [M' [rho' [H1 H2]]]. exists M, rho. apply H. eapply H10p_to_PA2_model_sat with (M := M') (rho := rho'). + intros phi H3 rho''. eapply sat_ext_closed. 4: apply H1, H3. all: apply PA2_closed, H3. + eapply sat_ext_closed_FO. apply encoding_first_order. apply encoding_closed. apply H2. Qed.
imports: PeanoNat Lia Vector List Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts PA2_categoricity) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.H10(H10p) Undecidability.Shared.Dec