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) | 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 |