A semantics for equational hybrid propositional type theory

Abstract

The definition of identity in terms of other logical symbols is a recurrent issue in logic. In particular, in First-Order Logic (FOL) there is no way of defining the global relation of identity, while in standard Second-Order Logic (SOL) this definition is not only possible, but widely used. In this paper, the reverse question is posed and affirmatively answered: Can we define with only equality and abstraction the remaining logical symbols? Our present work is developed in the context of an equational hybrid logic (i.e. a modal logic with equations as propositional atoms enlarged with the hybrid expressions: nominals and the @ operator). Our logical base is propositional type theory. We take the propositional equality, abstraction, nominals, and @ operators as primitive symbols and we demonstrate that all of the remaining logical symbols can be defined, including propositional quantifiers and equational equality.