Formalized Formal Logic

3.2.Β Neighborhood Semantics

3.2.1.Β Minimal Modal Logic

Minimal modal logic needs only modal equivalence rule (Hilbert.WithRE.re), not necessitation rule.

πŸ”—inductive predicate
LO.Modal.Hilbert.WithRE.{u_1} {Ξ± : Type u_1} (Ax : Axiom Ξ±) : Logic Ξ±
LO.Modal.Hilbert.WithRE.{u_1}
  {Ξ± : Type u_1} (Ax : Axiom Ξ±) : Logic Ξ±

Constructors

axm.{u_1} {Ξ± : Type u_1} {Ax : Axiom Ξ±} {Ο† : Formula Ξ±}
  (s : Substitution Ξ±) : Ο† ∈ Ax β†’ Hilbert.WithRE Ax (Ο†βŸ¦s⟧)
mdp.{u_1} {Ξ± : Type u_1} {Ax : Axiom Ξ±} {Ο† ψ : Formula Ξ±} :
  Hilbert.WithRE Ax (Ο† ➝ ψ) β†’
    Hilbert.WithRE Ax Ο† β†’ Hilbert.WithRE Ax ψ
re.{u_1} {Ξ± : Type u_1} {Ax : Axiom Ξ±} {Ο† ψ : Formula Ξ±} :
  Hilbert.WithRE Ax (Ο† β­€ ψ) β†’ Hilbert.WithRE Ax (β–‘Ο† β­€ β–‘Οˆ)
imply₁.{u_1} {Ξ± : Type u_1} {Ax : Axiom Ξ±}
  (Ο† ψ : Formula Ξ±) : Hilbert.WithRE Ax (Axioms.Imply₁ Ο† ψ)
implyβ‚‚.{u_1} {Ξ± : Type u_1} {Ax : Axiom Ξ±}
  (Ο† ψ Ο‡ : Formula Ξ±) :
  Hilbert.WithRE Ax (Axioms.Implyβ‚‚ Ο† ψ Ο‡)
ec.{u_1} {Ξ± : Type u_1} {Ax : Axiom Ξ±} (Ο† ψ : Formula Ξ±) :
  Hilbert.WithRE Ax (Axioms.ElimContra Ο† ψ)

3.2.2.Β Neighborhood Semantics

TODO

3.2.3.Β Canonical Model

TODO

3.2.4.Β Filtration

Filtration for transitive axioms 4 is proposed in KopnevΒ (2023)K. Kopnev,Β 2023. β€œThe Finite Model Property of Some Non-normal Modal Logics with the Transitivity Axiom”. arXiv:2305.08605. For this purpose, we need basis filtration, transitiveFiltration.

πŸ”—def
LO.Modal.Neighborhood.transitiveFiltration (M : Model) [M.IsTransitive]
  (T : FormulaSet β„•) [T.IsSubformulaClosed] : Filtration M T
LO.Modal.Neighborhood.transitiveFiltration
  (M : Model) [M.IsTransitive]
  (T : FormulaSet β„•)
  [T.IsSubformulaClosed] : Filtration M T

As the name suggests, transitiveFiltration is transitive.

πŸ”—theorem
LO.Modal.Neighborhood.transitiveFiltration.isTransitive {M : Model}
  {T : FormulaSet β„•} [T.IsSubformulaClosed] [M.IsTransitive] :
  (transitiveFiltration M T).toModel.IsTransitive
LO.Modal.Neighborhood.transitiveFiltration.isTransitive
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed]
  [M.IsTransitive] :
  (transitiveFiltration M
        T).toModel.IsTransitive

Reflexivity is preserved when original model is reflexive.

πŸ”—theorem
LO.Modal.Neighborhood.transitiveFiltration.isReflexive {M : Model}
  {T : FormulaSet β„•} [T.IsSubformulaClosed] [M.IsTransitive]
  [M.IsReflexive] : (transitiveFiltration M T).toModel.IsReflexive
LO.Modal.Neighborhood.transitiveFiltration.isReflexive
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed] [M.IsTransitive]
  [M.IsReflexive] :
  (transitiveFiltration M
        T).toModel.IsReflexive

To show that contains-unit property is preserved is not trivial, it needs that β–‘βŠ€ is in the filter.

πŸ”—theorem
LO.Modal.Neighborhood.transitiveFiltration.containsUnit {M : Model}
  {T : FormulaSet β„•} [T.IsSubformulaClosed] [M.IsTransitive]
  [M.ContainsUnit] (hT : β–‘βŠ€ ∈ T) :
  (transitiveFiltration M T).toModel.ContainsUnit
