proposition: Lemma ksoundness_bot_model {ff1 ff2 : falsity_flag} A (psi : @form _ _ _ ff1) (phi : @form _ _ _ ff2) D (M : kmodel D): closed psi -> (ff2 = falsity_on -> forall u rho xi, rho ⊩(u,M) (psi → xi)) -> A ⊢I phi -> forall u rho, (forall psi', psi' el (map (fun x => x [psi/⊥]) A) -> rho ⊩(u,M) psi') -> rho ⊩(u,M) (phi[psi/⊥]).
proof: Proof. intros Hclosed Hexpl Hprv. remember intu as s. revert psi Hexpl Hclosed. induction Hprv; intros newbot Hexp Hclosed; subst; cbn; intros u rho HA. all: repeat (clean_ksoundness + discriminate). all: (eauto || comp; eauto). - intros v Hr Hpi. eapply IHHprv. 1-2:easy. intros ? []; subst; eauto using ksat_mon. - eapply IHHprv1. 1-2:easy. 3: eapply IHHprv2. all: eauto. apply M. - intros d. apply IHHprv. 1-2: now rewrite subst_closed. intros xi [psi' [<- [psi'' [<- Hpsi'']]%in_map_iff]] % in_map_iff. rewrite <- subst_falsity_comm. rewrite ksat_comp. apply HA, in_map, Hpsi''. - erewrite <- (subst_closed _ Hclosed). rewrite <- subst_falsity_comm. rewrite ksat_comp. eapply ksat_ext. 2: { specialize (IHHprv newbot Hexp Hclosed). rewrite subst_closed in IHHprv. 2:easy. now eapply (IHHprv u rho HA (eval rho t)). } unfold funcomp. now intros []. - apply (Hexp u rho). 1: apply M. apply IHHprv. 1-2:easy. apply HA. - now eapply HA, in_map. Qed.
imports: Undecidability(FOL.Semantics.Kripke.FragmentCore FOL.Deduction.FragmentND) Undecidability(Shared.ListAutomation)