By terms-allowed-in-types capacity, the Logic of Proofs LP enjoys a system of advanced combinatory terms, while including types of the form t: Φ{t), which have self-referential meanings. This paper suggests a research on possible S4 measures of self-refer entiality introduced by this capacity. Specifically, we define "prehistoric phenomena" in G3s, a Gentzen-style formulation of modal logic S4. A special phenomenon, namely, "left prehistoric loop", is then shown to be necessary for self-referentiality in realizations of S4 theorems in LP.
展开▼