LO.Modal.Neighborhood.transitiveFiltration.containsUnit
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed] [M.IsTransitive]
  [M.ContainsUnit] (hT : β–‘βŠ€ ∈ T) :
  (transitiveFiltration M
        T).toModel.ContainsUnit

We expand transitiveFiltration to suites for several logics. First one is for monotonicity, we add supplementation for transitiveFiltration.

πŸ”—def
LO.Modal.Neighborhood.supplementedTransitiveFiltration (M : Model)
  [M.IsMonotonic] [M.IsTransitive] (T : FormulaSet β„•)
  [T.IsSubformulaClosed] : Filtration M T
LO.Modal.Neighborhood.supplementedTransitiveFiltration
  (M : Model) [M.IsMonotonic]
  [M.IsTransitive] (T : FormulaSet β„•)
  [T.IsSubformulaClosed] : Filtration M T

By supplementation, monotonicity is recovered.

πŸ”—theorem
LO.Modal.Neighborhood.supplementedTransitiveFiltration.isMonotonic
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] :
  (supplementedTransitiveFiltration M T).toModel.IsMonotonic
LO.Modal.Neighborhood.supplementedTransitiveFiltration.isMonotonic
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] :
  (supplementedTransitiveFiltration M
        T).toModel.IsMonotonic

Similarly, transitivity, reflexivity and contains-unit property is preserved (of course contains-unit needs β–‘βŠ€ is in filter).

πŸ”—theorem
LO.Modal.Neighborhood.supplementedTransitiveFiltration.isTransitive
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] :
  (supplementedTransitiveFiltration M T).toModel.IsTransitive
LO.Modal.Neighborhood.supplementedTransitiveFiltration.isTransitive
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] :
  (supplementedTransitiveFiltration M
        T).toModel.IsTransitive
πŸ”—theorem
LO.Modal.Neighborhood.supplementedTransitiveFiltration.isReflexive
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] [M.IsReflexive] :
  (supplementedTransitiveFiltration M T).toModel.IsReflexive
LO.Modal.Neighborhood.supplementedTransitiveFiltration.isReflexive
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] [M.IsReflexive] :
  (supplementedTransitiveFiltration M
        T).toModel.IsReflexive
πŸ”—theorem
LO.Modal.Neighborhood.supplementedTransitiveFiltration.containsUnit
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] [M.ContainsUnit] (hT : β–‘βŠ€ ∈ T) :
  (supplementedTransitiveFiltration M T).toModel.ContainsUnit
LO.Modal.Neighborhood.supplementedTransitiveFiltration.containsUnit
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed] [M.IsMonotonic]
  [M.IsTransitive] [M.ContainsUnit]
  (hT : β–‘βŠ€ ∈ T) :
  (supplementedTransitiveFiltration M
        T).toModel.ContainsUnit

Second one is for regularity, we add quasi-filtering for transitiveFiltration.

πŸ”—def
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration (M : Model)
  [M.IsMonotonic] [M.IsTransitive] [M.IsRegular] (T : FormulaSet β„•)
  [T.IsSubformulaClosed] (hT : Set.Finite T) : Filtration M T
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration
  (M : Model) [M.IsMonotonic]
  [M.IsTransitive] [M.IsRegular]
  (T : FormulaSet β„•)
  [T.IsSubformulaClosed]
  (hT : Set.Finite T) : Filtration M T

By quasi-filtering, regularity is recovered.

πŸ”—theorem
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isRegular
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed]
  {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] :
  (quasiFilteringTransitiveFiltration M T T_finite).toModel.IsRegular
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isRegular
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed]
  {T_finite : Set.Finite T}
  [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] :
  (quasiFilteringTransitiveFiltration M T
        T_finite).toModel.IsRegular

Similarly, Transitivity and reflexivity are preserved, and contains-unit property is preserved.

πŸ”—theorem
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isMonotonic
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed]
  {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] :
  (quasiFilteringTransitiveFiltration M T T_finite).toModel.IsMonotonic
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isMonotonic
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed]
  {T_finite : Set.Finite T}
  [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] :
  (quasiFilteringTransitiveFiltration M T
        T_finite).toModel.IsMonotonic
πŸ”—theorem
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isTransitive
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed]
  {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] :
  (quasiFilteringTransitiveFiltration M T T_finite).toModel.IsTransitive
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isTransitive
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed]
  {T_finite : Set.Finite T}
  [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] :
  (quasiFilteringTransitiveFiltration M T
        T_finite).toModel.IsTransitive
