Title: Axiomatic and dual systems for constructive necessity, a formally verified equivalence
Abstract: We present a proof of the equivalence between two deductive systems for constructive necessity, namely an axiomatic characterisation inspired by Hakli and Negri's system of derivations from assumptions for modal logic , a Hilbert-style formalism designed to ensure the validity of the deduction theorem, and the judgmental reconstruction given by Pfenning and Davies by means of a natural deduction approach that makes a distinction between valid and true formulae, constructively. Both systems and the proof of their equivalence are formally verified using the state-of-the-art proof assistant Coq. The proof approach taken throughout the paper unveils the use of some alternative proof methods that allow for a smooth transition from the high-level mathematical proofs to their mechanised counterparts.
Publication Year: 2019
Publication Date: 2019-07-03
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 5
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot