Theory TAO_8_Definitions

theory TAO_8_Definitions
imports TAO_7_Axioms


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"
  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)"

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𝗈"
  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)"

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𝗈"
  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)"

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))"


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