πŸ”—theorem
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.containsUnit
  {M : Model} {T : FormulaSet β„•} [T.IsSubformulaClosed]
  {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] [M.ContainsUnit] (hT : β–‘βŠ€ ∈ T) :
  (quasiFilteringTransitiveFiltration M T T_finite).toModel.ContainsUnit
LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.containsUnit
  {M : Model} {T : FormulaSet β„•}
  [T.IsSubformulaClosed]
  {T_finite : Set.Finite T}
  [M.IsMonotonic] [M.IsTransitive]
  [M.IsRegular] [M.ContainsUnit]
  (hT : β–‘βŠ€ ∈ T) :
  (quasiFilteringTransitiveFiltration M T
        T_finite).toModel.ContainsUnit

3.2.5.Β Logics

We summarize the soundness and completeness in neighborhood semantics for the several minimal modal logics.

3.2.5.1.Β For Modal.E

πŸ”—def
LO.Modal.Neighborhood.FrameClass.E : FrameClass
LO.Modal.Neighborhood.FrameClass.E :
  FrameClass
πŸ”—theorem
LO.Modal.E.Neighborhood.sound : Sound Modal.E FrameClass.E
LO.Modal.E.Neighborhood.sound :
  Sound Modal.E FrameClass.E
πŸ”—theorem
LO.Modal.E.Neighborhood.complete : Complete Modal.E FrameClass.E
LO.Modal.E.Neighborhood.complete :
  Complete Modal.E FrameClass.E

Next we consider combinations of basic axioms in neighborhood semantics.

3.2.5.2.Β For Modal.EM

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EM : FrameClass
LO.Modal.Neighborhood.FrameClass.EM :
  FrameClass
πŸ”—theorem
LO.Modal.EM.Neighborhood.sound : Sound Modal.EM FrameClass.EM
LO.Modal.EM.Neighborhood.sound :
  Sound Modal.EM FrameClass.EM
πŸ”—theorem
LO.Modal.EM.Neighborhood.complete : Complete Modal.EM FrameClass.EM
LO.Modal.EM.Neighborhood.complete :
  Complete Modal.EM FrameClass.EM

3.2.5.3.Β For Modal.EC

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EC : FrameClass
LO.Modal.Neighborhood.FrameClass.EC :
  FrameClass
πŸ”—theorem
LO.Modal.EC.Neighborhood.sound : Sound Modal.EC FrameClass.EC
LO.Modal.EC.Neighborhood.sound :
  Sound Modal.EC FrameClass.EC
πŸ”—theorem
LO.Modal.EC.Neighborhood.complete : Complete Modal.EC FrameClass.EC
LO.Modal.EC.Neighborhood.complete :
  Complete Modal.EC FrameClass.EC

3.2.5.4.Β For Modal.EN

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EN : FrameClass
LO.Modal.Neighborhood.FrameClass.EN :
  FrameClass
πŸ”—theorem
LO.Modal.EN.Neighborhood.sound : Sound Modal.EN FrameClass.EN
LO.Modal.EN.Neighborhood.sound :
  Sound Modal.EN FrameClass.EN
πŸ”—theorem
LO.Modal.EN.Neighborhood.complete : Complete Modal.EN FrameClass.EN
LO.Modal.EN.Neighborhood.complete :
  Complete Modal.EN FrameClass.EN

3.2.5.5.Β For Modal.EMC

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMC : FrameClass
LO.Modal.Neighborhood.FrameClass.EMC :
  FrameClass
πŸ”—theorem
LO.Modal.EMC.Neighborhood.sound : Sound Modal.EMC FrameClass.EMC
LO.Modal.EMC.Neighborhood.sound :
  Sound Modal.EMC FrameClass.EMC
πŸ”—theorem
LO.Modal.EMC.Neighborhood.complete : Complete Modal.EMC FrameClass.EMC
LO.Modal.EMC.Neighborhood.complete :
  Complete Modal.EMC FrameClass.EMC

3.2.5.6.Β For Modal.ECN

πŸ”—def
LO.Modal.Neighborhood.FrameClass.ECN : FrameClass
LO.Modal.Neighborhood.FrameClass.ECN :
  FrameClass
πŸ”—theorem
LO.Modal.ECN.Neighborhood.sound : Sound Modal.ECN FrameClass.ECN
LO.Modal.ECN.Neighborhood.sound :
  Sound Modal.ECN FrameClass.ECN
