A new perspective on intuitionistic and non-classical modal logics
The formalization of model-theoretic semantics for non-classical modal logics is often uniquely challenging. In the classical setting, propositional models are defined through functions that assign truth values to propositions, whereas modal semantics are defined through Kripke models that contain a set of propositional models (its "worlds") plus some relation between them. The problem is that many non-classical logics already require the use of Kripke models in their propositional semantics, so it is not clear (neither from a technical nor from a conceptual perspective) what their modal semantics should look like. In the case of intuitionistic logic, the answer traditionally provided by the literature takes the shape of a birelational model, which is a Kripke model with two distinct relations between its classical propositional models -- the first is used to induce the desired intuitionistic propositional behaviour, and the second plays the role of a proper modal relation. This answer is not entirely satisfactory since, in order to provide semantics for some interesting intuitionistic modal logics, we need to restrict our models by requiring satisfaction of some "interaction conditions" between the two relations, which bring about some practical complications and are also not easy to justify from a conceptual viewpoint. In this context, our work tries to promote a very simple change of perspective that leads to a new kind of modal semantics for intuitionistic logic in particular and non-classical logics in general. First, we show that it is indeed possible to define an intuitionistic modal model as a set of intuitionistic propositional models plus some relation between them, which leads to a natural generalization of the very notion of a Kripke model. Second, we argue that the same temporal intuitions used to philosophically justify propositional intuitionistic models also justify the new modal semantics. Third, we prove that this framework is mathematically equivalent to the birelational one by providing mappings from one class of models into the other. Fourth, we show that the "interaction conditions" externally imposed on birelational models emerge naturally from the new framework and don't need to be explicitly stipulated. Finally, we show that this also leads to a modular approach capable of generating a reasonable modal version of each and every non-classical logic semantically characterized by Kripke models.
A new approach to Base-extension semantics for Classical Logics
In this talk I will present a new approach to giving a Base-extension Semantics for a logic based on considering literals as basic. This simple change allows one to capture classical behaviours whilst retaining the same broad structure as introduced by Sandqvist for Intuitionistic Logics. I will then show how this new approach can be used to give a new, intrinsic, semantics for the Classical Modal Logic S4.
Bilateral base-extension semantics
Bilateralism is the position according to which assertion and rejection are conceptually independent speech acts. Logical bilateralism demands that systems of logic provide conditions for assertion and rejection that are not reducible to each other, which often leads to independent definitions of proof rules (for assertion) and dual proof rules, also called refutation rules (for rejection). Since it provides a critical account of what it means for something to be a proof or a refutation, bilateralism is often studied in the context of proof-theoretic semantics, an approach that aims to elucidate both the meaning of proofs (and refutations) and what kinds of semantics can be given if proofs (and refutations) are considered as basic semantic notions. In this paper we present a bilateral version of base-extension semantics—one of the most widely studied proof-theoretic semantics—by allowing atomic bases to contain both atomic proof rules and atomic refutation rules. The semantics is shown to be sound and complete with respect to the bilateral dual intuitionistic logic 2Int. Structural similarities between atomic proofs and refutations allow us to define duality notions for atomic rules, deductions and bases, which may then be used for the proof of bilateral semantic harmony results. Bilateral semantic harmony is shown to be a restatement of the syntactic horizontal inversion principle, whose meaning-conferring character may now be interpreted as the requirement of preservation of harmony notions already present at the core of the semantics.
A sequent view of PtS
We define base-extension semantics (Bes) using atomic systems based on sequent calculus rather than natural deduction. While traditional Bes aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a Bes framework more suited to classical semantics. The harmony in classical sequents leads to straightforward semantic clauses derived solely from right introduction rules.
This framework enables a Sandqvist-style completeness proof that extracts a sequent calculus proof from any valid semantic consequence. Moreover, we show that the inclusion or omission of atomic cut rules meaningfully affects the semantics, yet completeness holds in both cases.
In this talk we briefly discuss an extension of Kearns modal semantics to all the normal modal logics, providing a decision procedure for each logic by solving the analyticity problem.