MetaPRL Logical framework

The framework is modular: theories are constructed as objects, and logics are defined incrementally by adding properties to existing modules. The primitives of the framework are a term language, and a weak higher-order Horn logic for defining relations between the terms. Modules contain these constructs: