Theory TAO_2_Semantics

(*<*)
theory TAO_2_Semantics
imports 
  TAO_1_Embedding 
  "HOL-Eisbach.Eisbach"
begin
(*>*)

section‹Semantic Abstraction›
text‹\label{TAO_Semantics}›

subsection‹Semantics›
text‹\label{TAO_Semantics_Semantics}›

locale Semantics
begin
  named_theorems semantics

  subsubsection‹Semantic Domains›
  text‹\label{TAO_Semantics_Semantics_Domains}›
  type_synonym R⇩κ = "ν"
  type_synonym R⇩0 = "j⇒i⇒bool"
  type_synonym R⇩1 = "υ⇒R⇩0"
  type_synonym R⇩2 = "υ⇒υ⇒R⇩0"
  type_synonym R⇩3 = "υ⇒υ⇒υ⇒R⇩0"
  type_synonym W = i

  subsubsection‹Denotation Functions›
  text‹\label{TAO_Semantics_Semantics_Denotations}›

  lift_definition d⇩κ :: "κ⇒R⇩κ option" is id .
  lift_definition d⇩0 :: "Π⇩0⇒R⇩0 option" is Some .
  lift_definition d⇩1 :: "Π⇩1⇒R⇩1 option" is Some .
  lift_definition d⇩2 :: "Π⇩2⇒R⇩2 option" is Some .
  lift_definition d⇩3 :: "Π⇩3⇒R⇩3 option" is Some .

  subsubsection‹Actual World›
  text‹\label{TAO_Semantics_Semantics_Actual_World}›
  definition w⇩0 where "w⇩0 ≡ dw"

  subsubsection‹Exemplification Extensions›
  text‹\label{TAO_Semantics_Semantics_Exemplification_Extensions}›

  definition ex0 :: "R⇩0⇒W⇒bool"
    where "ex0 ≡ λ F . F dj"
  definition ex1 :: "R⇩1⇒W⇒(R⇩κ set)"
    where "ex1 ≡ λ F w . { x . F (νυ x) dj w }"
  definition ex2 :: "R⇩2⇒W⇒((R⇩κ×R⇩κ) set)"
    where "ex2 ≡ λ F w . { (x,y) . F (νυ x) (νυ y) dj w }"
  definition ex3 :: "R⇩3⇒W⇒((R⇩κ×R⇩κ×R⇩κ) set)"
    where "ex3 ≡ λ F w . { (x,y,z) . F (νυ x) (νυ y) (νυ z) dj w }"

  subsubsection‹Encoding Extensions›
  text‹\label{TAO_Semantics_Semantics_Encoding_Extension}›

  definition en :: "R⇩1⇒(R⇩κ set)"
    where "en ≡ λ F . { x . case x of αν y ⇒ makeΠ⇩1 (λ x . F x) ∈ y
                                       | _ ⇒ False }"

  subsubsection‹Collection of Semantic Definitions›
  text‹\label{TAO_Semantics_Semantics_Definitions}›

  named_theorems semantics_defs
  declare d⇩0_def[semantics_defs] d⇩1_def[semantics_defs]
          d⇩2_def[semantics_defs] d⇩3_def[semantics_defs]
          ex0_def[semantics_defs] ex1_def[semantics_defs]
          ex2_def[semantics_defs] ex3_def[semantics_defs]
          en_def[semantics_defs] d⇩κ_def[semantics_defs]
          w⇩0_def[semantics_defs]

  subsubsection‹Truth Conditions of Exemplification Formulas›
  text‹\label{TAO_Semantics_Semantics_Exemplification}›

  lemma T1_1[semantics]:
    "(w ⊨ ⦇F,x⦈) = (∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ ex1 r w)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def)
    by (metis option.discI option.exhaust option.sel)

  lemma T1_2[semantics]:
    "(w ⊨ ⦇F,x,y⦈) = (∃ r o⇩1 o⇩2 . Some r = d⇩2 F ∧ Some o⇩1 = d⇩κ x
                               ∧ Some o⇩2 = d⇩κ y ∧ (o⇩1, o⇩2) ∈ ex2 r w)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def)
    by (metis option.discI option.exhaust option.sel)

  lemma T1_3[semantics]:
    "(w ⊨ ⦇F,x,y,z⦈) = (∃ r o⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
                                    ∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
                                    ∧ (o⇩1, o⇩2, o⇩3) ∈ ex3 r w)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def)
    by (metis option.discI option.exhaust option.sel)

  lemma T3[semantics]:
    "(w ⊨ ⦇F⦈) = (∃ r . Some r = d⇩0 F ∧ ex0 r w)"
    unfolding semantics_defs
    by (simp add: meta_defs meta_aux)

  subsubsection‹Truth Conditions of Encoding Formulas›
  text‹\label{TAO_Semantics_Semantics_Encoding}›

  lemma T2[semantics]:
    "(w ⊨ ⦃x,F⦄) = (∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ en r)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def split: ν.split)
    by (metis ν.exhaust ν.inject(2) ν.simps(4) νκ.rep_eq option.collapse
              option.discI rep.rep_eq rep_proper_id)

  subsubsection‹Truth Conditions of Complex Formulas›
  text‹\label{TAO_Semantics_Semantics_Complex_Formulas}›

  lemma T4[semantics]: "(w ⊨ ❙¬ψ) = (¬(w ⊨ ψ))"
    by (simp add: meta_defs meta_aux)

  lemma T5[semantics]: "(w ⊨ ψ ❙→ χ) = (¬(w ⊨ ψ) ∨ (w ⊨ χ))"
    by (simp add: meta_defs meta_aux)

  lemma T6[semantics]: "(w ⊨ ❙□ψ) = (∀ v . (v ⊨ ψ))"
    by (simp add: meta_defs meta_aux)

  lemma T7[semantics]: "(w ⊨ ❙𝒜ψ) = (dw ⊨ ψ)"
    by (simp add: meta_defs meta_aux)

  lemma T8_ν[semantics]: "(w ⊨ ❙∀⇩ν x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_0[semantics]: "(w ⊨ ❙∀⇩0 x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_1[semantics]: "(w ⊨ ❙∀⇩1 x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_2[semantics]: "(w ⊨ ❙∀⇩2 x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_3[semantics]: "(w ⊨ ❙∀⇩3 x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_𝗈[semantics]: "(w ⊨ ❙∀⇩𝗈 x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  subsubsection‹Denotations of Descriptions›
  text‹\label{TAO_Semantics_Semantics_Descriptions}›

  lemma D3[semantics]:
    "d⇩κ (❙ιx . ψ x) = (if (∃x . (w⇩0 ⊨ ψ x) ∧ (∀ y . (w⇩0  ⊨ ψ y) ⟶ y = x))
                      then (Some (THE x . (w⇩0 ⊨ ψ x))) else None)"
    unfolding semantics_defs
    by (auto simp: meta_defs meta_aux)

  subsubsection‹Denotations of Lambda Expressions›
  text‹\label{TAO_Semantics_Semantics_Lambda_Expressions}›

  lemma D4_1[semantics]: "d⇩1 (❙λ x . ⦇F, x⇧P⦈) = d⇩1 F"
    by (simp add: meta_defs meta_aux)

  lemma D4_2[semantics]: "d⇩2 (❙λ⇧2 (λ x y . ⦇F, x⇧P, y⇧P⦈)) = d⇩2 F"
    by (simp add: meta_defs meta_aux)

  lemma D4_3[semantics]: "d⇩3 (❙λ⇧3 (λ x y z . ⦇F, x⇧P, y⇧P, z⇧P⦈)) = d⇩3 F"
    by (simp add: meta_defs meta_aux)

  lemma D5_1[semantics]:
    assumes "IsProperInX φ"
    shows "⋀ w o⇩1 r . Some r = d⇩1 (❙λ x . (φ (x⇧P))) ∧ Some o⇩1 = d⇩κ x
                      ⟶ (o⇩1 ∈ ex1 r w) = (w ⊨ φ x)"
    using assms unfolding IsProperInX_def semantics_defs
    by (auto simp: meta_defs meta_aux rep_def proper_def νκ.abs_eq)

  lemma D5_2[semantics]:
    assumes "IsProperInXY φ"
    shows "⋀ w o⇩1 o⇩2 r . Some r = d⇩2 (❙λ⇧2 (λ x y . φ (x⇧P) (y⇧P)))
                       ∧ Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y
                       ⟶ ((o⇩1,o⇩2) ∈ ex2 r w) = (w ⊨ φ x y)"
    using assms unfolding IsProperInXY_def semantics_defs
    by (auto simp: meta_defs meta_aux rep_def proper_def νκ.abs_eq)

  lemma D5_3[semantics]:
    assumes "IsProperInXYZ φ"
    shows "⋀ w o⇩1 o⇩2 o⇩3 r . Some r = d⇩3 (❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P)))
                          ∧ Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
                          ⟶ ((o⇩1,o⇩2,o⇩3) ∈ ex3 r w) = (w ⊨ φ x y z)"
    using assms unfolding IsProperInXYZ_def semantics_defs
    by (auto simp: meta_defs meta_aux rep_def proper_def νκ.abs_eq)

  lemma D6[semantics]: "(⋀ w r . Some r = d⇩0 (❙λ⇧0 φ) ⟶ ex0 r w = (w ⊨ φ))"
    by (auto simp: meta_defs meta_aux semantics_defs)

  subsubsection‹Auxiliary Lemmas›
  text‹\label{TAO_Semantics_Semantics_Auxiliary_Lemmata}›

  lemma propex⇩0: "∃ r . Some r = d⇩0 F"
    unfolding d⇩0_def by simp
  lemma propex⇩1: "∃ r . Some r = d⇩1 F"
    unfolding d⇩1_def by simp
  lemma propex⇩2: "∃ r . Some r = d⇩2 F"
    unfolding d⇩2_def by simp
  lemma propex⇩3: "∃ r . Some r = d⇩3 F"
    unfolding d⇩3_def by simp
  lemma d⇩κ_proper: "d⇩κ (u⇧P) = Some u"
    unfolding d⇩κ_def by (simp add: νκ_def meta_aux)
  lemma ConcretenessSemantics1:
    "Some r = d⇩1 E! ⟹ (∃ w . ων x ∈ ex1 r w)"
    unfolding semantics_defs apply transfer
    by (simp add: OrdinaryObjectsPossiblyConcreteAxiom νυ_ων_is_ωυ)
  lemma ConcretenessSemantics2:
    "Some r = d⇩1 E! ⟹ (x ∈ ex1 r w ⟶ (∃y. x = ων y))"
    unfolding semantics_defs apply transfer apply simp
    by (metis ν.exhaust υ.exhaust υ.simps(6) no_αω)
  lemma d⇩0_inject: "⋀x y. d⇩0 x = d⇩0 y ⟹ x = y"
    unfolding d⇩0_def by (simp add: eval𝗈_inject)
  lemma d⇩1_inject: "⋀x y. d⇩1 x = d⇩1 y ⟹ x = y"
    unfolding d⇩1_def by (simp add: evalΠ⇩1_inject)
  lemma d⇩2_inject: "⋀x y. d⇩2 x = d⇩2 y ⟹ x = y"
    unfolding d⇩2_def by (simp add: evalΠ⇩2_inject)
  lemma d⇩3_inject: "⋀x y. d⇩3 x = d⇩3 y ⟹ x = y"
    unfolding d⇩3_def by (simp add: evalΠ⇩3_inject)
  lemma d⇩κ_inject: "⋀x y o⇩1. Some o⇩1 = d⇩κ x ∧ Some o⇩1 = d⇩κ y ⟹ x = y"
  proof -
    fix x :: κ and y :: κ and o⇩1 :: ν
    assume "Some o⇩1 = d⇩κ x ∧ Some o⇩1 = d⇩κ y"
    thus "x = y" apply transfer by auto
  qed
end

subsection‹Introduction Rules for Proper Maps›
text‹\label{TAO_Semantics_Proper}›

text‹
\begin{remark}
  Every map whose arguments only occur in exemplification
  expressions is proper.
\end{remark}
›

named_theorems IsProper_intros

lemma IsProperInX_intro[IsProper_intros]:
  "IsProperInX (λ x . χ
    ― ‹one place:› (λ F . ⦇F,x⦈)
    ― ‹two place:› (λ F . ⦇F,x,x⦈) (λ F a . ⦇F,x,a⦈) (λ F a . ⦇F,a,x⦈)
    ― ‹three place three ‹x›:› (λ F . ⦇F,x,x,x⦈)
    ― ‹three place two ‹x›:› (λ F a . ⦇F,x,x,a⦈) (λ F a . ⦇F,x,a,x⦈)
                            (λ F a . ⦇F,a,x,x⦈)
    ― ‹three place one ‹x›:› (λ F a b. ⦇F,x,a,b⦈) (λ F a b. ⦇F,a,x,b⦈)
                            (λ F a b . ⦇F,a,b,x⦈))"
  unfolding IsProperInX_def
  by (auto simp: meta_defs meta_aux)

lemma IsProperInXY_intro[IsProper_intros]:
  "IsProperInXY (λ x y . χ
    ― ‹only ‹x››
      ― ‹one place:› (λ F . ⦇F,x⦈)
      ― ‹two place:› (λ F . ⦇F,x,x⦈) (λ F a . ⦇F,x,a⦈) (λ F a . ⦇F,a,x⦈)
      ― ‹three place three ‹x›:› (λ F . ⦇F,x,x,x⦈)
      ― ‹three place two ‹x›:› (λ F a . ⦇F,x,x,a⦈) (λ F a . ⦇F,x,a,x⦈)
                              (λ F a . ⦇F,a,x,x⦈)
      ― ‹three place one ‹x›:› (λ F a b. ⦇F,x,a,b⦈) (λ F a b. ⦇F,a,x,b⦈)
                              (λ F a b . ⦇F,a,b,x⦈)
    ― ‹only ‹y››
      ― ‹one place:› (λ F . ⦇F,y⦈)
      ― ‹two place:› (λ F . ⦇F,y,y⦈) (λ F a . ⦇F,y,a⦈) (λ F a . ⦇F,a,y⦈)
      ― ‹three place three ‹y›:› (λ F . ⦇F,y,y,y⦈)
      ― ‹three place two ‹y›:› (λ F a . ⦇F,y,y,a⦈) (λ F a . ⦇F,y,a,y⦈)
                              (λ F a . ⦇F,a,y,y⦈)
      ― ‹three place one ‹y›:› (λ F a b. ⦇F,y,a,b⦈) (λ F a b. ⦇F,a,y,b⦈)
                              (λ F a b . ⦇F,a,b,y⦈)
    ― ‹‹x› and ‹y››
      ― ‹two place:› (λ F . ⦇F,x,y⦈) (λ F . ⦇F,y,x⦈)
      ― ‹three place ‹(x,y)›:› (λ F a . ⦇F,x,y,a⦈) (λ F a . ⦇F,x,a,y⦈)
                              (λ F a . ⦇F,a,x,y⦈)
      ― ‹three place ‹(y,x)›:› (λ F a . ⦇F,y,x,a⦈) (λ F a . ⦇F,y,a,x⦈)
                              (λ F a . ⦇F,a,y,x⦈)
      ― ‹three place ‹(x,x,y)›:› (λ F . ⦇F,x,x,y⦈) (λ F . ⦇F,x,y,x⦈)
                                (λ F . ⦇F,y,x,x⦈)
      ― ‹three place ‹(x,y,y)›:› (λ F . ⦇F,x,y,y⦈) (λ F . ⦇F,y,x,y⦈)
                                (λ F . ⦇F,y,y,x⦈)
      ― ‹three place ‹(x,x,x)›:› (λ F . ⦇F,x,x,x⦈)
      ― ‹three place ‹(y,y,y)›:› (λ F . ⦇F,y,y,y⦈))"
  unfolding IsProperInXY_def by (auto simp: meta_defs meta_aux)

