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