Natural deduction and semantic models of justification logic in the proof assistant Coq
Jesús Mauricio Andrade Guzmán, Francisco Hernández Quiroz · Logic Journal of IGPL · 2020
Abstract The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for $\mathsf{L}\mathsf{P}$ with respect to Fitting models.