A Note on the Use of Sum in the Logic of Proofs

Kuznets, Roman (2009). A Note on the Use of Sum in the Logic of Proofs. In: Drossos, Costas; , ; , ; Tsinakis, Constantine (eds.) Proceedings of the 7th Panhellenic Logic Symposium (pp. 99-103). Patras University Press

Full text not available from this repository. (Request a copy)

The Logic of Proofs~LP, introduced by Artemov, encodes the same reasoning as the modal logic~S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application~$\cdot$, positive introspection~!, and sum~+) are sufficient to mimic provability concealed in S4~modality. While the first two operations go back to G{\"o}del, the exact role of~+ remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP.

Item Type: Conference or Workshop Item (Paper)
Division/Institute: 08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG)
08 Faculty of Science > Institute of Computer Science (INF)
UniBE Contributor: Kuznets, Roman
Publisher: Patras University Press
Language: English
Submitter: Factscience Import
Date Deposited: 04 Oct 2013 15:23
Last Modified: 08 Sep 2015 16:16
URI: http://boris.unibe.ch/id/eprint/37194 (FactScience: 207169)

Actions (login required)

Edit item Edit item
Provide Feedback