Practical Reflection for Nuprl

These are some materials from my reflection & quotation work in Nuprl:

  • The Reflection theory, as rendered by Nuprl. (Note that the “Fiat” proofs should be considered as axioms.)
  • My example of using it: a formalization of the Tarski result about truth not being reflected, as sketched by Stuart Allen. Formalized as a Nuprl theory.
  • The Tarski proof is also available in HTML format made by Stuart's Nuprl magic tricks, with either my notations or Stuart's.
  • My thesis and talk are also available.
(Papers are found on the previous page.)