Theory BaseDefs

subsection‹Preliminaries: Further Basic Notions (Fig.~3 in \<^cite>‹"C85"›)›

theory BaseDefs imports HOML
begin  
text‹Positive properties.› 
consts posProp::"γ⇒σ" ("𝒫")

text‹Basic definitions for modal ontological argument.›
abbreviation a ("_❙⊑_") where "X❙⊑Y ≡ ❙∀⇧Ez.((X z) ❙→ (Y z))"
abbreviation b ("_⇛_") where "X⇛Y ≡ ❙□(X❙⊑Y)"
abbreviation c ("𝒫𝗈𝗌") where "𝒫𝗈𝗌 Z ≡ ❙∀X.((Z X) ❙→ (𝒫 X))"
abbreviation d ("_⨅_") where "X⨅𝒵 ≡ ❙□(❙∀⇧Eu.((X u) ❙↔ (❙∀Y.((𝒵 Y) ❙→ (Y u)))))"

text‹Definition of Godlike.›
definition G ("𝒢") where "𝒢 x ≡ ❙∀Y.((𝒫 Y) ❙→ (Y x))"

text‹Definitions of Essence and Necessary Existence.›
definition E ("ℰ") where "ℰ Y x ≡ (Y x) ❙∧ (❙∀Z.((Z x) ❙→ (Y⇛Z)))"
definition NE ("𝒩ℰ") where "𝒩ℰ x ≡ ❙∀Y.((ℰ Y x) ❙→ ❙□(❙∃⇧E Y))"
end