Theory FL_Logical_Equivalence

theory FL_Logical_Equivalence
imports
  FL_Validity
begin

section ‹(Strong) Logical Equivalence›

text ‹The definition of formulas is parametric in the index type, but from now on we want to work
with a fixed (sufficiently large) index type.›

locale indexed_effect_nominal_ts = effect_nominal_ts satisfies transition effect_apply
  for satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix ‹⊢› 70)
  and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool" (infix ‹→› 70)
  and effect_apply :: "'effect::fs ⇒ 'state ⇒ 'state" (‹⟨_⟩_› [0,101] 100) +
  assumes card_idx_perm: "|UNIV::perm set| <o |UNIV::'idx set|"
      and card_idx_state: "|UNIV::'state set| <o |UNIV::'idx set|"
begin

  definition FL_logically_equivalent :: "'effect first ⇒ 'state ⇒ 'state ⇒ bool" where
    "FL_logically_equivalent F P Q ≡
       ∀x::('idx,'pred,'act,'effect) formula. x ∈ 𝒜[F] ⟶ (P ⊨ x ⟷ Q ⊨ x)"

  text ‹We could (but didn't need to) prove that this defines an equivariant equivalence relation.›

end

end