Online Demonstration of Syntactic Reflection. Realizing an Argument about Syntax (Tarski).
Eli has finished a formalization of the Tarski undefinability-of-truth result using his devices for reflecting syntax. He will review the informal proof, demonstrate on a running Nuprl system his formalization (most effectively exploiting color as a quotation marking device), and review the as-yet-unproved rules that were added to achieve it.
Associated Files:reflection.ps; tarski.ps; reflection.thy; tarski.thy