We discuss a modular natural deduction framework for intuitionistic modal logics dealing with applicative functors and verificationist knowledge, extending a calculus for belief/applicative programming ( IEL− ) to one (IEL) for knowledge in mathematics and other contexts as well. Through the proofs-as-programs paradigm, we map these systems into modal type theories and prove strong normalisation via CPS translations, uniformly handling detours and permutations. Finally, we give a categorical interpretation of the modal operator as a monoidal functor, reflecting the rewrite structure of the calculi.
entire records (Figure 1e), guaranteeing all validation functions execute regardless of individual failures.
A key advantage of this approach is that it enables computational optimisations which are
unavailable in a purely monadic context. Because the arguments in an applicative computation are
independent of one another, validation functions can be executed concurrently without violating
referential transparency. Furthermore, under parallel evaluation, time complexity transforms from
sequential (1 + 2 + · · · + ) – where ≤ validations execute before first failure – to parallel
(max(1, 2, . . . , )) – where all validators execute concurrently.
type ('a, 'e) validation_result =
| Success of 'a
| Failure of 'e list
type validation_error =
| UsernameTooShort
| InvalidEmail
| AgeTooYoung
Intuitionistic epistemic states. On the purely modal front, verificationist epistemic logic has been
developed axiomatically and semantically by [
The two-part scenario in Figure 2 would make these points more concrete. The story’s first part aligns
with a verificationist account of belief. The second part explains factivity of knowledge in intuitionistic
terms and qualifies it as a formal BHK-based version of knowledge as belief tracking the truth of the
matter under discussion proposed by [
Introduced first in [ 22], natural deduction systems for classical and intuitionistic logic, usually denoted by NK and NJ, respectively, provide a formal model for deduction under hypotheses. The key feature of these systems is the absence of logical axioms from the calculus. The entire deductive apparatus relies only on inference rules that encode the atomic deductive steps involved in any logical argument and reflect the operational meaning of the logical connectives of a given base language. Starting from assumptions – any formula is per se a proof whose premise and conclusion are itself – intuitionistic deductions are then developed according to the rules in Figure 3, defining the propositional fragment of NJ, that we denote by NJp.
By identifying the types of a simple type theory with the same grammar generating the propositional formulas of NJp, we can then define a further correspondence between labelled deductions in NJp and the type assignments for typed terms, via the mapping shown in Figure 4. Thus, we can manipulate deductions in the proof system by performing computations in simple type theory.
Definition 1. Let Ξ denote the reflexive and transitive closure of the relation >Ξ defined as follows: 1 Detours: ∙ (. ) >Ξ [ := ]
∙ (1, 2) >Ξ ∙ C(in, .1, .2) >Ξ [ := ] Permutations: ∙ C(C(, .1, .2), .1, .2) >Ξ C(, .C(1, .1, .2), .C(2, .1, .2)) ∙ C(, .1, .2) >Ξ C(, .1, .2) ∙ C(, .1, .2) >Ξ C(, . 1, . 2) ∙ ⊥ ( ) >Ξ ⊥ ( ) ∙ ⊥ ( ) >Ξ ⊥ ( ) ∙ C(⊥ ( ), .1, .2) >Ξ ⊥ ( ) ∙ ⊥ (⊥ ( )) >Ξ ⊥ ( ) where [ := ] denotes the substitution of for all free occurrences of in .
A Ξ-normal form is just a typed term that cannot be rewritten with respect to Ξ. For this system of rewritings, it is possible to prove a confluence property and a strong normalisation theorem,2 whose correspondent for NJp is proven in [24, 25].
Calculus design. We refer to [
∨ ∨ℐ2 []
[] 1 →−↦ in1. : , →−↦ in2. : , →−↦ (⊥ ) : →−↦* : ⊤ ∨ℰ 2 →↦− C(, ( : .1), ( : .2)) where C bounds all occurrences of in 1 and all occurrences caoonfrdrespo,innd1,t22o, ′, 1, 2, resp. Definition 2. Let IEL be the calculus extending NJp by the following rules:
Notice that the rule □ ℐ difers from the one introduced by [ 26] by allowing the set Δ of additional hypotheses in the subdeduction of . The □ ℰ -free fragment of IEL is denoted by IEL− and corresponds to the natural deduction calculus for intuitionistic belief of [19].
We write Γ ⇒L when is derivable in L for L ∈ {IEL− , IEL} assuming the set of hypotheses
Γ, and we write L ⊢ when ∅ ⇒L . Denoting provability in the axiomatic calculi of [
Normalisation. Building on common notations for the standard Curry-Howard correspondence we recall in the opening of this section, we obtain modal -calculi by decorating L-deductions with proof names: we only need to extend the mapping of Figure 4 with type constructors for □ ℐ (box[1, · · · , ]. with 1, · · · , ) and □ ℰ (unbox with .).
The rewriting system Ξ of Def. 1 (based on the conversions from [24]) is then extended by the conversions in Figure 5, which we state in natural deduction fashion for the sake of readability. ⇝ □ · · · Γ . .
. □ ⃗ ⇝ □ ⇝ □ · · ·
1. Deductions in IEL− strongly normalise w.r.t. the rewriting system Ξ + □ 2. Deductions in IEL strongly normalise w.r.t. the rewriting system Ξ + □ + □ . + □ + □ + □ .
Proof. A simple CPS translation as in [19] cannot handle modal permutations: we need a variant ⟨−⟩ it, from our modal -calculus to simple type theory, defined as follows: of ⟨⊥⟩ := ⊥ ⟨⊤⟩ := ⊤ ⟨⟩ := To 1. ⟨ → ⟩ := ⟨⟩ → ⟨⟩ ⟨ ∧ ⟩ := ⟨⟩ ∧ ⟨⟩ ⟨ ∨ ⟩ := ⟨⟩ ∨ ⟨⟩ ⟨□ ⟩ := ⟨⟩ ∨
It is then straightforward to check that both □ and □ are preserved by this translation, and recovered by permutation conversions of Ξ. Since deductions in NJp are strongly normalising w.r.t. Ξ – as proven in e.g. [24] – we have the desired strong normalisation for IEL− -deductions.
To 2. As for the previous point, by imposing ⟨□ ⟩ := ∨ ⊥ and ⟨unbox with .⟩ := C(⟨ ⟩, .⟨⟩, .). This translation tweaks preserve □ and □ too, using applications of rewritings in Ξ concerning ∨-detours and permutations.
Combined with associated proofs of the subformula property of normal L-deductions, normalisation has interesting corollaries for these logics, namely: consistency, decidability, disjunction property, □ -primality, and modal disjunction property [19, 27].
Categorical semantics. The correspondence between type theory and natural deduction is further extended to category theory via the Curry-Howard-Lambek correspondence summarised by the partial glossary of Figure 6.
Logic proposition
proof theorem conjunction
true implication disjunction false
Type Theory type term inhabitant product type
unit type function type sum type empty type
Category Theory object arrow element-arrow
product terminal object
exponential (weak) coproduct (weak) initial object
The defining properties of these categorical constructions correspond to rewritings of deductions in NJp, as documented in [28, Ch. I.8]. Note, however, that the system of rewritings imposed by the universal properties of the initial object and coproducts is a proper extension of Ξ from Def. 1. We thus refer to the categorical counterparts of ⊥ and ∨ w.r.t. system Ξ as the weak initial object and weak coproduct, respectively.
For space reasons, we omit the standard definition of the notions for categories, functors, and natural transformations – we refer the reader to classic textbooks such as [28] and [29] for more details – to recall that any category having products and exponentials for any of its objects is called cartesian closed (CCCat); moreover, if it has also (weak) coproducts, it is called bi-cartesian closed (bi-CCCat).
For epistemic operators, we need to add to the basics of the categorical semantics for NJp the following definitions.
Definition 3.
Given any CCCat C , • an endofunctor F : C → C is pointed if there exists a natural transformation : C ⇒ F such that F ∘ = ∘ , where is called the point of F. • a monoidal endofunctor consists of a functor F : C → C together with – a natural transformation , : F × F → F( × ); – a morphism 1 : 1 → F1, when × ∘ F, = G, ∘ × and 1 ∘ 1F = 1G ∘ id1.
preserving the monoidal structure of C .3 These are called structure morphisms of F. • given monoidal endofunctors F, G : C → C , a natural transformation : F ⇒ G is monoidal Definition 4. An IEL− -category is given by a bi-CCCat C together with a monoidal pointed endofunctor K whose point is monoidal. When K preserves the initial object 0 of C up-to-isomorphism, we say that K is dense, and C is an IEL-category.
It is not hard to see that □ is needed to prove that the construction induced by the modal operator preserves arrow composition. However, that construction cannot be a functor unless one considers the Γ . . following extensionality principle □ for □ ℐ: . ⇝ □ [] □
IEL− -deductions strongly normalise w.r.t. the rewriting system Ξ+ □ + □ + □ + □ : The translation ⟨−⟩ is capable of mimicking □ in a simple type theory extended by a sum extensionality principle ∨, which in type-theoretic syntax can be defined as C(, .in1(), .in2()) > ∨ . Normalisation of L-deductions w.r.t. Ξ + □ + □ + □ + □ is then derived from the fact that ∨reductions can be postponed in any sequence of Ξ + ∨-rewritings, so that simple type theory is normalising w.r.t. Ξ + ∨ too [23, Ch. 4]. The adequacy of this categorical interpretation is now natural to state and prove: Γ . .
.
□ □ ℐ
(i) Let C be an IEL− -category. Then there is a canonical interpretation J− K of IEL− in C such that – a formula is mapped to a C -object JK; – a deduction of 1, · · · , ⇒IEL− is mapped to an arrow J K : J1K×· · ·× JK → JK; – for any two deductions and which are equal modulo Ξ + □ + □ -rewritings, we have
J K = JK.
The analogous soundness result holds for any IEL-category, by considering the system of rewritings Ξ + □ + □ + □ extended by □ . (ii) If the interpretation of two L-deductions is equal in all L-categories, then the two deductions are equal modulo Ξ + □ + □ + □ + □ .
I am grateful to the two anonymous reviewers for their constructive feedback and suggestions.
This work was partially supported by: the project SERICS – Security and Rights in CyberSpace PE0000014, financed within PNRR, M4C2 I.1.3, funded by the European Union - NextGenerationEU (MUR Code: 2022CY2J5S, CUP: D67G22000340001); the International Research Network “Logic and Interaction”; the EC-COST Action (CA20111) “EuroProofNet”.
3See [29, Sect. VII.1] for the corresponding commuting diagrams and the definition of monoidal category. pp. 869–914. URL: https://proceedings.mlr.press/v274/dinu25a.html. [19] C. Perini Brogi, Curry-Howard-Lambek Correspondence for Intuitionistic Belief, Studia Logica 109 (2021) 1441–1461. doi:10.1007/S11225-021-09952-3. [20] D. Leivant, Syntactic translations and provably recursive functions, The Journal of Symbolic Logic 50 (1985) 682–688. [21] D. van Dalen, Logic and Structure, 4th ed., Springer, 2008. [22] G. Gentzen, Untersuchungen über das logische Schließen I, Mathematische zeitschrift 39 (1935) 176–210. [23] M. H. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2006. [24] D. Prawitz, Ideas and results in proof theory, in: Studies in Logic and the Foundations of
Mathematics, volume 63, Elsevier, 1971, pp. 235–307. [25] P. Mancosu, S. Galvan, R. Zach, An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs, Oxford University Press, 2021. [26] V. de Paiva, E. Ritter, Basic constructive modality, Logic without Frontiers: Festschrift for Walter
Alexandre Carnielli on the occasion of his 60th Birthday (2011) 411–428. [27] C. Perini Brogi, Investigations of proof theory and automated reasoning for non-classical logics,
Ph.D. thesis, University of Genoa, Italy, 2022. [28] J. Lambek, P. J. Scott, Introduction to higher-order categorical logic, volume 7, Cambridge University Press, 1988. [29] S. Mac Lane, Categories for the working mathematician, volume 5, Springer Science & Business
Media, 2013. [30] I. van der Giessen, Admissible rules for six intuitionistic modal logics, Ann. Pure Appl. Log. 174 (2023) 103233. doi:10.1016/J.APAL.2022.103233. [31] S. Guerrini, A. Masini, M. Zorzi, Natural deduction calculi for classical and intuitionistic S5, J.
Appl. Non Class. Logics 33 (2023) 165–205. doi:10.1080/11663081.2023.2233750. [32] C. Hagemeier, D. Kirst, Constructive and mechanised meta-theory of IEL and similar modal logics, J. Log. Comput. 32 (2022) 1585–1610. doi:10.1093/LOGCOM/EXAC068.