Theory TAO_8_Definitions

theory TAO_8_Definitions
imports TAO_7_Axioms
(*<*)
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 propnot0  "propnot :: Π0⇒Π0"
            propnot1  "propnot :: Π1⇒Π1"
            propnot2  "propnot :: Π2⇒Π2"
            propnot3  "propnot :: Π3⇒Π3"
begin
  definition propnot0 :: 0⇒Π0" where
    "propnot0 ≡ λ p . λ0 (¬p)"
  definition propnot1 where
    "propnot1 ≡ λ F . λ x . ¬⦇F, xP⦈"
  definition propnot2 where
    "propnot2 ≡ λ F . λ2 (λ x y . ¬⦇F, xP, yP⦈)"
  definition propnot3 where
    "propnot3 ≡ λ F . λ3 (λ x y z . ¬⦇F, xP, yP, zP⦈)"
end

named_theorems propnot_defs
declare propnot0_def[propnot_defs] propnot1_def[propnot_defs]
        propnot2_def[propnot_defs] propnot3_def[propnot_defs]

subsection‹Noncontingent and Contingent Relations›

consts Necessary :: "'a⇒𝗈"
overloading Necessary0  "Necessary :: Π0⇒𝗈"
            Necessary1  "Necessary :: Π1⇒𝗈"
            Necessary2  "Necessary :: Π2⇒𝗈"
            Necessary3  "Necessary :: Π3⇒𝗈"
begin
  definition Necessary0 where
    "Necessary0 ≡ λ p . p"
  definition Necessary1 :: 1⇒𝗈" where
    "Necessary1 ≡ λ F . ( x . ⦇F,xP⦈)"
  definition Necessary2 where
    "Necessary2 ≡ λ F . ( x y . ⦇F,xP,yP⦈)"
  definition Necessary3 where
    "Necessary3 ≡ λ F . ( x y z . ⦇F,xP,yP,zP⦈)"
end

named_theorems Necessary_defs
declare Necessary0_def[Necessary_defs] Necessary1_def[Necessary_defs]
        Necessary2_def[Necessary_defs] Necessary3_def[Necessary_defs]

consts Impossible :: "'a⇒𝗈"
overloading Impossible0  "Impossible :: Π0⇒𝗈"
            Impossible1  "Impossible :: Π1⇒𝗈"
            Impossible2  "Impossible :: Π2⇒𝗈"
            Impossible3  "Impossible :: Π3⇒𝗈"
begin
  definition Impossible0 where
    "Impossible0 ≡ λ p . ¬p"
  definition Impossible1 where
    "Impossible1 ≡ λ F . ( x. ¬⦇F,xP⦈)"
  definition Impossible2 where
    "Impossible2 ≡ λ F . ( x y. ¬⦇F,xP,yP⦈)"
  definition Impossible3 where
    "Impossible3 ≡ λ F . ( x y z. ¬⦇F,xP,yP,zP⦈)"
end

named_theorems Impossible_defs
declare Impossible0_def[Impossible_defs] Impossible1_def[Impossible_defs]
        Impossible2_def[Impossible_defs] Impossible3_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,xP ⦇F,xP⦈)"

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 (xP))"
definition UniversalObject :: "κ" ("aV") where
  "UniversalObject ≡ (ιx . Universal (xP))"

subsection‹Propositional Properties›

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

subsection‹Indiscriminate Properties›

definition Indiscriminate :: 1⇒𝗈" where
  "Indiscriminate ≡ λ F . (( x . ⦇F,xP⦈)  ( x . ⦇F,xP⦈))"

subsection‹Miscellaneous›

definition not_identicalE :: "κ⇒κ⇒𝗈" (infixl "E" 63)
  where "not_identicalE ≡ λ x y . ⦇(λ2 (λ x y . xP =E yP))-, x, y⦈"

(*<*)
end
(*>*)