Prehistoric Graph in Modal Derivations and Self-Referentiality |
| |
Authors: | Junhua Yu |
| |
Affiliation: | 1. Doctoral Program in Computer Science, The Graduate Center, The City University of New York, New York, USA
|
| |
Abstract: | By terms-allowed-in-formulas capacity, Artemov’s Logic of Proofs LP Artemov includes self-referential formulas of the form t:?(t) that play a crucial role in the realization of modal logic S4 in LP, and in the Brouwer–Heyting–Kolmogorov semantics of intuitionistic logic via LP. In an earlier work appeared in the Proceedings of CSR 2010 the author defined prehistoric loop in a sequent calculus of S4, and verified its necessity to self-referentiality in S4?LP realization. In this extended version we generalize results there to T and K4, two modal logics smaller than S4 that yet call for self-referentiality in their realizations into corresponding justification logics JT and J4. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|