The Internalized Disjunction Property for Intuitionistic Justification Logic

Marti, Michel; Studer, Thomas (2018). The Internalized Disjunction Property for Intuitionistic Justification Logic. In: Bezhanishvili, Guram; D'Agostino, Giovanna; Metcalfe, George; Studer, Thomas (eds.) Advances in Modal Logic 12 (pp. 511-529). College Publications

Text aiml18_revised.pdf - Accepted Version Restricted to registered users only Available under License Publisher holds Copyright. Download (386kB)

In intuitionistic justification logic, evidence terms represent intuitionistic proofs, thatis a formula r:A means r is an intuitionistic proof of A. A natural principle in thiscontext is the internalized disjunction property (IDP), which is: for each term r thereexists a term s such that r:(A or B) implies s:A or s:B.We introduce a light extension of iJT4, in which IDP is valid. Our proof relies ona model construction that enforces sharp evidence relations and a tight connectionbetween syntax and semantics. This makes it possible to switch between proofs andmodels, which will be the key to proving IDP.

Interest & Impact

Downloads

2 since deposited on 15 May 2019
0 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item