πŸ”—theorem
LO.Modal.ECN.Neighborhood.complete : Complete Modal.ECN FrameClass.ECN
LO.Modal.ECN.Neighborhood.complete :
  Complete Modal.ECN FrameClass.ECN

3.2.5.7.Β For Modal.EMN

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMN : FrameClass
LO.Modal.Neighborhood.FrameClass.EMN :
  FrameClass
πŸ”—theorem
LO.Modal.EMN.Neighborhood.sound : Sound Modal.EMN FrameClass.EMN
LO.Modal.EMN.Neighborhood.sound :
  Sound Modal.EMN FrameClass.EMN
πŸ”—theorem
LO.Modal.EMN.Neighborhood.complete : Complete Modal.EMN FrameClass.EMN
LO.Modal.EMN.Neighborhood.complete :
  Complete Modal.EMN FrameClass.EMN

3.2.5.8.Β For Modal.EMCN

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMCN : FrameClass
LO.Modal.Neighborhood.FrameClass.EMCN :
  FrameClass
πŸ”—theorem
LO.Modal.EMCN.Neighborhood.sound : Sound Modal.EMCN FrameClass.EMCN
LO.Modal.EMCN.Neighborhood.sound :
  Sound Modal.EMCN FrameClass.EMCN
πŸ”—theorem
LO.Modal.EMCN.Neighborhood.complete :
  Complete Modal.EMCN FrameClass.EMCN
LO.Modal.EMCN.Neighborhood.complete :
  Complete Modal.EMCN FrameClass.EMCN

Since Modal.K is equivalent to Modal.EMCN, so Modal.K is also sound and complete with respect to neighborhood semantics.

Next consider additional axioms.

3.2.5.9.Β For Modal.E4

πŸ”—def
LO.Modal.Neighborhood.FrameClass.E4 : FrameClass
LO.Modal.Neighborhood.FrameClass.E4 :
  FrameClass
πŸ”—theorem
LO.Modal.E4.Neighborhood.sound : Sound Modal.E4 FrameClass.E4
LO.Modal.E4.Neighborhood.sound :
  Sound Modal.E4 FrameClass.E4
πŸ”—theorem
LO.Modal.E4.Neighborhood.complete : Complete Modal.E4 FrameClass.E4
LO.Modal.E4.Neighborhood.complete :
  Complete Modal.E4 FrameClass.E4

By using transitiveFiltration, we can show that Modal.E4 enjoys FFP.

πŸ”—theorem
LO.Modal.E4.Neighborhood.finite_complete :
  Complete Modal.E4 FrameClass.finite_E4
LO.Modal.E4.Neighborhood.finite_complete :
  Complete Modal.E4 FrameClass.finite_E4

3.2.5.10.Β For Modal.ET4

πŸ”—def
LO.Modal.Neighborhood.FrameClass.ET4 : FrameClass
LO.Modal.Neighborhood.FrameClass.ET4 :
  FrameClass
πŸ”—theorem
LO.Modal.ET4.Neighborhood.sound : Sound Modal.ET4 FrameClass.ET4
LO.Modal.ET4.Neighborhood.sound :
  Sound Modal.ET4 FrameClass.ET4
πŸ”—theorem
LO.Modal.ET4.Neighborhood.complete : Complete Modal.ET4 FrameClass.ET4
LO.Modal.ET4.Neighborhood.complete :
  Complete Modal.ET4 FrameClass.ET4

By using transitiveFiltration, we can show that Modal.ET4 enjoys FFP.

πŸ”—theorem
LO.Modal.ET4.Neighborhood.finite_complete :
  Complete Modal.ET4 FrameClass.finite_ET4
LO.Modal.ET4.Neighborhood.finite_complete :
  Complete Modal.ET4 FrameClass.finite_ET4

3.2.5.11.Β For Modal.ENT4

Similar to Modal.ET4.

πŸ”—def
LO.Modal.Neighborhood.FrameClass.ENT4 : FrameClass
LO.Modal.Neighborhood.FrameClass.ENT4 :
  FrameClass
πŸ”—theorem
LO.Modal.ENT4.Neighborhood.sound : Sound Modal.ENT4 FrameClass.ENT4
LO.Modal.ENT4.Neighborhood.sound :
  Sound Modal.ENT4 FrameClass.ENT4
πŸ”—theorem
LO.Modal.ENT4.Neighborhood.complete :
  Complete Modal.ENT4 FrameClass.ENT4
