Intuitionistic modal logic made explicit. Marti, M. & Studer, T. IfCoLog Journal of Logics and their Applications, 3(5):877-901, 2016. Paper abstract bibtex The logic of proofs of Heyting arithmetic includes explicit justifications for all admissible rules of intuitionistic logic in order to satisfy completeness with respect to provability semantics. We study the justification logic iJT4, which does not have these additional justification terms. We establish that iJT4 is complete with respect to modular models, which provide a Kripke-style semantics, and that there is a realization of intuitionistic S4 into iJT4. Hence iJT4 can be seen as an explicit version of intuitionistic S4.
@article {mast16,
title = {Intuitionistic modal logic made explicit},
year = {2016},
journal = {IfCoLog Journal of Logics and their Applications},
volume = {3},
number = {5},
pages = {877-901},
url = {2016/mast16.pdf},
author = {Michel Marti and Thomas Studer},
abstract = {The logic of proofs of Heyting arithmetic includes explicit
justifications for all admissible rules of intuitionistic logic in order to
satisfy completeness with respect to provability semantics. We study the
justification logic iJT4, which does not have these additional justification
terms. We establish that iJT4 is complete with respect to modular models,
which provide a Kripke-style semantics, and that there is a realization
of intuitionistic S4 into iJT4. Hence iJT4 can be seen as an explicit
version of intuitionistic S4.}
}
Downloads: 0
{"_id":"wR3ny3uvfELKXMbfE","bibbaseid":"marti-studer-intuitionisticmodallogicmadeexplicit-2016","authorIDs":[],"author_short":["Marti, M.","Studer, T."],"bibdata":{"bibtype":"article","type":"article","title":"Intuitionistic modal logic made explicit","year":"2016","journal":"IfCoLog Journal of Logics and their Applications","volume":"3","number":"5","pages":"877-901","url":"2016/mast16.pdf","author":[{"firstnames":["Michel"],"propositions":[],"lastnames":["Marti"],"suffixes":[]},{"firstnames":["Thomas"],"propositions":[],"lastnames":["Studer"],"suffixes":[]}],"abstract":"The logic of proofs of Heyting arithmetic includes explicit justifications for all admissible rules of intuitionistic logic in order to satisfy completeness with respect to provability semantics. We study the justification logic iJT4, which does not have these additional justification terms. We establish that iJT4 is complete with respect to modular models, which provide a Kripke-style semantics, and that there is a realization of intuitionistic S4 into iJT4. Hence iJT4 can be seen as an explicit version of intuitionistic S4.","bibtex":"@article {mast16,\n\ttitle = {Intuitionistic modal logic made explicit},\n\tyear = {2016},\n\tjournal = {IfCoLog Journal of Logics and their Applications},\n\tvolume = {3},\n\tnumber = {5},\n\tpages = {877-901},\n\turl = {2016/mast16.pdf},\n\tauthor = {Michel Marti and Thomas Studer},\n\tabstract = {The logic of proofs of Heyting arithmetic includes explicit\n\tjustifications for all admissible rules of intuitionistic logic in order to\n\tsatisfy completeness with respect to provability semantics. We study the\n\tjustification logic iJT4, which does not have these additional justification\n\tterms. We establish that iJT4 is complete with respect to modular models,\n\twhich provide a Kripke-style semantics, and that there is a realization\n\tof intuitionistic S4 into iJT4. Hence iJT4 can be seen as an explicit\n\tversion of intuitionistic S4.}\n}\n\n\n\n","author_short":["Marti, M.","Studer, T."],"key":"mast16","id":"mast16","bibbaseid":"marti-studer-intuitionisticmodallogicmadeexplicit-2016","role":"author","urls":{"Paper":"http://home.inf.unibe.ch/~brambi/2016/mast16.pdf"},"downloads":0},"bibtype":"article","biburl":"http://home.inf.unibe.ch/~brambi/ltg.bib","creationDate":"2020-02-26T09:06:58.993Z","downloads":0,"keywords":[],"search_terms":["intuitionistic","modal","logic","made","explicit","marti","studer"],"title":"Intuitionistic modal logic made explicit","year":2016,"dataSources":["jFQMeatnEb8qn3qdH"]}