proposition: Lemma PA2_valid_alternative phi : PA2 ⊨ phi <-> forall M, M ⊨ PA2 -> M ⊨ phi.
proof: Proof. split. - intros H1 M H2 rho. apply H1. intros psi H3. repeat destruct H3 as [<-|H3]; try apply H2; try easy; clear; firstorder. - intros H1 M rho H2. apply H1. intros psi H3. repeat destruct H3 as [<-|H3]; intros rho'. apply (H2 ax_eq_refl). 2: apply (H2 ax_eq_symm). 3: apply (H2 ax_zero_succ). 4: apply (H2 ax_succ_inj). 5: apply (H2 ax_add_zero). 6: apply (H2 ax_add_rec). 7: apply (H2 ax_mul_zero). 8: apply (H2 ax_mul_rec). 9: apply (H2 ax_ind). all: easy. 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