# 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)
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⇒𝗈"
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⇒𝗈"
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
(*>*)