LO.Modal.ENT4.Neighborhood.complete :
  Complete Modal.ENT4 FrameClass.ENT4
πŸ”—theorem
LO.Modal.ENT4.Neighborhood.finite_complete :
  Complete Modal.ENT4 FrameClass.finite_ENT4
LO.Modal.ENT4.Neighborhood.finite_complete :
  Complete Modal.ENT4
    FrameClass.finite_ENT4

3.2.5.12.Β For Modal.EMT4

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMT4 : FrameClass
LO.Modal.Neighborhood.FrameClass.EMT4 :
  FrameClass
πŸ”—theorem
LO.Modal.EMT4.Neighborhood.sound : Sound Modal.EMT4 FrameClass.EMT4
LO.Modal.EMT4.Neighborhood.sound :
  Sound Modal.EMT4 FrameClass.EMT4
πŸ”—theorem
LO.Modal.EMT4.Neighborhood.complete :
  Complete Modal.EMT4 FrameClass.EMT4
LO.Modal.EMT4.Neighborhood.complete :
  Complete Modal.EMT4 FrameClass.EMT4

By using supplementedTransitiveFiltration, we can show that Modal.EMT4 enjoys FFP.

πŸ”—theorem
LO.Modal.EMT4.Neighborhood.finite_complete :
  Complete Modal.EMT4 FrameClass.finite_EMT4
LO.Modal.EMT4.Neighborhood.finite_complete :
  Complete Modal.EMT4
    FrameClass.finite_EMT4

3.2.5.13.Β For Modal.EMNT4

Similar to Modal.EMT4.

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMNT4 : FrameClass
LO.Modal.Neighborhood.FrameClass.EMNT4 :
  FrameClass
πŸ”—theorem
LO.Modal.EMNT4.Neighborhood.sound : Sound Modal.EMNT4 FrameClass.EMNT4
LO.Modal.EMNT4.Neighborhood.sound :
  Sound Modal.EMNT4 FrameClass.EMNT4
πŸ”—theorem
LO.Modal.EMNT4.Neighborhood.complete :
  Complete Modal.EMNT4 FrameClass.EMNT4
LO.Modal.EMNT4.Neighborhood.complete :
  Complete Modal.EMNT4 FrameClass.EMNT4
πŸ”—theorem
LO.Modal.EMNT4.Neighborhood.finite_complete :
  Complete Modal.EMNT4 FrameClass.finite_EMNT4
LO.Modal.EMNT4.Neighborhood.finite_complete :
  Complete Modal.EMNT4
    FrameClass.finite_EMNT4

3.2.5.14.Β For Modal.EMC4

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMC4 : FrameClass
LO.Modal.Neighborhood.FrameClass.EMC4 :
  FrameClass
πŸ”—theorem
LO.Modal.EMC4.Neighborhood.sound : Sound Modal.EMC4 FrameClass.EMC4
LO.Modal.EMC4.Neighborhood.sound :
  Sound Modal.EMC4 FrameClass.EMC4
πŸ”—theorem
LO.Modal.EMC4.Neighborhood.complete :
  Complete Modal.EMC4 FrameClass.EMC4
LO.Modal.EMC4.Neighborhood.complete :
  Complete Modal.EMC4 FrameClass.EMC4

By using quasiFilteringTransitiveFiltration, we can show that Modal.EMC4 enjoys FFP.

πŸ”—theorem
LO.Modal.EMC4.Neighborhood.finite_complete :
  Complete Modal.EMC4 FrameClass.finite_EMC4
LO.Modal.EMC4.Neighborhood.finite_complete :
  Complete Modal.EMC4
    FrameClass.finite_EMC4

3.2.5.15.Β For Modal.EMCN4

Similar to Modal.EMC4.

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMCN4 : FrameClass
LO.Modal.Neighborhood.FrameClass.EMCN4 :
  FrameClass
πŸ”—theorem
LO.Modal.EMCN4.Neighborhood.sound : Sound Modal.EMCN4 FrameClass.EMCN4
LO.Modal.EMCN4.Neighborhood.sound :
  Sound Modal.EMCN4 FrameClass.EMCN4
πŸ”—theorem
LO.Modal.EMCN4.Neighborhood.complete :
  Complete Modal.EMCN4 FrameClass.EMCN4
LO.Modal.EMCN4.Neighborhood.complete :
  Complete Modal.EMCN4 FrameClass.EMCN4
πŸ”—theorem
LO.Modal.EMCN4.Neighborhood.finite_complete :
  Complete Modal.EMCN4 FrameClass.finite_EMCN4
