Theory TAO_4_BasicDefinitions

theory TAO_4_BasicDefinitions
imports TAO_3_Quantifiable
(*<*)
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
(*>*)