Rn and Gn Logics

This paper proposes a simple, set-theoretic framework providing expressive typing, higher-order functions and initial models at the same time. Building upon Russell's ramified theory of types, we develop the theory of Rn-logics, which are axiomatisable by an order-sorted equational Horn logic with a membership predicate, and of Gn-logics, that provide in addition partial functions. The latter are therefore more adapted to the use in the program specification domain, while sharing interesting properties, like existence of an initial model, with Rn-logics. Operational semantics of Rn-/Gn-logics presentations is obtained through order-sorted conditional rewriting.