This paper introduces NAMOR (New Agda MOdal Realization), a comprehensive Agda library for mechanizing modal proof theory through extended sequents. Our approach employs position-based reasoning that mirrors ifrst-order logic structures while maintaining implicit accessibility relations. Building on our previous investigation of extended deductive systems, NAMOR provides a unified framework for formalizing proof-theoretical properties across normal extensions of modal logic K, from basic K through S5. The library is founded on our novel sequent calculus E , which exhibits remarkable modularity: all captured logics share identical inference rules, difering mainly in their modal constraints. This enables systematic verification of meta-theoretical properties while preserving the intuitive structure of paper-and-pencil proofs. By leveraging Agda's expressive type system, NAMOR establishes a direct correspondence between formal proofs and their mathematical counterparts, creating a robust platform for symbolic reasoning in domains where modal logic naturally applies.
The recent renaissance in modal proof theory has introduced diverse deductive styles, including
labelled systems [
It is with these advantages in mind that we present NAMOR, a new Agda library for normal modal
logics designed to be as close as possible to pen-and-paper theory. Its main contributions are:
• A new sequent calculus, E , that provides a unified theoretical foundation for normal modal
logics. Building on our previous work [
CEUR Workshop
ISSN1613-0073
logic. This allows a wide range of normal modal logics—from K to S5—to be captured using an
identical set of deductive rules, distinguished only by their modal constraints.
• The implementation of this calculus in NAMOR, a new Agda library. We generalize the core
ideas from our previous implementation for S4.2 [
In Section 2 we present the sequent calculus E , we show some sample of the Agdaimplementation and we provide an example of axiom derivation in NAMOR; Related work are discussed in Section 3; Section 4 is devoted to discussion and future work.
relation ◁ ⇔ ∃ ∈ . = ∘ ⟨⟩ closures.
We first present the position-based sequent calculus E . According to some constraints of the rules □ ⊢, ⊢ ♦ and Cut, E
captures several normal extensions of the logic K by incorporating the basic
axiom ≡
≡ □ →
□ ( → ) → ( □ →
□ ) and one or more of the following axioms: ≡
□ →
♦ ,
, 4 ≡ □ → □
, .2 ≡ ♦□
→
♦□
and 5 ≡ →
□♦
. This results in K (containing
only the basic axiom ), D (K+D), T (K+T), K4 (K+4), D4 (K+D+4), S4 (K+T+4), S4.2 (K+T+4+.2) and S5
(K+T+4+5). The system is inspired by our previous work [
The language ℒ consists of a countably infinite set of propositional symbols 0, 1, …, propositional connectives ∧, ∨, →, ¬, ⊥, modal operators □ , ♦ , and a denumerable set of tokens (ranged over by , ,
), which act as atomic world-identifiers. Modal formulas are defined inductively as usual.
) is a finite sequence of tokens, i.e., an element of ∗ . We denote a sequence as ⟨ 1, … , ⟩, with ⟨ ⟩ being the empty sequence. The (associative) concatenation of positions is defined as ⟨ 1, … , ⟩ ∘ ⟨ 1, … , ⟩ = ⟨ 1, … , , 1, … , ⟩. On positions, we define the successor , and its reflexive ( ◁0), transitive (⊏), and reflexive-transitive ( ⊑) A position-formula (or p-formula) is an expression , where is a modal formula and is a position. An extended sequent (or e-sequent) is an expression Γ ⊢ Δ, where Γ and Δ are finite sequences of p-formulas.
The rules of E
are in Figure 1. Modal rules represent the core of the system and are common to all the logics. The system is designed as much as possible in analogy with first-order logic quantifiers as suggested by the constraints on ⊢ □ and ♦ ⊢, that are reminiscent of the analogous for ∀ and ∃: in the rules ⊢ □ on which ∘⟨⟩ and ♦ ⊢, one has ∘ ⟨⟩ ∉ ℑ[Γ, Δ] depends and ℑ[Σ] = { ∶ ∃ ∈ Σ. ⊑ } .
, where Γ and Δ are the lists of (open) assumptions
As previously said, all logics in the normal spectrum from K to S5 share the rules above; a specific system is obtained simply by “tuning” the constraints on the □ ⊢, ⊢ ♦ and on the cut rule for systems K and K4. Constraints on modal and cut rules are in Table 1 and Table 2, respectively.
Axiom and Cut Rule Structural Rules Propositional Rules ⊢
Γ, Γ ⊢⊢ΔΔ ⊢ Γ, , ⊢ Δ
Γ, ⊢ Δ ⊢ Γ1, , , Γ2 ⊢ Δ Γ1, , , Γ2 ⊢ Δ ⊢ Γ1 ⊢ , Δ1 Γ2, ⊢ Δ2 Γ1, Γ2 ⊢ Δ1, Δ2
Γ ⊢ Δ Γ ⊢ , Δ ⊢ Γ ⊢ , , Δ ⊢
Γ ⊢ , Δ Γ ⊢ Δ1, , , Δ2 ⊢ Γ ⊢ Δ1, , , Δ2 Modal Rules Γ, Γ∧, ⊢⊢ΔΔ ∧1 ⊢ Γ, Γ∧, ⊢⊢Δ Δ ∧2 ⊢ Γ1 ⊢ , Δ1 Γ2 ⊢ , Δ2 ⊢ ∧
Γ1, Γ2 ⊢ ∧ , Δ1, Δ2 Γ1, ⊢ Δ1 Γ2, ⊢ Δ2 ∨ ⊢ Γ1, Γ2, ∨ ⊢ Δ1, Δ2
Γ ⊢ , Δ ⊢ ∨1 Γ ⊢ ∨ , Δ
Γ ⊢ , Δ Γ ⊢ ∨ , Δ ⊢ ∨2 Γ1 ⊢ , Δ1 Γ2, ⊢ Δ2 →⊢ Γ1, Γ2, → ⊢ Δ1, Δ2
ΓΓ⊢, →⊢ ,,ΔΔ ⊢→ Γ, ⊢ Δ □ ⊢ Γ, □ ⊢ Δ Γ, ∘⟨⟩ ⊢ Δ Γ, ♦ ⊢ Δ ♦ ⊢ ΓΓ⊢⊢ □ ∘⟨⟩ ,,ΔΔ ⊢ □ ΓΓ⊢⊢♦ ,,ΔΔ ⊢ ♦ Calculus
ES5 ES4.2 ES4 ET ED ED4 EK4 EK
Constraints on the rules □ ⊢ and ⊢ ♦ no constraints ⊆ ⊑ ◁ 0 ◁ ⊏ ⊏ there is at least a formula ∘∘ in either Γ or Δ
◁ there is at least a formula ∘∘ in either Γ or Δ
Constraints on the cut rule
no constraints ∈ ℑ[Γ 1, Δ1 − ] or ∈ ℑ[Γ 2 − , Δ2] ⊢♦ : ∀ {M A Γ Δ} → modalConstraint M Γ Δ → Proof (Γ ,, [ A ^ ] ⊢ Δ) → Proof (Γ ,, [ □ A ^ ] ⊢ Δ) → modalConstraint M Γ Δ → Proof (Γ ⊢ [ A ^ ] ,, Δ) → Proof (Γ ⊢ [ ♦ A ^ ] ,, Δ)
Following Table 1, the specific constraint for each logic is implemented in the proof-assistant by the modalConstraints function, as follows: modalConstraint : Logic → position → position → List pf → List pf → Type modalConstraint S5 Γ Δ = Unit modalConstraint S4dot2 Γ Δ = ⊆ modalConstraint S4 Γ Δ = ⊑ modalConstraint T Γ Δ
= ◁0 modalConstraint D Γ Δ = ◁ modalConstraint D4 Γ Δ = ⊏ modalConstraint K4 Γ Δ = ⊏ × (Γ ,, Δ) has modalConstraint K Γ Δ = ◁ × (Γ ,, Δ) has Finally, following Table 2, constraints for the cut- rule are implemented in Agda as cutConstraint _ A Γ1 Γ2 Δ1 Δ2 = Unit cutConstraint : Logic → mf → position → List pf → List pf → List pf → List pf → Type cutConstraint K A Γ1 Γ2 Δ1 Δ2 = ( ∈ Init (Γ1 ,, (Δ1 - A ^ ))) ⊎ ( ∈ Init ((Γ2 - A ^ ) ,, Δ2)) cutConstraint K4 A Γ1 Γ2 Δ1 Δ2 = ( ∈ Init (Γ1 ,, (Δ1 - A ^ ))) ⊎ ( ∈ Init ((Γ2 - A ^ ) ,, Δ2)) In the next section we propose an example to show how both the constraints and the implementation work.
To show how the framework E
works, we propose two derivations of the Geach axiom, also called .2: □♦ → ♦□
. The Geach axiom is characteristic for the logic S4.2, an intermediate system between S4 and S5, that is particulary interesting and enjoy several applications both in mathematics and in computer science.
We first try to derive the axiom in the wrong system
the derivation. Then we show the correct derivation in the system S4.2.
Let’s start observing what happens if we try to derive .2 by setting NAMOR to logic S4: axiomG-S4-FAILED : ∀ {A} → (Proof ([] ⊢ [((♦ (□ A)) ⇒ (□ (♦ A)) ^ [])])) axiomG-S4-FAILED = ⊢⇒ (♦ ⊢ {x = "x"} {Γ = []} ( { (here ()) ; (there ()) }) (⊢□ {x = "y"} ( { (there (here ())) ; (there (there ())) }) (⊢♦ {M = S4} { = ⟨"y"⟩} { = ⟨"x"⟩ ∘ ⟨"y"⟩} {! !} {! !} ))) -- FAILURE The logic S4 has constraint
4 Γ Δ = ⊑ so for the ⊢♦ rule we need ⟨"y"⟩ ⊑ (⟨"x"⟩ ∘ ⟨"y"⟩). The meaning is that we are requiring ⟨"y"⟩ is a prefix of ⟨"x", "y"⟩, but it is not, so the constraint is not satisfied and the derivation fails.
One might wonder if choosing diferent tokens or swapping "x" and "y" could make the derivation work in S4. However, the failure is structural, not dependent on variable names. The modal rules force a specific order of token introduction: the ♦ elimination introduces "x" first, then the □ introduction introduces "y" . The resulting constraint always requires the second token to be a prefix of the concatenated position, which is impossible under the prefix relation regardless of the chosen variable names.
For the second derivation we set the constraints to capture S4.2 and then we have: axiomG : ∀ {A} → (Proof ([] ⊢ [((♦ (□ A)) ⇒ (□ (♦ A)) ^ [])])) axiomG = ⊢⇒ (♦ ⊢ {x = "x"} {Γ = []} ( { (here ()) ; (there ()) }) (⊢□ {x = "y"} ( { (there (here ())) ; (there (there ())) }) (⊢♦ {M = S4dot2} { = ⟨"y"⟩} { = ⟨"x"⟩ ∘ ⟨"y"⟩} ( {x} → there) (□ ⊢ {M = S4dot2} { = ⟨"x"⟩} { = ⟨"x"⟩ ∘ ⟨"y"⟩} {Γ = []} (xs⊆xs++ys ⟨ "x" ⟩ ⟨ "y" ⟩) Ax )))) The logic S4.2 has constraint:
4.2 Γ Δ = ⊆
For the ⊢♦ rule we need to specify ⟨"y"⟩ ⊆ (⟨"x"⟩ ∘ ⟨"y"⟩). This constraint is satisfied by ( {x} → there) that shows "y" is at position there in ["x", "y"]. For the □ ⊢ rule we need ⟨"x"⟩ ⊆ (⟨"x"⟩ ∘ ⟨"y"⟩). This constraint is satisfied by xs⊆xs++ys that shows ["x"] ⊆ ["x"] ++ ["y"]. So the derivation succeeds by applying the axiom rule.
We spend some words about here, there, and freshness patterns. In Agda, proofs of list membership are constructed with here (for the head) and there (for the tail). We use these to enforce freshness constraints in modal rules, which is analogous to the eigen-variable conditions in traditional sequent calculi.
For instance, to prove a token is fresh for an empty context, we must show it cannot be a member. We do this with a function that uses Agda’s absurd pattern () to demonstrate that both cases—the token being here or there—are impossible. This pattern-matching against an absurd case is a standard Agda idiom for proving negative properties, ensuring that new tokens are genuinely fresh.
The success of S4.2 lies in the flexibility of the subset relation ( ⊆) compared to the prefix relation. While positions in S4 must be ordered as prefixes (reflecting the transitivity of accessibility), S4.2 allows positions to be interpreted as sets, where subset inclusion is more permissive.
The automation of modal reasoning is receiving increasing attention from the research community. In
this context, it is worth mentioning recent developments in the HOL Light proof assistant by Maggesi
et al., which are closely aligned with our work with partially diferent motivations. In [
Our motivations are complementary. While HOLMS moves towards automated deduction, we
position our work at the level of meta-theoretical formalization. This is reflected in our choice of a classical,
LK-style calculus, which is well-suited for studying meta-properties, in contrast to the G3-style
systems (see, e.g., [
The development of NAMOR is an ongoing project that opens several directions for future work. Our
current goal is to formally verify the Cut-Elimination Theorem, a central results in proof-theory, for
the calculus E . Following our approach in [
Beyond this foundational work, our main short-term goal is to develop and implement semantics for
specific instances of E . We are particularly focused on S4.2 [
Finally, we plan to explore the computational interpretations of our work. The logic S5, for instance,
has deep connections to computation [
During the preparation of this work, the authors used Gemini 2.5 Pro in order to: Grammar and spelling check, Paraphrase and reword. After using this tool/service, the authors reviewed and edited the content as needed and takes full responsibility for the publication’s content. [20] S. Guerrini, A. Masini, M. Zorzi, Natural deduction calculi for classical and intuitionistic S5, Journal of Applied Non-Classical Logics 33 (2023) 165–205. doi:10.1080/11663081.2023.2233750.