KnowledgeBase » SEMINAR » ID = 287

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.