PRL Seminars 1998-99

We will examine the difference between the explicit reflection of proof that Artemov discussed last week and the implicit reflection of provability that is discussed in the 1990 LICS paper on reflection in Nuprl.

We will show an example of how each rule could be used, discuss implications for implementation issues and discuss the proof theoretic power of the two different rules as well as the inconsistency of the naive rule.

It will be fun.