lemma IsProperInXYZ_intro[IsProper_intros]:
  "IsProperInXYZ (λ x y z . χ
    ― ‹only ‹x››
      ― ‹one place:› (λ F . ⦇F,x⦈)
      ― ‹two place:› (λ F . ⦇F,x,x⦈) (λ F a . ⦇F,x,a⦈) (λ F a . ⦇F,a,x⦈)
      ― ‹three place three ‹x›:› (λ F . ⦇F,x,x,x⦈)
      ― ‹three place two ‹x›:› (λ F a . ⦇F,x,x,a⦈) (λ F a . ⦇F,x,a,x⦈)
                              (λ F a . ⦇F,a,x,x⦈)
      ― ‹three place one ‹x›:› (λ F a b. ⦇F,x,a,b⦈) (λ F a b. ⦇F,a,x,b⦈)
                              (λ F a b . ⦇F,a,b,x⦈)
    ― ‹only ‹y››
      ― ‹one place:› (λ F . ⦇F,y⦈)
      ― ‹two place:› (λ F . ⦇F,y,y⦈) (λ F a . ⦇F,y,a⦈) (λ F a . ⦇F,a,y⦈)
      ― ‹three place three ‹y›:› (λ F . ⦇F,y,y,y⦈)
      ― ‹three place two ‹y›:› (λ F a . ⦇F,y,y,a⦈) (λ F a . ⦇F,y,a,y⦈)
                              (λ F a . ⦇F,a,y,y⦈)
      ― ‹three place one ‹y›:› (λ F a b. ⦇F,y,a,b⦈) (λ F a b. ⦇F,a,y,b⦈)
                              (λ F a b . ⦇F,a,b,y⦈)
    ― ‹only ‹z››
      ― ‹one place:› (λ F . ⦇F,z⦈)
      ― ‹two place:› (λ F . ⦇F,z,z⦈) (λ F a . ⦇F,z,a⦈) (λ F a . ⦇F,a,z⦈)
      ― ‹three place three ‹z›:› (λ F . ⦇F,z,z,z⦈)
      ― ‹three place two ‹z›:› (λ F a . ⦇F,z,z,a⦈) (λ F a . ⦇F,z,a,z⦈)
                              (λ F a . ⦇F,a,z,z⦈)
      ― ‹three place one ‹z›:› (λ F a b. ⦇F,z,a,b⦈) (λ F a b. ⦇F,a,z,b⦈)
                              (λ F a b . ⦇F,a,b,z⦈)
    ― ‹‹x› and ‹y››
      ― ‹two place:› (λ F . ⦇F,x,y⦈) (λ F . ⦇F,y,x⦈)
      ― ‹three place ‹(x,y)›:› (λ F a . ⦇F,x,y,a⦈) (λ F a . ⦇F,x,a,y⦈)
                              (λ F a . ⦇F,a,x,y⦈)
      ― ‹three place ‹(y,x)›:› (λ F a . ⦇F,y,x,a⦈) (λ F a . ⦇F,y,a,x⦈)
                              (λ F a . ⦇F,a,y,x⦈)
      ― ‹three place ‹(x,x,y)›:› (λ F . ⦇F,x,x,y⦈) (λ F . ⦇F,x,y,x⦈)
                                (λ F . ⦇F,y,x,x⦈)
      ― ‹three place ‹(x,y,y)›:› (λ F . ⦇F,x,y,y⦈) (λ F . ⦇F,y,x,y⦈)
                                (λ F . ⦇F,y,y,x⦈)
      ― ‹three place ‹(x,x,x)›:› (λ F . ⦇F,x,x,x⦈)
      ― ‹three place ‹(y,y,y)›:› (λ F . ⦇F,y,y,y⦈)
    ― ‹‹x› and ‹z››
      ― ‹two place:› (λ F . ⦇F,x,z⦈) (λ F . ⦇F,z,x⦈)
      ― ‹three place ‹(x,z)›:› (λ F a . ⦇F,x,z,a⦈) (λ F a . ⦇F,x,a,z⦈)
                              (λ F a . ⦇F,a,x,z⦈)
      ― ‹three place ‹(z,x)›:› (λ F a . ⦇F,z,x,a⦈) (λ F a . ⦇F,z,a,x⦈)
                              (λ F a . ⦇F,a,z,x⦈)
      ― ‹three place ‹(x,x,z)›:› (λ F . ⦇F,x,x,z⦈) (λ F . ⦇F,x,z,x⦈)
                                (λ F . ⦇F,z,x,x⦈)
      ― ‹three place ‹(x,z,z)›:› (λ F . ⦇F,x,z,z⦈) (λ F . ⦇F,z,x,z⦈)
                                (λ F . ⦇F,z,z,x⦈)
      ― ‹three place ‹(x,x,x)›:› (λ F . ⦇F,x,x,x⦈)
      ― ‹three place ‹(z,z,z)›:› (λ F . ⦇F,z,z,z⦈)
    ― ‹‹y› and ‹z››
      ― ‹two place:› (λ F . ⦇F,y,z⦈) (λ F . ⦇F,z,y⦈)
      ― ‹three place ‹(y,z)›:› (λ F a . ⦇F,y,z,a⦈) (λ F a . ⦇F,y,a,z⦈)
                              (λ F a . ⦇F,a,y,z⦈)
      ― ‹three place ‹(z,y)›:› (λ F a . ⦇F,z,y,a⦈) (λ F a . ⦇F,z,a,y⦈)
                              (λ F a . ⦇F,a,z,y⦈)
      ― ‹three place ‹(y,y,z)›:› (λ F . ⦇F,y,y,z⦈) (λ F . ⦇F,y,z,y⦈)
                                (λ F . ⦇F,z,y,y⦈)
      ― ‹three place ‹(y,z,z)›:› (λ F . ⦇F,y,z,z⦈) (λ F . ⦇F,z,y,z⦈)
                                (λ F . ⦇F,z,z,y⦈)
      ― ‹three place ‹(y,y,y)›:› (λ F . ⦇F,y,y,y⦈)
      ― ‹three place ‹(z,z,z)›:› (λ F . ⦇F,z,z,z⦈)
    ― ‹‹x y z››
      ― ‹three place ‹(x,…)›:› (λ F . ⦇F,x,y,z⦈) (λ F . ⦇F,x,z,y⦈)
      ― ‹three place ‹(y,…)›:› (λ F . ⦇F,y,x,z⦈) (λ F . ⦇F,y,z,x⦈)
      ― ‹three place ‹(z,…)›:› (λ F . ⦇F,z,x,y⦈) (λ F . ⦇F,z,y,x⦈))"
  unfolding IsProperInXYZ_def
  by (auto simp: meta_defs meta_aux)    

method show_proper = (fast intro: IsProper_intros)

subsection‹Validity Syntax›
text‹\label{TAO_Semantics_Validity}›

(* disable list syntax [] to replace it with truth evaluation *)
(*<*) no_syntax "_list" :: "args ⇒ 'a list" ("[(_)]") (*>*) 
(*<*) no_syntax "__listcompr" :: "args ⇒ 'a list" ("[(_)]") (*>*) 

abbreviation validity_in :: "𝗈⇒i⇒bool" ("[_ in _]" [1]) where
  "validity_in ≡ λ φ v . v ⊨ φ"
definition actual_validity :: "𝗈⇒bool" ("[_]" [1]) where
  "actual_validity ≡ λ φ . dw ⊨ φ"
definition necessary_validity :: "𝗈⇒bool" ("□[_]" [1]) where
  "necessary_validity ≡ λ φ . ∀ v . (v ⊨ φ)"

(*<*)
end
(*>*)