Axiomatic and dual systems for constructive necessity, a formally verified equivalence

Journal of Applied Non-Classical Logics 29 (3):255-287 (2019)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 80,119

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Solutions in Constructive Field Theory.Leif Hancox-Li - 2017 - Philosophy of Science 84 (2):335-358.
A Study in Paradoxes and Type-Free Theories.Inkyo Chung - 1990 - Dissertation, University of Minnesota


Added to PP

7 (#1,068,322)

6 months
3 (#241,683)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Favio Ezequiel Miranda-Perea
National Autonomous University of Mexico

References found in this work

Modal Logic: An Introduction.Brian F. Chellas - 1980 - New York: Cambridge University Press.
Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
A New Introduction to Modal Logic.M. J. Cresswell & G. E. Hughes - 1996 - New York: Routledge. Edited by M. J. Cresswell.
Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.

View all 34 references / Add more references