Skip to main content
PRL Project

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

by Regina Barzilay
2002-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.

Associated Files:

reflection.ps; tarski.ps; reflection.thy; tarski.thy