proposition: Lemma PA2_model_valid_iff_model_valid (phi : @form PA2_funcs_signature PA2_preds_signature _) : (forall M rho, (M, rho) ⊨ PA2 -> (M, rho) ⊨ phi) <-> (forall 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 H M' rho fO fS fM fA pE. 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 |}). eapply (embed_form_correct rho). + cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]]. + intros H_PA2. apply (H M), PA2_Model_sat_PA2_form, H_PA2. - intros H M rho M_correct. 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' rho zero' succ mult plus equal). eapply embed_form_correct in H. + apply H. apply -> PA2_Model_sat_PA2_form. apply M_correct. + 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