Prehistoric Phenomena and Self-referentiality in Realization Procedure
Junhua Yu

Abstract:
With terms allowed in types, the Logic of Proofs (LP) has its
polynomials as advanced combinatory terms. As a result, types of the
form t: ϕ(t), which have self-referential meanings, are also
included. If we can fix the class of non-self-referential-realizable
S4-theorems, then we may find some S4 (and hence, intuitionistic)
measure of self-referentiality introduced by the terms-in-types
feature. In this paper, we define and study “prehistoric phenomena” 
in G3s, a Gentzen-style formulation of S4. A special prehistoric
phenomenon, i.e., the left-prehistoric-loop, is then shown to be
necessary for self-referentiality in S4-LP realization.