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

[img] Text
aiml18_revised.pdf - Accepted Version
Restricted to registered users only
Available under License Publisher holds Copyright.

Download (386kB) | Request a copy

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.

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:

Marti, Michel and Studer, Thomas

Subjects:

000 Computer science, knowledge & systems
500 Science > 510 Mathematics

Publisher:

College Publications

Language:

English

Submitter:

Lukas Jaun

Date Deposited:

15 May 2019 18:26

Last Modified:

24 Oct 2019 07:34

BORIS DOI:

10.7892/boris.125734

URI:

https://boris.unibe.ch/id/eprint/125734

Actions (login required)

Edit item Edit item
Provide Feedback