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!,x⇧P⦈"
definition Abstract :: "Π⇩1" (‹A!›) where "Abstract ≡ ❙λx. ❙¬❙◇⦇E!,x⇧P⦈"

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

definition basic_identity⇩E::"Π⇩2" where
  "basic_identity⇩E ≡ ❙λ⇧2 (λ x y . ⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈
                         ❙& ❙□(❙∀ F. ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈))"

definition basic_identity⇩E_infix::"κ⇒κ⇒𝗈" (infixl ‹❙=⇩E› 63) where
  "x ❙=⇩E y ≡ ⦇basic_identity⇩E, 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_identity⇩1 (infixl ‹❙=⇩1› 63) where
  "basic_identity⇩1 ≡ λ F G . ❙□(❙∀ x. ⦃x⇧P,F⦄ ❙≡ ⦃x⇧P,G⦄)"

definition basic_identity⇩2 :: "Π⇩2⇒Π⇩2⇒𝗈" (infixl ‹❙=⇩2› 63) where
  "basic_identity⇩2 ≡ λ F G .  ❙∀ x. ((❙λy. ⦇F,x⇧P,y⇧P⦈) ❙=⇩1 (❙λy. ⦇G,x⇧P,y⇧P⦈))
                                 ❙& ((❙λy. ⦇F,y⇧P,x⇧P⦈) ❙=⇩1 (❙λy. ⦇G,y⇧P,x⇧P⦈))"

definition basic_identity⇩3::"Π⇩3⇒Π⇩3⇒𝗈" (infixl ‹❙=⇩3› 63) where
  "basic_identity⇩3 ≡ λ F G . ❙∀ x y. (❙λz. ⦇F,z⇧P,x⇧P,y⇧P⦈) ❙=⇩1 (❙λz. ⦇G,z⇧P,x⇧P,y⇧P⦈)
                                  ❙& (❙λz. ⦇F,x⇧P,z⇧P,y⇧P⦈) ❙=⇩1 (❙λz. ⦇G,x⇧P,z⇧P,y⇧P⦈)
                                  ❙& (❙λz. ⦇F,x⇧P,y⇧P,z⇧P⦈) ❙=⇩1 (❙λz. ⦇G,x⇧P,y⇧P,z⇧P⦈)"

definition basic_identity⇩0::"𝗈⇒𝗈⇒𝗈" (infixl ‹❙=⇩0› 63) where
  "basic_identity⇩0 ≡ λ F G . (❙λy. F) ❙=⇩1 (❙λy. G)"

(*<*)
end
(*>*)