# * Semantics and Pragmatics of Reflected Proof *

## by Stuart F. Allen, Sergei Artemov, Robert L. Constable

1998-1999

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.