Theory TAO_8_Definitions

(*<*)
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⇩0 ≡ "propnot :: Π⇩0⇒Π⇩0"
            propnot⇩1 ≡ "propnot :: Π⇩1⇒Π⇩1"
            propnot⇩2 ≡ "propnot :: Π⇩2⇒Π⇩2"
            propnot⇩3 ≡ "propnot :: Π⇩3⇒Π⇩3"
begin
  definition propnot⇩0 :: "Π⇩0⇒Π⇩0" where
    "propnot⇩0 ≡ λ p . ❙λ⇧0 (❙¬p)"
  definition propnot⇩1 where
    "propnot⇩1 ≡ λ F . ❙λ x . ❙¬⦇F, x⇧P⦈"
  definition propnot⇩2 where
    "propnot⇩2 ≡ λ F . ❙λ⇧2 (λ x y . ❙¬⦇F, x⇧P, y⇧P⦈)"
  definition propnot⇩3 where
    "propnot⇩3 ≡ λ F . ❙λ⇧3 (λ x y z . ❙¬⦇F, x⇧P, y⇧P, z⇧P⦈)"
end

named_theorems propnot_defs
declare propnot⇩0_def[propnot_defs] propnot⇩1_def[propnot_defs]
        propnot⇩2_def[propnot_defs] propnot⇩3_def[propnot_defs]

subsection‹Noncontingent and Contingent Relations›

consts Necessary :: "'a⇒𝗈"
overloading Necessary⇩0 ≡ "Necessary :: Π⇩0⇒𝗈"
            Necessary⇩1 ≡ "Necessary :: Π⇩1⇒𝗈"
            Necessary⇩2 ≡ "Necessary :: Π⇩2⇒𝗈"
            Necessary⇩3 ≡ "Necessary :: Π⇩3⇒𝗈"
begin
  definition Necessary⇩0 where
    "Necessary⇩0 ≡ λ p . ❙□p"
  definition Necessary⇩1 :: "Π⇩1⇒𝗈" where
    "Necessary⇩1 ≡ λ F . ❙□(❙∀ x . ⦇F,x⇧P⦈)"
  definition Necessary⇩2 where
    "Necessary⇩2 ≡ λ F . ❙□(❙∀ x y . ⦇F,x⇧P,y⇧P⦈)"
  definition Necessary⇩3 where
    "Necessary⇩3 ≡ λ F . ❙□(❙∀ x y z . ⦇F,x⇧P,y⇧P,z⇧P⦈)"
end

named_theorems Necessary_defs
declare Necessary⇩0_def[Necessary_defs] Necessary⇩1_def[Necessary_defs]
        Necessary⇩2_def[Necessary_defs] Necessary⇩3_def[Necessary_defs]

consts Impossible :: "'a⇒𝗈"
overloading Impossible⇩0 ≡ "Impossible :: Π⇩0⇒𝗈"
            Impossible⇩1 ≡ "Impossible :: Π⇩1⇒𝗈"
            Impossible⇩2 ≡ "Impossible :: Π⇩2⇒𝗈"
            Impossible⇩3 ≡ "Impossible :: Π⇩3⇒𝗈"
begin
  definition Impossible⇩0 where
    "Impossible⇩0 ≡ λ p . ❙□❙¬p"
  definition Impossible⇩1 where
    "Impossible⇩1 ≡ λ F . ❙□(❙∀ x. ❙¬⦇F,x⇧P⦈)"
  definition Impossible⇩2 where
    "Impossible⇩2 ≡ λ F . ❙□(❙∀ x y. ❙¬⦇F,x⇧P,y⇧P⦈)"
  definition Impossible⇩3 where
    "Impossible⇩3 ≡ λ F . ❙□(❙∀ x y z. ❙¬⦇F,x⇧P,y⇧P,z⇧P⦈)"
end

named_theorems Impossible_defs
declare Impossible⇩0_def[Impossible_defs] Impossible⇩1_def[Impossible_defs]
        Impossible⇩2_def[Impossible_defs] Impossible⇩3_def[Impossible_defs]

definition NonContingent where
  "NonContingent ≡ λ F . (Necessary F) ❙∨ (Impossible F)"
definition Contingent where
  "Contingent ≡ λ F .  ❙¬(Necessary F ❙∨ Impossible F)"

definition ContingentlyTrue :: "𝗈⇒𝗈" where
  "ContingentlyTrue ≡ λ p . p ❙& ❙◇❙¬p"
definition ContingentlyFalse :: "𝗈⇒𝗈" where
  "ContingentlyFalse ≡ λ p . ❙¬p ❙& ❙◇p"

definition WeaklyContingent where
  "WeaklyContingent ≡ λ F . Contingent F ❙& (❙∀ x. ❙◇⦇F,x⇧P⦈ ❙→ ❙□⦇F,x⇧P⦈)"

subsection‹Null and Universal Objects›

definition Null :: "κ⇒𝗈" where
  "Null ≡ λ x . ⦇A!,x⦈ ❙& ❙¬(❙∃ F . ⦃x, F⦄)"
definition Universal :: "κ⇒𝗈" where
  "Universal ≡ λ x . ⦇A!,x⦈ ❙& (❙∀ F . ⦃x, F⦄)"

definition NullObject :: "κ" ("❙a⇩∅") where
  "NullObject ≡ (❙ιx . Null (x⇧P))"
definition UniversalObject :: "κ" ("❙a⇩V") where
  "UniversalObject ≡ (❙ιx . Universal (x⇧P))"

subsection‹Propositional Properties›

definition Propositional where
  "Propositional F ≡ ❙∃  p . F ❙= (❙λ x . p)"

subsection‹Indiscriminate Properties›

definition Indiscriminate :: "Π⇩1⇒𝗈" where
  "Indiscriminate ≡ λ F . ❙□((❙∃ x . ⦇F,x⇧P⦈) ❙→ (❙∀ x . ⦇F,x⇧P⦈))"

subsection‹Miscellaneous›

definition not_identical⇩E :: "κ⇒κ⇒𝗈" (infixl "❙≠⇩E" 63)
  where "not_identical⇩E ≡ λ x y . ⦇(❙λ⇧2 (λ x y . x⇧P ❙=⇩E y⇧P))⇧-, x, y⦈"

(*<*)
end
(*>*)