|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
Uniform provability realization of intuitionistic logic, modality and λ-termsстатья
Информация о цитировании статьи получена из
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 28 мая 2015 г.
- Автор: Artemov S.N.
- Журнал: Electronic Notes in Theoretical Computer Science
- Том: 23
- Номер: 1
- Год издания: 1999
- Издательство: Elsevier BV
- Местоположение издательства: Netherlands
- Первая страница: 3
- Последняя страница: 12
- DOI: 10.1016/S1571-0661(04)00100-8
- Аннотация: The intended meaning of intuitionistic logic is explained by the Brouwer-Heyting-Kolmogorov (BHK) provability semantics which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs. The problem of finding an adequate formalization of the provability semantics and establishing the completeness of the intuitionistic logic Int was first raised by Gödel in 1933. This question turned out to be a part of the more general problem of the intended realization for Gödel’s modal logic of provability S4 which was open since 1933. In this tutorial talk we present a provability realization of Int and S4 that solves both of these problems. We describe the logic of explicit provability (LP) with the atoms "t is a proof of F" and establish that every theorem of S4 admits a reading in LP as the statement about operations on proofs. Moreover, both S4 and Int are shown to be complete with respect to this realization. In addition, LP subsumes the λ-calculus, modal λ-calculus, combinatory logic and provides a uniform provability realization of modality and λ-terms. © 1999 Published by Elsevier B.V.
- Добавил в систему: Артемов Сергей Николаевич