(*<*)
theory TAO_8_Definitions
imports TAO_7_Axioms
begin
(*>*)

section‹Definitions›
text‹\label{TAO_Definitions}›

subsection‹Property Negations›

consts propnot :: "'a→'a" (‹_^-› [90] 90)
overloading propnot₀ ≡ "propnot :: Π₀→Π₀"
            propnot₁ ≡ "propnot :: Π₁→Π₁"
            propnot₂ ≡ "propnot :: Π₂→Π₂"
            propnot₃ ≡ "propnot :: Π₃→Π₃"
begin
  definition propnot₀ :: "Π₀→Π₀" where
    "propnot₀ ≡ λ p . \<lambda>⁰ (\<not>p)"
  definition propnot₁ where
    "propnot₁ ≡ λ F . \<lambda> x . \<not>(F, x^P)"
  definition propnot₂ where
    "propnot₂ ≡ λ F . \<lambda>² (λ x y . \<not>(F, x^P, y^P))"
  definition propnot₃ where
    "propnot₃ ≡ λ F . \<lambda>³ (λ x y z . \<not>(F, x^P, y^P, z^P))"
end

named_theorems propnot_defs
declare propnot₀_def[propnot_defs] propnot₁_def[propnot_defs]
        propnot₂_def[propnot_defs] propnot₃_def[propnot_defs]

subsection‹Noncontingent and Contingent Relations›

consts Necessary :: "'a→o"
overloading Necessary₀ ≡ "Necessary :: Π₀→o"
            Necessary₁ ≡ "Necessary :: Π₁→o"
            Necessary₂ ≡ "Necessary :: Π₂→o"
            Necessary₃ ≡ "Necessary :: Π₃→o"
begin
  definition Necessary₀ where
    "Necessary₀ ≡ λ p . \<box>p"
  definition Necessary₁ :: "Π₁→o" where
    "Necessary₁ ≡ λ F . \<box>(\<forall> x . (F,x^P))"
  definition Necessary₂ where
    "Necessary₂ ≡ λ F . \<box>(\<forall> x y . (F,x^P,y^P))"
  definition Necessary₃ where
    "Necessary₃ ≡ λ F . \<box>(\<forall> x y z . (F,x^P,y^P,z^P))"
end

named_theorems Necessary_defs
declare Necessary₀_def[Necessary_defs] Necessary₁_def[Necessary_defs]
        Necessary₂_def[Necessary_defs] Necessary₃_def[Necessary_defs]

consts Impossible :: "'a→o"
overloading Impossible₀ ≡ "Impossible :: Π₀→o"
            Impossible₁ ≡ "Impossible :: Π₁→o"
            Impossible₂ ≡ "Impossible :: Π₂→o"
            Impossible₃ ≡ "Impossible :: Π₃→o"
begin
  definition Impossible₀ where
    "Impossible₀ ≡ λ p . \<box>\<not>p"
  definition Impossible₁ where
    "Impossible₁ ≡ λ F . \<box>(\<forall> x. \<not>(F,x^P))"
  definition Impossible₂ where
    "Impossible₂ ≡ λ F . \<box>(\<forall> x y. \<not>(F,x^P,y^P))"
  definition Impossible₃ where
    "Impossible₃ ≡ λ F . \<box>(\<forall> x y z. \<not>(F,x^P,y^P,z^P))"
end

named_theorems Impossible_defs
declare Impossible₀_def[Impossible_defs] Impossible₁_def[Impossible_defs]
        Impossible₂_def[Impossible_defs] Impossible₃_def[Impossible_defs]

definition NonContingent where
  "NonContingent ≡ λ F . (Necessary F) \<or> (Impossible F)"
definition Contingent where
  "Contingent ≡ λ F . \<not>(Necessary F \<or> Impossible F)"

definition ContingentlyTrue :: "o→o" where
  "ContingentlyTrue ≡ λ p . p & \<diamond>\<not>p"
definition ContingentlyFalse :: "o→o" where
  "ContingentlyFalse ≡ λ p . \<not>p & \<diamond>p"

definition WeaklyContingent where
  "WeaklyContingent ≡ λ F . Contingent F & (\<forall> x. \<diamond>(F,x^P) \<rightarrow> \<box>(F,x^P))"

subsection‹Null and Universal Objects›

definition Null :: "κ→o" where
  "Null ≡ λ x . (A!,x) & \<not>(\<exists> F . {x, F})"
definition Universal :: "κ→o" where
  "Universal ≡ λ x . (A!,x) & (\<forall> F . {x, F})"

definition NullObject :: "κ" (‹a_\∅›) where
  "NullObject ≡ (\<iota>x . Null (x^P))"
definition UniversalObject :: "κ" (‹a_V›) where
  "UniversalObject ≡ (\<iota>x . Universal (x^P))"

subsection‹Propositional Properties›

definition Propositional where
  "Propositional F ≡ \<exists> p . F = (\<lambda> x . p)"

subsection‹Indiscriminate Properties›

definition Indiscriminate :: "Π₁→o" where
  "Indiscriminate ≡ λ F . \<box>((\<exists> x . (F,x^P)) \<rightarrow> (\<forall> x . (F,x^P)))"

subsection‹Miscellaneous›

definition not_identical_E :: "κ→κ→o" (infixl ‹\≠_E› 63)
  where "not_identical_E ≡ λ x y . ((\<lambda>² (λ x y . x^P =_E y^P))^-, x, y)"

(*<*)
end
(*>*)