proposition: Lemma sound_for_classical_model {p:peirce} {ff : falsity_flag} A phi (D : Type) (I : interp D) (rho : env D) : classical I -> A ⊢ phi -> rho ⊫ A -> rho ⊨ phi.
proof: Proof. intros LEM HD. revert LEM rho. induction HD; cbn; intros LEM rho HA. - intros Hphi. apply IHHD. 1:easy. intros a [<-|Ha]; try easy. now apply HA. - now apply IHHD1, IHHD2. - intros d. apply IHHD; trivial. intros psi [psi'[<- H' % HA]] % in_map_iff. eapply sat_comp. now comp. - eapply sat_comp, sat_ext. 2: apply (IHHD LEM rho HA (eval rho t)). now intros []. - apply (IHHD) in HA; cbn in *; eauto. exfalso;easy. - apply HA, H. - intros H. unfold classical in LEM. cbn in LEM. eapply LEM. exact H. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Deduction.FragmentND Undecidability(Shared.ListAutomation) Vector Lia