Reflection is the ability of some entity to describe itself. In a logical context,
it is the ability of a logic to reason about itself. Reflection is, therefore, placed at
the core of meta-mathematics, making it an important part of formal reasoning;
where it revolves mainly around syntax and semantics — the main challenge is in
making the syntax of the logic become part of its semantic domain.
Given its importance, it is surprising that logical computer systems tend to
avoid the subject, or provide poor tools for reflective work. This is in sharp contrast
to the area of programming languages, where reflection is well researched and
used in a variety of ways where it plays an central role. One factor in making
reflection inaccessible in logical systems is the relative diculty that is immediately
encountered when formalizing syntax: dealing with formal syntax means dealing
with structures that involve bindings, and in a logical context it seems natural
to use the same formal tools to describe syntax — often limiting the usability of
such formalizations to specific theories and toy examples. G¨odel numbers are an
example for a reflective formalism that serves its purpose, yet is impractical as a
basis for syntactical reasoning in applied systems.
In programming languages, there is a simple yet elegant strategy for implementing
reflection: instead of making a system that describes itself, the system is
made available to itself. We name this direct reflection, where the representation of
language features via its semantics is actually part of the semantics itself — unlike
the usual practice in formal systems of employing indirect reflection. The advantages
of this approach is the fact that both the system and its reflected counterpart
are inherently identical, making for a lightweight implementation.
In this work we develop the formal background and the practical capabilities
of an applied system, namely Nuprl, that are needed to support direct reflection
of its own syntax. Achieving this is a major milestone on the road for a fully
reflected logical system. As we shall demonstrate, our results enable dealing with
syntactical meta-mathematical content.