PRL Seminars
Online Demonstration of Syntactic Reflection. Realizing an Argument about Syntax (Tarski).
Eli Barzilay
March 3, 2003
Abstract
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.