LO.Modal.EMCN4.Neighborhood.finite_complete :
  Complete Modal.EMCN4
    FrameClass.finite_EMCN4

3.2.5.16.Β For Modal.ED

πŸ”—def
LO.Modal.Neighborhood.FrameClass.ED : FrameClass
LO.Modal.Neighborhood.FrameClass.ED :
  FrameClass
πŸ”—theorem
LO.Modal.ED.Neighborhood.sound : Sound Modal.ED FrameClass.ED
LO.Modal.ED.Neighborhood.sound :
  Sound Modal.ED FrameClass.ED

3.2.5.17.Β For Modal.E5

πŸ”—def
LO.Modal.Neighborhood.FrameClass.E5 : FrameClass
LO.Modal.Neighborhood.FrameClass.E5 :
  FrameClass
πŸ”—theorem
LO.Modal.E5.Neighborhood.sound : Sound Modal.E5 FrameClass.E5
LO.Modal.E5.Neighborhood.sound :
  Sound Modal.E5 FrameClass.E5
πŸ”—theorem
LO.Modal.E5.Neighborhood.complete : Complete Modal.E5 FrameClass.E5
LO.Modal.E5.Neighborhood.complete :
  Complete Modal.E5 FrameClass.E5

3.2.5.18.Β For Modal.ET

πŸ”—def
LO.Modal.Neighborhood.FrameClass.ET : FrameClass
LO.Modal.Neighborhood.FrameClass.ET :
  FrameClass
πŸ”—theorem
LO.Modal.ET.Neighborhood.sound : Sound Modal.ET FrameClass.ET
LO.Modal.ET.Neighborhood.sound :
  Sound Modal.ET FrameClass.ET
πŸ”—theorem
LO.Modal.ET.Neighborhood.complete : Complete Modal.ET FrameClass.ET
LO.Modal.ET.Neighborhood.complete :
  Complete Modal.ET FrameClass.ET

3.2.5.19.Β For Modal.EMT

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EMT : FrameClass
LO.Modal.Neighborhood.FrameClass.EMT :
  FrameClass
πŸ”—theorem
LO.Modal.EMT.Neighborhood.sound : Sound Modal.EMT FrameClass.EMT
LO.Modal.EMT.Neighborhood.sound :
  Sound Modal.EMT FrameClass.EMT
πŸ”—theorem
LO.Modal.EMT.Neighborhood.complete : Complete Modal.EMT FrameClass.EMT
LO.Modal.EMT.Neighborhood.complete :
  Complete Modal.EMT FrameClass.EMT

3.2.5.20.Β For Modal.EP

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EP : FrameClass
LO.Modal.Neighborhood.FrameClass.EP :
  FrameClass
πŸ”—theorem
LO.Modal.EP.Neighborhood.sound : Sound Modal.EP FrameClass.EP
LO.Modal.EP.Neighborhood.sound :
  Sound Modal.EP FrameClass.EP

3.2.5.21.Β For Modal.EN4

πŸ”—def
LO.Modal.Neighborhood.FrameClass.EN4 : FrameClass
LO.Modal.Neighborhood.FrameClass.EN4 :
  FrameClass
πŸ”—theorem
LO.Modal.EN4.Neighborhood.sound : Sound Modal.EN4 FrameClass.EN4
LO.Modal.EN4.Neighborhood.sound :
  Sound Modal.EN4 FrameClass.EN4
πŸ”—theorem
LO.Modal.EN4.Neighborhood.complete : Complete Modal.EN4 FrameClass.EN4
LO.Modal.EN4.Neighborhood.complete :
  Complete Modal.EN4 FrameClass.EN4

3.2.5.22.Β For Modal.END

πŸ”—def
LO.Modal.Neighborhood.FrameClass.END : FrameClass
LO.Modal.Neighborhood.FrameClass.END :
  FrameClass
πŸ”—theorem
LO.Modal.END.Neighborhood.sound : Sound Modal.END FrameClass.END
LO.Modal.END.Neighborhood.sound :
  Sound Modal.END FrameClass.END

3.2.5.23.Β For Modal.END4

πŸ”—def
LO.Modal.Neighborhood.FrameClass.END4 : FrameClass
LO.Modal.Neighborhood.FrameClass.END4 :
  FrameClass
πŸ”—theorem
LO.Modal.END4.Neighborhood.sound : Sound Modal.END4 FrameClass.END4
LO.Modal.END4.Neighborhood.sound :
  Sound Modal.END4 FrameClass.END4