By terms-allowed-in-types capacity, the Logic of Proofs LP includes formulas of the form t : ϕ(t), which have self-referential meanings. In this paper, “prehistoric phenomena” in a Gentzen-style formulation of modal logic S4 are defined. A special phenomenon, i.e., “left prehistoric loop”, is then shown to be necessary for self-referentiality in S4-LP realization.