zbMATH — the first resource for mathematics

An arithmetical interpretation of verification and intuitionistic knowledge. (English) Zbl 06751247
Artemov, Sergei (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4–7, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9537, 317-330 (2016).
Summary: Intuitionistic epistemic logic introduces an epistemic operator, which reflects the intended BHK semantics of intuitionism, to intuitionistic logic. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the logic of proofs and its arithmetical semantics. We show here that this interpretation can be extended to the notion of verification upon which intuitionistic knowledge is based, thereby providing the systems of intuitionistic epistemic logic extended by an epistemic operator based on verification with an arithmetical semantics too.
For the entire collection see [Zbl 1364.03006].

03B70 Logic in computer science
Full Text: DOI arXiv
[1] Artemov, S.: Operational modal logic. Technical report. MSI 95–29, Cornell University (1995)
[2] Artemov, S.: Explicit provability and constructive semantics. Bull. Symbolic Logic 7(1), 1–36 (2001) · Zbl 0980.03059
[3] Artemov, S.: Justified common knowledge. Theor. Comput. Sci. 357, 4–22 (2006) · Zbl 1094.03005
[4] Artemov, S.: The logic of justification. Rev. Symbolic Logic 1(4), 477–513 (2008) · Zbl 1205.03027
[5] Artemov, S., Protopopescu, T.: Intuitionistic epistemic logic. Technical report, December 2014. http://arxiv.org/abs/1406.1582 · Zbl 1408.03004
[6] Boolos, G.: The Logic of Provability. Cambridge University Press, Cambridge (1993) · Zbl 0891.03004
[7] Brezhnev, V.N., Kuznets, R.: Making knowledge explicit: how hard it is. Theor. Comput. Sci. 357(1), 23–34 (2006). http://dx.doi.org/10.1016/j.tcs.2006.03.010 · Zbl 1094.03006
[8] Chagrov, A., Zakharyaschev, M.: Modal Logic. Clarendon Press, Oxford (1997)
[9] Feferman, S.: Arithmetization of metamathematics in a general setting. Fundam. Math. 49(1), 35–92 (1960) · Zbl 0095.24301
[10] Fitting, M.: The logic of proofs, semantically. Ann. Pure Appl. Logic 132, 1–25 (2005) · Zbl 1066.03059
[11] Gödel, K.: An interpretation of the intuitionistic propositional calculus. In: Feferman, S., Dawson, J.W., Goldfarb, W., Parsons, C., Solovay, R.M. (eds.) Collected Works, vol. 1, pp. 301–303. Oxford University Press, Oxford (1933)
[12] McKinsey, J.C.C., Tarski, A.: Some theorems about the sentential calculi of lewis and heyting. J. Symbolic Logic 13(1), 1–15 (1948). http://www.jstor.org/stable/2268135 · Zbl 0037.29409
[13] Mints, G.: A Short Introduction to Intuitionistic Logic. Springer, Berlin (2000) · Zbl 1036.03003
[14] Protopopescu, T.: Intuitionistic epistemology and modal logics of verification. In: van der Hoek, W., Holliday, W.H., Wang, W. (eds.) LORI 2015. LNCS, vol. 9394, pp. 295–307. Springer, Heidelberg (2015) · Zbl 06521586
[15] Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (2000) · Zbl 0957.03053
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.