Skip to main content
PRL Project

Online Demonstration of Syntactic Reflection. Realizing an Argument about Syntax (Tarski).

by Regina Barzilay


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.thy; tarski.thy