Theory TAO_4_BasicDefinitions

(*<*)
theory TAO_4_BasicDefinitions
imports TAO_3_Quantifiable
begin
(*>*)

section‹Basic Definitions›
text‹\label{TAO_BasicDefinitions}›

subsection‹Derived Connectives›
text‹\label{TAO_BasicDefinitions_DerivedConnectives}›

definition conj::"𝗈𝗈𝗈" (infixl "&" 53) where
  "conj  λ x y . ¬(x  ¬y)"
definition disj::"𝗈𝗈𝗈" (infixl "" 52) where
  "disj  λ x y . ¬x  y"
definition equiv::"𝗈𝗈𝗈" (infixl "" 51) where
  "equiv  λ x y . (x  y) & (y  x)"
definition diamond::"𝗈𝗈" ("_" [62] 63) where
  "diamond  λ φ . ¬¬φ"
definition (in quantifiable) exists :: "('a𝗈)𝗈" (binder "" [8] 9) where
    "exists  λ φ . ¬( x . ¬φ x)"

named_theorems conn_defs
declare diamond_def[conn_defs] conj_def[conn_defs]
        disj_def[conn_defs] equiv_def[conn_defs]
        exists_def[conn_defs]

subsection‹Abstract and Ordinary Objects›
text‹\label{TAO_BasicDefinitions_AbstractOrdinary}›

definition Ordinary :: "Π1" ("O!") where "Ordinary  λx. E!,xP"
definition Abstract :: "Π1" ("A!") where "Abstract  λx. ¬E!,xP"

subsection‹Identity Definitions›
text‹\label{TAO_BasicDefinitions_Identity}›

definition basic_identityE::"Π2" where
  "basic_identityE  λ2 (λ x y . O!,xP & O!,yP
                         & ( F. F,xP  F,yP))"

definition basic_identityE_infix::"κκ𝗈" (infixl "=E" 63) where
  "x =E y  basic_identityE, x, y"

definition basic_identityκ (infixl "=κ" 63) where
  "basic_identityκ  λ x y . (x =E y)  A!,x & A!,y
                             & ( F. x,F  y,F)"

definition basic_identity1 (infixl "=1" 63) where
  "basic_identity1  λ F G . ( x. xP,F  xP,G)"

definition basic_identity2 :: "Π2Π2𝗈" (infixl "=2" 63) where
  "basic_identity2  λ F G .   x. ((λy. F,xP,yP) =1 (λy. G,xP,yP))
                                 & ((λy. F,yP,xP) =1 (λy. G,yP,xP))"

definition basic_identity3::"Π3Π3𝗈" (infixl "=3" 63) where
  "basic_identity3  λ F G .  x y. (λz. F,zP,xP,yP) =1 (λz. G,zP,xP,yP)
                                  & (λz. F,xP,zP,yP) =1 (λz. G,xP,zP,yP)
                                  & (λz. F,xP,yP,zP) =1 (λz. G,xP,yP,zP)"

definition basic_identity0::"𝗈𝗈𝗈" (infixl "=0" 63) where
  "basic_identity0  λ F G . (λy. F) =1 (λy. G)"

(*<*)
end
(*>*)