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-referentiality 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. © 2010 Springer-Verlag.
CITATION STYLE
Yu, J. (2010). Prehistoric phenomena and self-referentiality. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6072 LNCS, pp. 384–396). https://doi.org/10.1007/978-3-642-13182-0_38
Mendeley helps you to discover research relevant for your work.