Base-extension Semantics for Intuitionistic Modal Logics

TL;DR

This paper develops a proof-theoretic semantics framework called base-extension semantics for intuitionistic modal logics, providing a direct proof-theoretic counterpart to Kripke models and establishing soundness and completeness.

Contribution

It introduces base-extension semantics for Simpson's intuitionistic modal logics, linking proof-theoretic semantics with existing proof systems.

Findings

Established B-eS for Simpson's intuitionistic modal logics

Proved soundness and completeness with respect to natural deduction systems

Provided a proof-theoretic alternative to Kripke models

Abstract

The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by proof-theoretic semantics, which is a logical realization of inferentialism, in which the meaning of constructs is understood through their use. The key idea in proof-theoretic semantics is that of a base of atomic rules, all of which refer only to propositional atoms and involve no logical connectives. A specific form of proof-theoretic semantics, known as base-extension semantics (B-eS), is concerned with the validity of formulae and provides a direct counterpart to Kripke models that is grounded in the provability of atomic formulae in a base. We establish, systematically, B-eS for Simpson's intuitionistic modal logics and, also systematically, obtain soundness and completeness theorems with respect to Simpson's natural deduction systems.