Abstract

Justification logics are explicit versions of modal logic. In the classical setting, this means boxes are refined with explicit proof terms and interact with each other through proof operations. This exercise was extended to intuitionistic modal logic with native diamonds. In this setting, diamonds are refined to satisfier terms and come equipped with additional operations.

Justification logic enjoys a connection to its corresponding modal logic through a realisation theorem. In the classical setting, this is achieved through either proof-theoretic or semantic methodology. So far, intuitionistic justification logic with satisfiers has only been presented syntactically with a proof-theoretic realisation theorem.

We present two classes of semantics for intuitionistic justification logic with soundness and completeness results: basic modular models, which extend possible world semantics for intuitionistic propositional logic; modular models which contain Kripke-style machinery to promote “backwards compatibility” to modal logic. Using modular models, we present a realisation theorem to establish a connection between intuitionistic justification logic and its corresponding intuitionistic modal logic.

1 Introduction↩︎

Justification logic makes knowledge explicit by attaching reasons to statements. It refines modalities in standard modal logic: the usual \(\Box_{}A\), which can mean “\(A\) is provable or known", is replaced with \([\mathtt{t}] A\) for some proof term \(\mathtt{t}\), interpreted as”\(\mathtt{t}\) is a proof or evidence of \(A\)".

Realisation theorem. The first proposed justification logic is the Logic of Proofs (\(\mathsf{LP}\)), introduced by Artemov [@artemov_operational_1995], which makes the modal logic \(\mathsf{S4}\) explicit. This is achieved formally via a realisation theorem translating each theorem of \(\mathsf{S4}\) into its corresponding theorem in \(\mathsf{LP}\) by realising every \(\Box_{}\) modality into a suitable proof term. The realisation theorem was first proved by Artemov using a proof-theoretic (and constructive) methodology [@artemov_explicit_2001], and later on via semantic techniques by Fitting [@fitting_logic_2005].

Semantics for justification logic. Originally, the logic of proofs was interpreted using proofs in Peano Arithmetic (\(\mathsf{PA}\)) [@artemov_operational_1995]. Later, simple and flexible semantic models akin to epistemic (possible-world) models were created, in which justification terms represent evidence rather than explicit arithmetic proofs [@mkrtychev_models_1997; @fitting_logic_2005]. These models helped apply justification logic in a more general fashion to the concepts of knowledge and evidence, better understand what justification terms mean, and prove important logical properties like decidability [@bucheli_decidability_2011] and complexity bounds [@kuznets_complexity_2000].

Intuitionistic justification logic. Since \(\mathsf{LP}\) interprets proofs in classical arithmetic, an intuitionistic version of the Logic of Proofs (\(\mathsf{iLP}\)) was sought to represent proofs in Heyting Arithmetic (\(\mathsf{HA}\)) [@artemov_basic_2007; @dashkov_arithmetical_2011]. Though \(\mathsf{iLP}\) is more than just \(\mathsf{LP}\) over intuitionistic logic: to match the proof interpretation in \(\mathsf{HA}\), additional axioms representing admissible rules must be included. The base logic (without these additional axioms) was shown to be an explicit justification version of intuitionistic modal logic \(\mathsf{iS4}\) [@artemov_unified_2002]. Its semantics was studied in [@marti_intutionistic_2016], where they provide intuitionistic Kripke-style models and prove completeness, and its proof theory in [@hill_analytic_2019]. Intermediate variants of \(\mathsf{LP}\) were also studied by Pischke [@pischke_intermediate_2023] providing in particular an adaptation of the semantic realisation technique.

Intuitionistic diamonds. In classical modal logic, \(\Box_{}\) and \(\Diamond_{}\) are dual, i.e., \(\Diamond_{}A\) can be defined as \(\mathord{\neg}\Box_{}\mathord{\neg}A\), making the behaviour of \(\Diamond_{}\) automatically determined by the one of \(\Box_{}\). However, the weaker negation of intuitionistic logic breaks this duality: \(\Diamond_{}\) must be given its own independent semantics and axioms, as it cannot simply be defined in terms of \(\Box_{}\). Furthermore, the addition of certain \(\Diamond_{}\)-axioms produces logics which are not conservative over the \(\Diamond_{}\)-free language [@das2023intuitionistic; @GroShiClo25; @DasGroShi25-blog], which justifies the interest in intuitionistic variants of modal logics with both modalities [@fischer_servi_modal_1977; @simpson_proof_1994].

Diamonds in justification logic. In justification logic, even intuitionistic variants, \(\Diamond_{}\) was never considered as a first-class citizen. The first justification logic which makes the \(\Diamond_{}\) modality explicit was postulated by [@kuznets_justification_2021] as a justification counterpart to constructive modal logic \(\mathsf{CK}\) [@bellin_extended_2001] with a syntactic realisation result. This work was then extended to provide a justification counterpart to intuitionistic modal logic \(\mathsf{IK}\) [@fischer_servi_modal_1977] syntactically in [@marin_justification_2025] with a proof-theoretic procedure based on nested sequents.

Contributions. We continue this line of work with a semantic exploration of intuitionistic justification logics (with \(\Diamond_{}\)). We extend the definition of basic intuitionistic modular models and intuitionistic modular models of [@marti_intutionistic_2016], and establish soundness and completeness results with respect to these semantics for \(\mathsf{JIK}\), the justification counterpart of intuitionistic modal logic \(\mathsf{IK}\). Building on these results, our investigation is crowned by an adaptation of the semantic realisation procedure in [@pischke_intermediate_2023] to \(\mathsf{JIK}\).

Outline. In Section 2 we introduce the preliminaries on \(\mathsf{IK}\) and intuitionistic justification logic \(\mathsf{JIK}\), notably providing some key properties of the latter logic our work relies on. In Section 3 we introduce basic intuitionistic modular models which extend [@marti_internalized_2018; @pischke_intermediate_2023] to incorporate the \(\Diamond_{}\) operator, and prove that they are still enough to ensure completeness with \(\mathsf{JIK}\). In Section 4 we expand on these to get intuitionistic modular models. They require more adaptation due to the addition of \(\Diamond_{}\) on the one hand, and to the complexity inherent to the semantics for \(\mathsf{IK}\) on the other hand. Indeed, the confluence conditions traditionally expected in the semantics for \(\mathsf{IK}\) are superfluous for justification \(\mathsf{JIK}\) (given that persistence already holds in the basic semantics) but they are needed to ensure backward compatibility with \(\mathsf{IK}\) in the realisation theorem. In Section 5 we are indeed able to prove the realisation theorem, that \(\mathsf{IK}\) and \(\mathsf{JIK}\) formally correspond, by adapting the semantic method [@fitting_logic_2005; @pischke_intermediate_2023] to \(\mathsf{IK}\) and the intuitionistic \(\Diamond_{}\). We conclude in Section 6 with some discussions on avenues for taking these ideas further.

2 Preliminaries↩︎

Let \(\mathsf{Prop}\) be a countable set of propositional variables. The language of modal logic \(\mathcal{L}_{\Box_{}}\) is defined by \[G \coloncolonequals p\in\mathsf{Prop}\mid \mathord{\mathord{\bot}}\mid G \mathbin{\wedge}G \mid G \mathbin{\vee}G \mid G \mathbin{\to}G \mid \Box_{}G \mid \Diamond_{}G\]

Let \(\mathsf{Int}\) be a finite set of axioms for \(\mathsf{IPL}\), e.g. [@troelstra_basic_2000]. We add a superscript \(I\) to denote the set of axiom instances of a given set of axioms, e.g. \(\mathsf{Int}^{I}\) for the set of axiom instances of \(\mathsf{Int}\). We define \(\mathsf{Mod}\) to be the set of axioms extending \(\mathsf{Int}\) with the modal axioms presented below [@plotkin_framework_1986].

\(\begin{array}{rcl} \mathsf{{k}_{1}} & : & \Box_{}(G \mathbin{\to}H) \mathbin{\to}(\Box_{}G \mathbin{\to}\Box_{}H) \\ \mathsf{{k}_{2}} & : & \Box_{}(G \mathbin{\to}H) \mathbin{\to}(\Diamond_{}G \mathbin{\to}\Diamond_{}H) \\ \end{array} \quad \begin{array}{rcl} \mathsf{{k}_{3}} & : & \Diamond_{}(G \mathbin{\vee}H) \mathbin{\to}(\Diamond_{}G \mathbin{\vee}\Diamond_{}H) \\ \mathsf{{k}_{4}} & : & (\Diamond_{}G \mathbin{\to}\Box_{}H) \mathbin{\to}\Box_{}(G \mathbin{\to}H) \\ \end{array} \quad \begin{array}{rcl} \mathsf{{k}_{5}} & : & \Diamond_{}\mathord{\mathord{\bot}}\mathbin{\to}\mathord{\mathord{\bot}} \end{array}\)

Definition 1. The logic \(\mathsf{IK}\) is the set of consecutions \(\Gamma \vdash_{} G\), where \(\Gamma= \ifthenelse{\equal{}{}} {\{G_1,\dots,G_n\}} {\{ \mid G_1,\dots,G_n\}}\) is a finite set of formulas, derivable in the system described by the following rules.

\(\inferLineSkip=3pt \infer[\hyperlink{rule:ax}{\mathsf{ax}}]{\Gamma \vdash_{} G}{G\in\mathsf{Mod}^{I}}\)

\(\inferLineSkip=3pt \infer[\hyperlink{rule:id}{\mathsf{id}}]{\Gamma \vdash_{} G_i}{1\leq i \leq n}\)

\(\inferLineSkip=3pt \infer[\hyperlink{rule:nec}{\mathsf{nec}}]{\Gamma \vdash_{} \Box_{}G}{\emptyset \vdash_{} G}\)

\(\inferLineSkip=3pt \infer[\hyperlink{rule:MP}{\mathsf{mp}}]{\Gamma \vdash_{} H}{ \Gamma \vdash_{} G & \Gamma \vdash_{} G\mathbin{\to}H}\)

If the consecution \(\Gamma \vdash_{} G\) is provable in the system for \(\mathsf{IK}\), we write \(\Gamma \vdash_{\mathsf{IK}} G\). We omit the curly brackets when clear from context and write \(G_1, \dots, G_n \vdash_{\mathsf{IK}} G\) for \(\ifthenelse{\equal{}{}} {\{G_1, \dots, G_n\}} {\{ \mid G_1, \dots, G_n\}} \vdash_{\mathsf{IK}} G\). For a potentially infinite set of formulas \(\primeset\), we write \(\primeset \vdash_{\mathsf{IK}} G\) if there are formulas \(G_1, \dots, G_n \in \Gamma\) such that \(G_1, \dots, G_n \vdash_{\mathsf{IK}} G\). We write \(\primeset, H \vdash_{\mathsf{IK}} G\) for \(\primeset \cup \ifthenelse{\equal{}{}} {\{H\}} {\{ \mid H\}} \vdash_{\mathsf{IK}} G\), and \(\vdash_{\mathsf{IK}} G\) for \(\emptyset \vdash_{\mathsf{IK}} G\).

The fact that the premise of the \(\hyperlink{rule:nec}{\mathsf{nec}}\) rule requires an empty context entails that we capture the local modal logic \(\mathsf{IK}\), understood as a consequence relation. A benefit of this rule is that the deduction theorem holds [@hakli_does_2012], a result implicitly used in some of the results below about \(\mathsf{IK}\).

With the syntax and axiomatic system of \(\mathsf{IK}\) defined, we turn to its (bi)relational semantics [@fischer_servi_modal_1977; @fischer_servi_semantics_1980].

Definition 2 (Frames). A (birelational) frame* is a tuple \((W, \leq, R)\), where \(W\) is a non-empty set of worlds, \(\leq\) is a preorder on \(W\) and \(R\) is a binary relation on \(W\) such that:*

for all worlds \(w, v, v'\) with \(w Rv \leq v'\), then there exists a world \(w'\) with \(w \leq w' Rv'\);
for all worlds \(w, w', v\) with \(w \leq w'\) and \(w Rv\), there exists a world \(v'\) with \(w' Rv'\) and \(v \leq v'\).

Note that \(BC\) stands for Backward Confluence, while \(FC\) stands for Forward Confluence.

Definition 3 (Models). A (birelational) model* for \(\mathsf{IK}\), is a tuple \(\mathcal{M}= (W, \leq, R, *)\) with \((W, \leq, R)\) a frame equipped with a map \(* : \mathsf{Prop}\times W \rightarrow \ifthenelse{\equal{}{}} {\{0, 1\}} {\{ \mid 0, 1\}}\) such that \(w \leq v\) and \(*(p,w)=1\) entail \(*(p,v)=1\). We henceforth use the notation \(p^{*}_{w}\) for \(*(p,w)\). For a model \(\mathcal{M}\), a point \(w\in W\) and a formula \(G\), the truth of \(G\) at \(w\) in \(\mathcal{M}\) is recursively defined on the structure of \(G\): \[\begin{array}{lcl} \mathcal{M} , w \Vdash p & \text{iff} & p^{*}_{w} = 1 \\ \mathcal{M} , w \Vdash\mathord{\mathord{\bot}} & & \text{never} \\ \mathcal{M} , w \Vdash G \mathbin{\wedge}H & \text{iff} & \text{\mathcal{M} , w \Vdash G and \mathcal{M} , w \Vdash H} \\ \mathcal{M} , w \Vdash G \mathbin{\vee}H & \text{iff} & \text{\mathcal{M} , w \Vdash G or \mathcal{M} , w \Vdash H} \\ \mathcal{M} , w \Vdash G \mathbin{\to}H & \text{iff} & \text{for all worlds w' with w \leq w', if \mathcal{M} , w' \Vdash G then \mathcal{M} , w' \Vdash H} \\ \mathcal{M} , w \Vdash\Box_{}G & \text{iff} & \text{for all worlds w', v' with w \leq w' Rv', \mathcal{M} , v' \Vdash G} \\ \mathcal{M} , w \Vdash\Diamond_{}G & \text{iff} & \text{there exists world v with w Rv, \mathcal{M} , v \Vdash G} \end{array}\] We write \(\mathcal{M} , w \Vdash\Gamma\) if \(\mathcal{M} , w \Vdash G\) for all \(G \in \Gamma\). We write \(\vDash G\) if \(\mathcal{M} , w \Vdash G\) for any \(\mathcal{M}\) and \(w\in W\).*

The following relates the semantic and axiomatic definitions of \(\mathsf{IK}\).

Theorem 1 (Soundness and Completeness [@fischer_servi_axiomatizations_1984; @plotkin_framework_1986; @simpson_proof_1994]). \(\vdash_{\mathsf{IK}} G \iff \vDash G\).

Later in the paper, we make use of the following consequence of soundness.

Corollary 1. \(\mathsf{IK}\) is consistent.

2.2 Intuitionistic Justification Logic↩︎

The sets of proof terms \(\mathsf{PrfTm}\) and of satisfier terms \(\mathsf{SatTm}\) are defined by mutual induction as follows

\(\mathtt{t} \coloncolonequals\mathtt{c}_{}\in\mathsf{PrfConst}\mid \mathtt{x_{\mathnormal{}}}\in\mathsf{PrfVar}\mid \mathtt{t} \mathbin{\cdot} \mathtt{t} \mid \mathtt{t} \mathbin{+} \mathtt{t} \mid {!}^{\mathnormal{}}\mathtt{t} \mid \mathtt{m} \mathbin{\triangleright} \mathtt{t} \qquad \mathtt{m} \coloncolonequals\mathtt{a_{\mathnormal{}}}\in\mathsf{SatVar}\mid \mathtt{m} \mathbin{\sqcup} \mathtt{m} \mid \mathtt{t} \mathbin{\star} \mathtt{m}\)

where proof constants \(\mathsf{PrfConst}\), proof variables \(\mathsf{PrfVar}\) and satisfier variables \(\mathsf{SatVar}\) are countable sets. The language of justification logic \(\mathcal{L}_{\mathsf{J}}\) reuses the set \(\mathsf{Prop}\) as shown in the following grammar \[A \coloncolonequals p\in\mathsf{Prop}\mid \mathord{\mathord{\bot}}\mid A \mathbin{\wedge}A \mid A \mathbin{\vee}A \mid A \mathbin{\to}A \mid [\mathtt{t}] A \mid \langle \mathtt{m} \rangle A\] where \(\mathtt{t} \in\mathsf{PrfTm}\) and \(\mathtt{m} \in\mathsf{SatTm}\).

Before defining logics over \(\mathcal{L}_{\mathsf{J}}\), we provide some intuitions on the intended meaning of the operators over proof and satisfier terms.

In justification logic, a formula of the shape \([\mathtt{t}] A\) can be read as \(\mathtt{t}\) is a proof of A. Proof terms can hence be thought of as capturing global reasoning, i.e. they assert the validity of statements with respect to any model. Dually, satisfier terms relate to local reasoning: \(\langle \mathtt{m} \rangle A\) could be read as \(\mathtt{m}\) is a model where \(A\) is satisfied, implying the consistency of \(A\). The operations proof sum \(\mathtt{} \mathbin{+} \mathtt{}\), application \(\mathtt{} \mathbin{\cdot} \mathtt{}\) and proof checker \({!}^{\mathnormal{}}\mathtt{}\) are standard justification operations relating to common proof manipulations [@artemov_operational_1995; @artemov_explicit_2001]. The operation on satisfiers of disjoint union \(\mathtt{} \mathbin{\sqcup} \mathtt{}\) is quite naturally the local counterpart to the proof sum. The propagation operation \(\mathtt{} \mathbin{\star} \mathtt{}\) combines global and local reasoning by taking as arguments a proof term and a satisfier term [@kuznets_justification_2021]. For example, the locality of \(A\) in \(\langle \mathtt{m} \rangle A\) can be exploited via the global holding of \(A \mathbin{\to}(A \mathbin{\vee}B)\) in \([\mathtt{\mathtt{t}}] (A \mathbin{\to}(A \mathbin{\vee}B))\) to locally establish \((A \mathbin{\vee}B)\) as \(\langle \mathtt{\mathtt{t} \mathbin{\star} \mathtt{m}} \rangle (A \mathbin{\vee}B)\). Finally, the local update operation \(\mathtt{} \mathbin{\triangleright} \mathtt{}\) expresses that if local reasoning implies global reasoning, global information can be updated using local information [@marin_justification_2025]. For example, if the satisfier \(\mathtt{m}\) locally reasons about \(A\) and implies the proof term \(\mathtt{t}\) globally reasons about \(B\), then this connection is updated into global reasoning by making the proof term \(\mathtt{m} \mathbin{\triangleright} \mathtt{t}\) globally reason about \(A \mathbin{\to}B\). While the interpretations of operations on proof terms are formally backed up by the completeness proof with respect to Peano arithmetic in the context of classical Logic of Proofs [@artemov_explicit_2001], in the intuitionistic context, these merely constitute guidelines to help us reason about the operations at a high-level and would require to be studied within a meta-theory such as Heyting arithmetic or related to be given a proper formal understanding.

The interpretation we gave to our operators is reflected in the set of axioms \(\mathsf{Base}\), which extends \(\mathsf{Int}\) with the additional justification axioms presented in the two left columns of Figure 3.

None

Figure 3: Intuitionistic justification axioms and rule.

While traditionally a set of axioms like \(\mathsf{Base}\) would generate a unique logic, justification logic allows for the definition of myriad logics via constant specifications.

Definition 4 (Constant specification). A constant specification for \(\mathsf{Base}\) is any subset \(\mathsf{CS}\subseteq \ifthenelse{\equal{[\mathtt{c}] A}{}} {\{\text{\mathtt{c} \in \mathsf{PrfConst} and A\in\mathsf{Base}^I}\}} {\{[\mathtt{c}] A \mid \text{\mathtt{c} \in \mathsf{PrfConst} and A\in\mathsf{Base}^I}\}}\). We call a constant specification \(\mathsf{CS}\) axiomatically appropriate* if for each axiom instance \(A\) of \(\mathsf{Base}\), there exists a proof constant \(\mathtt{c}\) such that \([\mathtt{c}] A \in \mathsf{CS}\). We call an axiomatically appropriate constant specification \(\mathsf{CS}\) schematic if for any instance \(A\) of an axiom in \(\mathsf{Base}^I\) we have that \([\mathtt{c}] A \in \mathsf{CS}\) entails \([\mathtt{c}] A' \in \mathsf{CS}\) for any instance \(A'\) of the same axiom.*

The parametricity in constant specifications of axiomatic systems for justification logics is illustrated by a characteristic rule of these calculi.

Definition 5. Given a constant specification \(\mathsf{CS}\) for \(\mathsf{Base}\), we define the logic \(\mathsf{JIK}_{\mathsf{CS}}\) as the set of consecutions \(\Gamma \vdash_{} A\) provable by the system described by the rules from Definition 1 (over \(\mathcal{L}_{\mathsf{J}}\)), where:

\(\mathsf{Mod}\) is replaced by \(\mathsf{Base}\) and
\(\hyperlink{rule:nec}{\mathsf{nec}}\) is replaced by the rule \(\hyperlink{rule:can}{\mathsf{can}}\) presented below. \[\hypertarget{rule:can}{ \inferLineSkip=3pt \infer[\hyperlink{rule:can}{\mathsf{can}}]{\Gamma\vdash [\mathtt{{!}^{\mathnormal{k}}\mathtt{c}}] \dots[\mathtt{{!}^{\mathnormal{}}\mathtt{c}}] [\mathtt{\mathtt{c}}] A} { [\mathtt{\mathtt{c}}] A \in \mathsf{CS} & k \geq 0}}\]

We adopt the conventions of Definition 1 with \(\vdash_{\mathsf{IK}}\) replaced by \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}}\).

The \({!}^{\mathnormal{}}\mathtt{}\) operator is not necessary to give a justification counterpart to non-transitive logics and we could opt for a formulation where \(\mathsf{CS}\subseteq \ifthenelse{\equal{[\mathtt{c_n}] [\mathtt{\dots}] [\mathtt{c_1}] A}{}} {\{\text{\mathtt{c_1}, \dots, \mathtt{c_n} \in \mathsf{PrfConst} and A\in\mathsf{Base}^I}\}} {\{[\mathtt{c_n}] [\mathtt{\dots}] [\mathtt{c_1}] A \mid \text{\mathtt{c_1}, \dots, \mathtt{c_n} \in \mathsf{PrfConst} and A\in\mathsf{Base}^I}\}}\) [@artemov_explicit_2001]. We prefer to use the explicit \({!}^{\mathnormal{}}\mathtt{}\) operator for a more concise presentation of \(\mathsf{CS}\) where proof constants can really be thought of as a witness to an axiom, and not to more complex formula of the form \({[\mathtt{c}] A}\).

The following is an example of a proof in \(\mathsf{JIK}_{\mathsf{CS}}\).

Example 1. We show that from \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A \mathbin{\to}(A \mathbin{\to}B) \mathbin{\to}B)~(1)\) one can infer \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{m} \rangle (A \mathbin{\to}B) \mathbin{\to}[\mathtt{s}] A \mathbin{\to}\langle \mathtt{\mathtt{(\mathtt{t} \mathbin{\cdot} \mathtt{s})} \mathbin{\star} \mathtt{m}} \rangle B\) for any proof term \(\mathtt{s}\) and satisfier term \(\mathtt{m}\). First, we instantiate \(\mathsf{{jk}_{1}}\) and \(\mathsf{{jk}_{2}}\) as follows: \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A \mathbin{\to}(A \mathbin{\to}B) \mathbin{\to}B) \mathbin{\to}[\mathtt{s}] A \mathbin{\to}[\mathtt{\mathtt{t} \mathbin{\cdot} \mathtt{s}}] ((A \mathbin{\to}B) \mathbin{\to}B))~(2)\) and \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{\mathtt{t} \mathbin{\cdot} \mathtt{s}}] ((A \mathbin{\to}B) \mathbin{\to}B)) \mathbin{\to}\langle \mathtt{m} \rangle (A \mathbin{\to}B) \mathbin{\to}\langle \mathtt{\mathtt{(\mathtt{t} \mathbin{\cdot} \mathtt{s})} \mathbin{\star} \mathtt{m}} \rangle B~(3)\). Second, we apply \(\hyperlink{rule:MP}{\mathsf{mp}}\) to (1) and (2) to obtain \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{s}] A \mathbin{\to}[\mathtt{\mathtt{t} \mathbin{\cdot} \mathtt{s}}] ((A \mathbin{\to}B) \mathbin{\to}B))~(4)\). Via transitivity of \(\mathbin{\to}\) on (3) and (4), we get \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{s}] A \mathbin{\to}\langle \mathtt{m} \rangle (A \mathbin{\to}B) \mathbin{\to}\langle \mathtt{\mathtt{(\mathtt{t} \mathbin{\cdot} \mathtt{s})} \mathbin{\star} \mathtt{m}} \rangle B~(5)\). Then by propositional reasoning on (5), we finally infer \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{m} \rangle (A \mathbin{\to}B) \mathbin{\to}[\mathtt{s}] A \mathbin{\to}\langle \mathtt{\mathtt{(\mathtt{t} \mathbin{\cdot} \mathtt{s})} \mathbin{\star} \mathtt{m}} \rangle B\). This is the justification version of the theorem \(\Diamond_{}(A \mathbin{\to}B) \mathbin{\to}\Box_{}A \mathbin{\to}\Diamond_{}B\) in \(\mathsf{IK}\).

2.3 Properties of Justification Logic↩︎

In this section, we recall key definitions and properties of justification logic needed throughout the paper.

Theorem 2 (Deduction Theorem). Let \(\Gamma\cup \ifthenelse{\equal{}{}} {\{A,B\}} {\{ \mid A,B\}}\subseteq\mathcal{L}_{\mathsf{J}}\). Then: \(\Gamma,A \vdash_{\mathsf{JIK}_{\mathsf{CS}}} B \iff \Gamma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A \mathbin{\to}B\)

Proof. This is a standard argument [@kuznets_logics_2019]: from right to left we simply use \(\hyperlink{rule:MP}{\mathsf{mp}}\) and monotonicity on the left of provability, and in the other direction we proceed by induction on the given proof of \(\Gamma,A \vdash_{\mathsf{JIK}_{\mathsf{CS}}} B\). ◻

Next, we show that \(\mathsf{JIK}_{\mathsf{CS}}\) is closed under a notion of substitution modifying proof and satisfier terms.

Definition 6 (Justification substitution). A (justification) substitution* is a pair of maps \(\sigma_t : \mathsf{PrfVar} \rightarrow \mathsf{PrfTm}\) and \(\sigma_s : \mathsf{SatVar} \rightarrow \mathsf{SatTm}\). For simplicity, we merge the two maps and write \(\sigma\) as a justification substitution. We define as expected the applications \(\mathtt{t} \sigma\), \(\mathtt{m} \sigma\) and \(A \sigma\) of \(\sigma\) to, respectively, the proof term \(\mathtt{t}\), the satisfier term \(\mathtt{m}\) and the formula \(A\). We write \(\Gamma \sigma\) to designate the set \(\{A \sigma\mid A\in\Gamma\}\).*

Lemma 1 (Substitution Lemma). Let \(\mathsf{CS}\) be a schematic constant specification, \(\Gamma\cup \ifthenelse{\equal{}{}} {\{A\}} {\{ \mid A\}}\subseteq\mathcal{L}_{\mathsf{J}}\), and \(\sigma\) a substitution. Then: \(\Gamma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A \implies \Gamma \sigma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A \sigma\)

Proof. The proof is similar to [@kuznets_logics_2019], and goes by induction on the structure of the proof of \(\Gamma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). The critical cases are when the last rule applied is \(\hyperlink{rule:ax}{\mathsf{ax}}\) or \(\hyperlink{rule:can}{\mathsf{can}}\). In the former case, it suffices to notice that if \(A\) is an instance of an axiom, then so is \(A \sigma\). In the latter case, we make use of the fact that \(\mathsf{CS}\) is schematic: with \([\mathtt{\mathtt{c}_{}}] A\in\mathsf{CS}\) and \([\mathtt{{!}^{\mathnormal{n}}\mathtt{\mathtt{c}_{}}}] \dots{[\mathtt{\mathtt{c}_{}}] A}\) appearing in our consecution, we obtain a proof of \(\Gamma \sigma \vdash_{} ([\mathtt{{!}^{\mathnormal{n}}\mathtt{\mathtt{c}_{}}}] \dots{[\mathtt{\mathtt{c}_{}}] A}) \sigma\) via \(\hyperlink{rule:can}{\mathsf{can}}\) by noticing that \(([\mathtt{{!}^{\mathnormal{n}}\mathtt{\mathtt{c}_{}}}] \dots{[\mathtt{\mathtt{c}_{}}] A}) \sigma = [\mathtt{{!}^{\mathnormal{n}}\mathtt{\mathtt{c}_{}}}] \dots{[\mathtt{\mathtt{c}_{}}] (A \sigma)}\) and that \([\mathtt{\mathtt{c}_{}}] A \sigma\in\mathsf{CS}\) as \(\mathsf{CS}\) is schematic. ◻

The next lemma expresses an interesting feature of justification logic: its (object) language allows for the reflection of its own (meta) proofs within formulas. On top of its conceptual interest, we leverage this lemma in many places throughout the paper.

Lemma 2 (Lifting Lemma). Let \(\mathsf{CS}\) be axiomatically appropriate. Let \(k \in \mathbb{N}\), \(\ifthenelse{\equal{}{}} {\{A_1, \dots, A_k, B, A\}} {\{ \mid A_1, \dots, A_k, B, A\}}\subseteq\mathcal{L}_{\mathsf{J}}\), \(\ifthenelse{\equal{}{}} {\{\mathtt{t}_1, \dots, \mathtt{t}_k\}} {\{ \mid \mathtt{t}_1, \dots, \mathtt{t}_k\}} \subseteq \mathsf{PrfTm}\) and \(\mathtt{m} \in \mathsf{SatTm}\). Then

If \(A_1, \dots, A_k \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\) then there exists a proof term \(\mathtt{t}\) s.t. \([\mathtt{\mathtt{t}_1}] A_1, \dots, [\mathtt{\mathtt{t}_k}] A_k \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{\mathtt{t}}] A\).
If \(A_1, \dots, A_k, B \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\) then there exists a satisfier term \(\mathtt{n}\) s.t. \([\mathtt{\mathtt{t}_1}] A_1, \dots, [\mathtt{\mathtt{t}_k}] A_k, \langle \mathtt{\mathtt{m}} \rangle B \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{\mathtt{n}} \rangle A\).

Proof. As in [@marin_justification_2025], we proceed by induction on the structure of the proof of \(A_1, \dots, A_k \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\), thereby inspecting the last rule applied. Our requirement that \(\mathsf{CS}\) is axiomatically appropriate shows in the base case when \(A\in\mathsf{Base}^{I}\): the existence of a constant \(\mathtt{c}\) such that \([\mathtt{c}] A \in \mathsf{CS}\) is ensured, thereby giving us \([\mathtt{\mathtt{t}_1}] A_1, \dots, [\mathtt{\mathtt{t}_k}] A_k \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{c}] A\) via \(\hyperlink{rule:can}{\mathsf{can}}\). We expand on the case for \(\hyperlink{rule:can}{\mathsf{can}}\), as the remaining cases are standard. In this case \(A = [\mathtt{{!}^{\mathnormal{l}}\mathtt{c}}] [\mathtt{\dots}] [\mathtt{{!}^{\mathnormal{}}\mathtt{c}}] [\mathtt{\mathtt{c}}] B\) for some proof constant \(\mathtt{c} \in \mathsf{PrfConst}\) and formula \(B\) with \([\mathtt{\mathtt{c}}] B \in \mathsf{CS}\). Instantiating \(\hyperlink{rule:can}{\mathsf{can}}\) one step further, we get \([\mathtt{\mathtt{t}_1}] A_1, \dots, [\mathtt{\mathtt{t}_k}] A_k \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{{!}^{\mathnormal{l+1}}\mathtt{c}}] [\mathtt{{!}^{\mathnormal{l}}\mathtt{c}}] [\mathtt{\dots}] [\mathtt{{!}^{\mathnormal{}}\mathtt{c}}] [\mathtt{\mathtt{c}}] B\) and hence \([\mathtt{\mathtt{t}_1}] A_1, \dots, [\mathtt{\mathtt{t}_k}] A_k \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{{!}^{\mathnormal{l+1}}\mathtt{c}}] A\). ◻

The proof of the above lemma informs us that the terms \(\mathtt{t}\) and \(\mathtt{n}\) we build are parametric in \(\mathtt{t}_1,\dots,\mathtt{t}_k\) and \(\mathtt{m}\). As a consequence, when \(k=0\) the first part of the lemma forces \(\mathtt{t}\) to be a ground term, i.e. a proof term which contains no proof or satisfier variable.

The technical lemma below generalises the axioms governing the operators \(\mathbin{+}\) and \(\mathbin{\sqcup}\), a useful tool in the completeness proof we provide later on.

Lemma 3. Let \(\mathsf{CS}\) be axiomatically appropriate. Let \(i,j \in \mathbb{N}\), \(\ifthenelse{\equal{}{}} {\{A_1, \dots, A_i, B_1, \dots, B_j\}} {\{ \mid A_1, \dots, A_i, B_1, \dots, B_j\}}\subseteq\mathcal{L}_{\mathsf{J}}\), \(\ifthenelse{\equal{}{}} {\{\mathtt{t}_1, \dots, \mathtt{t}_i\}} {\{ \mid \mathtt{t}_1, \dots, \mathtt{t}_i\}}\) \(\subseteq \mathsf{PrfTm}\) and \(\ifthenelse{\equal{}{}} {\{\mathtt{m}_1, \dots, \mathtt{m}_j\}} {\{ \mid \mathtt{m}_1, \dots, \mathtt{m}_j\}}\subseteq\mathsf{SatTm}\). Then there exists a proof term \(\mathtt{t}\) and a satisfier term \(\mathtt{m}\) such that:

\(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} ([\mathtt{\mathtt{t}_1}] A_1 \mathbin{\vee}\dots \mathbin{\vee}[\mathtt{\mathtt{t}_i}] A_i) \mathbin{\to}[\mathtt{\mathtt{t}}] (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_i)\)
\(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} (\langle \mathtt{\mathtt{m}_1} \rangle A_1 \mathbin{\vee}\dots \mathbin{\vee}\langle \mathtt{\mathtt{m}_j} \rangle A_j) \mathbin{\to}\langle \mathtt{\mathtt{m}} \rangle (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_j)\)

Proof. By the Lifting Lemma 2 and using the axioms \(\mathsf{j}{\mathtt{} \mathbin{+} \mathtt{}}_l\) and \(\mathsf{j}{\mathtt{} \mathbin{+} \mathtt{}}_r\) repetitively for the first statement, or \(\mathsf{j}{\mathtt{} \mathbin{\sqcup} \mathtt{}}_l\) and \(\mathsf{j}{\mathtt{} \mathbin{\sqcup} \mathtt{}}_r\) for the second statement. ◻

We now proceed to formalise the connection between \(\mathsf{JIK}_{\mathsf{CS}}\) and \(\mathsf{IK}\): in one direction, through translating their respective languages; in the other, by using realisation – this is the overarching goal of our paper.

Definition 7 (Forgetful projection). The forgetful projection* is a map \({(\cdot)}^{\mathsf{f}} : \mathcal{L}_{\mathsf{J}} \rightarrow \mathcal{L}_{\Box_{}}\) inductively defined below, where \(\ast \in \ifthenelse{\equal{}{}} {\{\mathbin{\wedge}, \mathbin{\vee}, \mathbin{\to}\}} {\{ \mid \mathbin{\wedge}, \mathbin{\vee}, \mathbin{\to}\}}\).*

\({\mathord{\mathord{\bot}}}^{\mathsf{f}} \colonequals \mathord{\mathord{\bot}}\)

\({p}^{\mathsf{f}} \colonequals p\)

\({(A \ast B)}^{\mathsf{f}} \colonequals ({A}^{\mathsf{f}} \ast {B}^{\mathsf{f}})\)

\({([\mathtt{\mathtt{t}}] A)}^{\mathsf{f}} \colonequals \Box_{}{A}^{\mathsf{f}}\)

\({(\langle \mathtt{\mathtt{m}} \rangle A)}^{\mathsf{f}} \colonequals \Diamond_{}{A}^{\mathsf{f}}\)

Theorem 3. Let \(A \in \mathcal{L}_{\mathsf{J}}\). If \(\Gamma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\) then \({\Gamma}^{\mathsf{f}} \vdash_{\mathsf{IK}} {A}^{\mathsf{f}}\).

Proof. This follows from the fact that the forgetful projection on axioms of \(\mathsf{JIK}_{\mathsf{CS}}\) and conclusions of the \(\hyperlink{rule:can}{\mathsf{can}}\) rule are theorems of \(\mathsf{IK}\). ◻

Corollary 2. \(\mathsf{JIK}_{\mathsf{CS}}\) is consistent.

Proof. Suppose \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \mathord{\mathord{\bot}}\). Then by Theorem 3, \(\vdash_{\mathsf{IK}} \mathord{\mathord{\bot}}\) which is a contradiction. ◻

The reverse direction is expressed via realisation maps.

Definition 8 (Realisation map). A realisation map* is a function \(r : \mathcal{L}_{\Box_{}} \rightarrow \mathcal{L}_{\mathsf{J}}\) such that \({r(G)}^{\mathsf{f}} = G\) for each \(G \in \mathcal{L}_{\Box_{}}\).*

In the remaining of the paper, we set ourselves to prove the next theorem.

Theorem 4 (Realisation Theorem). For schematic \(\mathsf{CS}\), there is a realisation map \(r\) such that: \[\forall G\in\mathcal{L}_{\Box_{}}.\;\;\; \vdash_{\mathsf{IK}} G \implies \vdash_{\mathsf{JIK}_{\mathsf{CS}}} r(G).\]

This realisation map is precisely what embeds the modal logic \(\mathsf{IK}\) into its corresponding justification logic \(\mathsf{JIK}_{\mathsf{CS}}\). The condition \({r(G)}^{\mathsf{f}} = G\) ensures that each \(\Box_{}\) (and each \(\Diamond_{}\)) occurring in \(G\) is replaced by exactly one proof term (and satisfier term, respectively). In other words, a realisation map takes a modal formula \(G\) into a justification formula with the same formula tree.

3 Basic Modular Models↩︎

Basic modular models were first introduced by Mkrtychev [@mkrtychev_models_1997] in a classical setting. These models can be seen as an extension of valuations for classical propositional logic, which assign a truth value to each proposition, with an additional interpretation on proof terms.

In the intuitionistic setting, Marti and Studer [@marti_intutionistic_2016] build basic modular models for an intuitionistic justification logic by instead enhancing the relational semantics for intuitionistic propositional logic. In this section, we extend these models with an interpretation on satisfier terms.

3.1 Definition and Soundness↩︎

For the definition of basic models for \(\mathsf{JIK}_{\mathsf{CS}}\), expanding upon the basic models given in [@marti_intutionistic_2016], we need the following operation on sets of formulas \(\primeset \mathtt{} \mathbin{\cdot} \mathtt{} \primeset[1] := \ifthenelse{\equal{B \in \mathcal{L}_{\mathsf{J}}}{}} {\{\text{A \mathbin{\to}B \in \primeset\text{ and }A \in \primeset[1]}\}} {\{B \in \mathcal{L}_{\mathsf{J}} \mid \text{A \mathbin{\to}B \in \primeset\text{ and }A \in \primeset[1]}\}}\).

Definition 9 (Basic model). A basic (intuitionistic modular) model* is a tuple \(\mathcal{B} = (W, \leq,*_\mathsf{Tm},*_\mathsf{Prop})\), where \(W\) is a non-empty set of worlds, \(\leq\) is a pre-order on \(W\), \(*_\mathsf{Prop} : \mathsf{Prop}\times W \rightarrow \ifthenelse{\equal{}{}} {\{0,1\}} {\{ \mid 0,1\}}\), and \(*_\mathsf{Tm} : (\mathsf{PrfTm}\cup\mathsf{SatTm}) \times W \rightarrow \mathcal{P}(\mathcal{L}_{\mathsf{J}})\).*

We abuse notation and combine \(*_\mathsf{Tm}\) and \(*_\mathsf{Prop}\) into a single function \(*\), making basic modular models tuples of the shape \((W, \leq,*)\). We also write \({\mathtt{s}}^{*}_{w}\) for \(*(\mathtt{s},w)\). In a basic modular model, the function \(*\) satisfies the following conditions on proof and satisfier terms:

1.	\(\mathtt{{\mathtt{s}}^{}_{\mathnormal{w}}} \mathbin{\cdot} \mathtt{{\mathtt{t}}^{}_{\mathnormal{w}}} \subseteq{(\mathtt{s} \mathbin{\cdot} \mathtt{t})}^{}_{w}\).*	5.	\(A \in {\mathtt{t}}^{}_{w}\) for any conclusion \([\mathtt{t}] A\) of \(\hyperlink{rule:can}{\mathsf{can}}\).*
2.	\(\mathtt{{\mathtt{s}}^{}_{\mathnormal{w}}} \mathbin{\cdot} \mathtt{{\mathtt{m}}^{}_{\mathnormal{w}}} \subseteq{(\mathtt{s} \mathbin{\star} \mathtt{m})}^{}_{\mathnormal{w}}\).*	6.	If \(A \mathbin{\vee}B \in {\mathtt{m}}^{}_{w}\) then \(A \in {\mathtt{m}}^{}_{w}\) or \(B \in {\mathtt{m}}^{}_{w}\).*
3.	\({\mathtt{s}}^{}_{w} \cup{\mathtt{t}}^{}_{w} \subseteq{(\mathtt{s} \mathbin{+} \mathtt{t})}^{}_{w}\).*	7.	If for all \(v \geq w\), \(A \notin {\mathtt{m}}^{}_{v}\) or \(B \in {\mathtt{t}}^{}_{v}\), then \(A \mathbin{\to}B \in{(\mathtt{\mathtt{m}} \mathbin{\triangleright} \mathtt{t})}^{}_{w}\).*
4.	\({\mathtt{m}}^{}_{w} \cup{\mathtt{n}}^{}_{w} \subseteq{(\mathtt{m} \mathbin{\sqcup} \mathtt{n})}^{}_{w}\).*	8.	\(\mathord{\mathord{\bot}}\notin {\mathtt{m}}^{}_{w}\).*

Definition 10 (Truth in a basic model). Given a basic model \(\mathcal{B}\), a point \(w\in W\) and a formula \(A\), we define the truth of \(A\) at \(w\) in \(\mathcal{B}\)* recursively on the structure of \(A\): \[\begin{array}{rcl} {\mathcal{B}} , w \Vdash p & \text{iff} & {p}^{*}_{w} = 1 \\ {\mathcal{B}} , w \Vdash\mathord{\mathord{\bot}} & & \text{never} \\ {\mathcal{B}} , w \Vdash A \mathbin{\wedge}B & \text{iff} & \text{{\mathcal{B}} , w \Vdash A and {\mathcal{B}} , w \Vdash B} \\ {\mathcal{B}} , w \Vdash A \mathbin{\vee}B & \text{iff} & \text{{\mathcal{B}} , w \Vdash A or {\mathcal{B}} , w \Vdash B} \\ {\mathcal{B}} , w \Vdash A \mathbin{\to}B & \text{iff} & \text{\forall v \geq w if {\mathcal{B}} , v \Vdash A then {\mathcal{B}} , v \Vdash B} \\ {\mathcal{B}} , w \Vdash[\mathtt{t}] A & \text{iff} & A \in {\mathtt{t}}^{*}_{w} \\ {\mathcal{B}} , w \Vdash\langle \mathtt{m} \rangle A & \text{iff} & A \in {\mathtt{m}}^{*}_{w} \\ \end{array}\] We write \(\vDash_\textsf{b}A\) if for any basic model \(\mathcal{B}\) and \(w \in W\) we have \({\mathcal{B}} , w \Vdash A\).*

The monotonicity conditions imposed on \(*\) port to the truth of formulas.

Lemma 4 (Monotonicity Lemma). Let \(\mathcal{B} = (W, \leq, *)\) be a basic modular model, \(w\) and \(v\in W\) such that \(w\leq v\), and \(A\) be a formula. Then: \({\mathcal{B}} , w \Vdash A \implies {\mathcal{B}} , v \Vdash A\).

Proof. We proceed by induction on \(A\). The base case \(A = p\) follows by the (M1) condition in Definition 9. The cases \(A = B \mathbin{\wedge}C, B \mathbin{\vee}C, B \mathbin{\to}C\) follow from a standard argument. When \(A = [\mathtt{\mathtt{t}}] B\), we get \(B \in {\mathtt{t}}^{*}_{w}\) by Definition 10. Then, using (M2) of Definition 9 we obtain \(B \in {\mathtt{t}}^{*}_{v}\) hence \({\mathcal{B}} , v \Vdash[\mathtt{\mathtt{t}}] B\). The case where \(A = \langle \mathtt{\mathtt{m}} \rangle B\) is similar. ◻

The soundness of \(\mathsf{JIK}_{\mathsf{CS}}\) with respect to its semantics on basic models can now be established.

Theorem 5 (Soundness). For any formula \(A\): \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A \implies \vDash_\textsf{b}{A}\).

Proof. By induction on the proof of \(A\) in \(\mathsf{JIK}_{\mathsf{CS}}\). Fix a basic model \({\mathcal{B}}\) and a world \(w \in W\). We show the validity of the new axioms and rules, and refer to [@marti_intutionistic_2016] for the remaining ones.

\(\mathsf{{jk}_{2}}: [\mathtt{s}] (A \mathbin{\to}B) \mathbin{\to}\langle \mathtt{m} \rangle A \mathbin{\to}\langle \mathtt{\mathtt{s} \mathbin{\star} \mathtt{m}} \rangle B\). Let \(v \geq w\) with \({\mathcal{B}} , v \Vdash[\mathtt{s}] (A \mathbin{\to}B)\) i.e. \(A \mathbin{\to}B \in {\mathtt{s}}^{*}_{v}\). Let \(u \geq v\) with \({\mathcal{B}} , u \Vdash\langle \mathtt{m} \rangle A\), i.e. \(A \in {\mathtt{m}}^{*}_{u}\). By the monotonicity property, \(A \mathbin{\to}B \in {\mathtt{s}}^{*}_{u}\). So \(B \in \mathtt{{\mathtt{s}}^{*}_{u}} \mathbin{\cdot} \mathtt{{\mathtt{m}}^{*}_{u}} \subseteq{(\mathtt{s} \mathbin{\star} \mathtt{m})}^{*}_{u}\) and hence \({\mathcal{B}} , u \Vdash\langle \mathtt{\mathtt{s} \mathbin{\star} \mathtt{m}} \rangle B\). Therefore by definition we have \({\mathcal{B}} , v \Vdash\langle \mathtt{m} \rangle A \mathbin{\to}[\mathtt{\mathtt{s} \mathbin{\star} \mathtt{m}}] B\) and hence \({\mathcal{B}} , w \Vdash[\mathtt{s}] (A \mathbin{\to}B) \mathbin{\to}\langle \mathtt{m} \rangle A \mathbin{\to}[\mathtt{\mathtt{s} \mathbin{\star} \mathtt{m}}] B\).
\(\mathsf{{jk}_{3}}: \langle \mathtt{m} \rangle (A \mathbin{\vee}B) \mathbin{\to}(\langle \mathtt{m} \rangle A \mathbin{\vee}\langle \mathtt{m} \rangle B)\). Let \(v \geq w\) with \({\mathcal{B}} , v \Vdash\langle \mathtt{m} \rangle (A \mathbin{\vee}B)\) i.e. \(A \mathbin{\vee}B \in {\mathtt{m}}^{*}_{v}\). By property 6 of Definition 9, \(A \in {\mathtt{m}}^{*}_{v}\) or \(B \in {\mathtt{m}}^{*}_{v}\). So \({\mathcal{B}} , v \Vdash\langle \mathtt{m} \rangle A\) or \({\mathcal{B}} , v \Vdash\langle \mathtt{m} \rangle B\), hence \({\mathcal{B}} , v \Vdash\langle \mathtt{m} \rangle A \mathbin{\vee}\langle \mathtt{m} \rangle B\). This gives \({\mathcal{B}} , w \Vdash\langle \mathtt{m} \rangle (A \mathbin{\vee}B) \mathbin{\to}(\langle \mathtt{m} \rangle A \mathbin{\vee}\langle \mathtt{m} \rangle B)\).
\(\mathsf{{jk}_{4}}: (\langle \mathtt{m} \rangle A \mathbin{\to}[\mathtt{t}] B) \mathbin{\to}[\mathtt{\mathtt{m} \mathbin{\triangleright} \mathtt{t}}] (A \mathbin{\to}B)\). Let \(v \geq w\) with \({\mathcal{B}} , v \Vdash\langle \mathtt{m} \rangle A \mathbin{\to}[\mathtt{t}] B\) i.e. for all \(u \geq v\), \(A \notin {\mathtt{m}}^{*}_{u}\) or \(B \in {\mathtt{t}}^{*}_{u}\). By property 7 of Definition 9, \(A \mathbin{\to}B \in {(\mathtt{m} \mathbin{\triangleright} \mathtt{t})}^{*}_{v}\). So \({\mathcal{B}} , v \Vdash[\mathtt{\mathtt{m} \mathbin{\triangleright} \mathtt{t}}] (A \mathbin{\to}B)\). Hence \({\mathcal{B}} , w \Vdash(\langle \mathtt{m} \rangle A \mathbin{\to}[\mathtt{t}] B) \mathbin{\to}[\mathtt{\mathtt{m} \mathbin{\triangleright} \mathtt{t}}] (A \mathbin{\to}B)\).
\(\mathsf{{jk}_{5}}: \langle \mathtt{m} \rangle \mathord{\mathord{\bot}} \mathbin{\to}\mathord{\mathord{\bot}}\). Let \(v \geq w\), by property 8 of Definition 9, we have \(\mathord{\mathord{\bot}}\notin {\mathtt{m}}^{*}_{v}\) and so \({\mathcal{B}} , v \not\Vdash\langle \mathtt{m} \rangle \mathord{\mathord{\bot}}\). Therefore, \({\mathcal{B}} , w \Vdash\langle \mathtt{m} \rangle \mathord{\mathord{\bot}} \mathbin{\to}\mathord{\mathord{\bot}}\).
\([\mathtt{{!}^{\mathnormal{n}}\mathtt{c}}] [\mathtt{{!}^{\mathnormal{n-1}}\mathtt{c}}] [\mathtt{\dots}] [\mathtt{{!}^{\mathnormal{}}\mathtt{c}}] [\mathtt{c}] A\) is a conclusion of \(\hyperlink{rule:can}{\mathsf{can}}\). Then, as \([\mathtt{{!}^{\mathnormal{n-1}}\mathtt{c}}] [\mathtt{\dots}] [\mathtt{{!}^{\mathnormal{}}\mathtt{c}}] [\mathtt{c}] A \in {({!}^{\mathnormal{n}}\mathtt{c})}^{*}_{w}\), we have that \({\mathcal{B}} , w \Vdash[\mathtt{{!}^{\mathnormal{n}}\mathtt{c}}] [\mathtt{{!}^{\mathnormal{n-1}}\mathtt{c}}] [\mathtt{\dots}] [\mathtt{{!}^{\mathnormal{}}\mathtt{c}}] [\mathtt{c}] A\).

◻

To show soundness, it is important that conditions 1-4 in Def. 9 are inclusions and not equalities. As for example, were they equalities, the formula \((\langle \mathtt{\mathtt{t} \mathbin{\star} \mathtt{m}} \rangle q \mathbin{\wedge}\langle \mathtt{m} \rangle p) \mathbin{\to}[\mathtt{t}] (p \mathbin{\to}q)\) would be valid. However, it is not a theorem of \(\mathsf{JIK}_{\mathsf{CS}}\) – otherwise, by Theorem 3 we would get \(\vdash_{\mathsf{IK}} (\Diamond_{}q \mathbin{\wedge}\Diamond_{}p) \mathbin{\to}\Box_{}(p \mathbin{\to}q )\) which is not true. We can build a countermodel \(\mathcal{B}\) to this formula meeting the inclusion-based conditions: \(W= \ifthenelse{\equal{}{}} {\{w\}} {\{ \mid w\}}, \leq= \ifthenelse{\equal{}{}} {\{(w,w)\}} {\{ \mid (w,w)\}}, {(\mathtt{t} \mathbin{\star} \mathtt{m})}^{*}_{w}= \ifthenelse{\equal{}{}} {\{q\}} {\{ \mid q\}}, {m}^{*}_{w} = \ifthenelse{\equal{}{}} {\{p\}} {\{ \mid p\}}, {t}^{*}_{w} = \emptyset\). Note that \({t}^{*}_{w} \mathtt{} \mathbin{\cdot} \mathtt{} {m}^{*}_{w} = \emptyset \subseteq{(\mathtt{t} \mathbin{\star} \mathtt{m})}^{*}_{w}\). We have \({\mathcal{B}} , w \Vdash\langle \mathtt{\mathtt{t} \mathbin{\star} \mathtt{m}} \rangle q \mathbin{\wedge}\langle \mathtt{m} \rangle p\) but \({\mathcal{B}} , w \not\Vdash[\mathtt{t}] (p \mathbin{\to}q)\), hence \({\mathcal{B}} , w \not\Vdash \langle \mathtt{(\mathtt{t} \mathbin{\star} \mathtt{m}} \rangle q \mathbin{\wedge}\langle \mathtt{m} \rangle p) \mathbin{\to}[\mathtt{t}] (p \mathbin{\to}q)\).

3.2 Completeness↩︎

In this section we prove the reverse direction of the last result, i.e. completeness.

Theorem 6 (Completeness). For any formula \(A\): \(\vDash_\textsf{b}{A} \implies \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\).

Our proof exploits the construction of a canonical model for intuitionistic justification logic. This syntactic structure uses prime sets as worlds.

Definition 11 (Prime Set). A prime set \(\primeset \subseteq\mathcal{L}_{\mathsf{J}}\) is a set of formulas satisfying the following:

**Deductive closure: if \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\) then \(A \in \primeset\).
**Primeness: if \(A \mathbin{\vee}B \in \primeset\) then \(A \in \primeset\) or \(B \in \primeset\).
**Consistency: \(\bot \notin \primeset\).

Let \(\primeset,\primeset[1] \subseteq\mathcal{L}_{\mathsf{J}}\). We write \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[1]\) if there is a finite set of formulas \(\ifthenelse{\equal{}{}} {\{A_1, \dots, A_n\}} {\{ \mid A_1, \dots, A_n\}}\subseteq\primeset[1]\) such that \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n\). We also write \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[1]\) when it does not hold that \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[1]\).

The completeness proof relies on projecting unprovable consecutions into the canonical model.

Lemma 5 (Prime Lemma). Let \(\primeset[0], \primeset[1] \subseteq\mathcal{L}_{\mathsf{J}}\). If \({\primeset[0]} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[1]\) then there exists a prime set \(\primeset' \supseteq\primeset[0]\) such that \(\primeset' \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[1]\). Furthermore, \(\primeset'\) is a maximal set (w.r.t. inclusion) satisfying these conditions.

Proof sketch. The proof goes via a standard argument: we exploit an enumeration of formulas to extend \(\Gamma\) step-by-step while ensuring that the extension does not entail \(\Delta\). The limit of this process can be shown to be a prime set \(\Gamma'\) not entailing \(\Delta\). The maximality of \(\Gamma'\) follows from the fact that if a formula could be added without entailing \(\Delta\), then it would indeed have been added when enumerated. ◻

Next, we define a structure which we show to be a basic (modular) model. To define parts of this structure, we use the sets of formulas \(\mathtt{t}^{-1}{\primeset} := \ifthenelse{\equal{A\in \mathcal{L}_{\mathsf{J}}}{}} {\{[\mathtt{\mathtt{t}}] A \in \primeset\}} {\{A\in \mathcal{L}_{\mathsf{J}} \mid [\mathtt{\mathtt{t}}] A \in \primeset\}}\) and \(\mathtt{m}^{-1}{\primeset} := \ifthenelse{\equal{A\in \mathcal{L}_{\mathsf{J}}}{}} {\{\langle \mathtt{\mathtt{m}} \rangle A \in \primeset\}} {\{A\in \mathcal{L}_{\mathsf{J}} \mid \langle \mathtt{\mathtt{m}} \rangle A \in \primeset\}}\).

Definition 12 (Canonical basic model). Let \(\mathcal{B}^c\) be the tuple \((W^c, \leq^c, *^c)\) where:

	\(W^c\colonequals \ifthenelse{\equal{\primeset}{}} {\{\text{\primeset is a prime set}\}} {\{\primeset \mid \text{\primeset is a prime set}\}}\);		\({\mathtt{t}}^{^c}_{\primeset} \colonequals \mathtt{t}^{-1}{\primeset}\);*
	\(\leq^c\colonequals \subseteq\);		\({\mathtt{m}}^{^c}_{\primeset} \colonequals \mathtt{m}^{-1}{\primeset}\).*
	\({p}^{^c}_{\primeset} = 1\) iff \(p \in \primeset\);*

\(\mathcal{B}^c\) is a basic model.

Proof. We are required to prove that this structure satisfies all the properties from Definition 9. As an example, we show that \(\mathtt{{s}^{*^c}_{\primeset}} \mathbin{\cdot} \mathtt{{t}^{*^c}_{\primeset}} \subseteq{(\mathtt{s} \mathbin{\cdot} \mathtt{t})}^{*^c}_{\primeset}\). Let \(B \in \mathtt{{s}^{*^c}_{\primeset}} \mathbin{\cdot} \mathtt{{t}^{*^c}_{\primeset}}\). By definition, there is a formula \(A\) such that \(A \mathbin{\to}B \in {s}^{*^c}_{\primeset}\) and \(A \in {t}^{*^c}_{\primeset}\). This means that \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{s}] (A \mathbin{\to}B)\) and \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] A\). Using the \(\mathsf{{jk}_{1}}\) axiom we get \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{\mathtt{s} \mathbin{\cdot} \mathtt{t}}] B\), hence \([\mathtt{\mathtt{s} \mathbin{\cdot} \mathtt{t}}] B \in \primeset\) by deductive closure. Therefore \(B \in \mathtt{(}\mathtt{s} \mathbin{\cdot} \mathtt{t})^{-1}{\primeset} = {(\mathtt{s} \mathbin{\cdot} \mathtt{t})}^{*^c}_{\primeset}\). ◻

Lemma 6 (Truth Lemma). Let \(A\) be a formula and \(\primeset\) be a prime set. Then: \(A \in \primeset \iff {\mathcal{B}^c} , \primeset \Vdash A\).

Proof. By induction on \(A\). All cases are covered in [@marti_intutionistic_2016], but the case for \(A = \langle \mathtt{\mathtt{m}} \rangle B\) which we show:

\(\langle \mathtt{\mathtt{m}} \rangle B \in \primeset\)	\(\iff\)	\(B \in \mathtt{m}^{-1}{\primeset}\) by definition of \(\mathtt{m}^{-1}{\primeset}\)
	\(\iff\)	\(B \in{\mathtt{m}}^{*^c}_{\primeset}\) by definition of the model \(\mathcal{B}^c\)
	\(\iff\)	\({\mathcal{B}^c} , \primeset \Vdash\langle \mathtt{\mathtt{m}} \rangle B\) by definition of truth in a basic model.

◻

With these results in hand, we can prove completeness.

Proof of Theorem 6. We prove the contrapositive. Suppose \(\not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). Then by the Prime Lemma 5, there exists a prime set \(\primeset\) such that \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). So \(A \notin \primeset\), and by the Truth Lemma 6 we have \({\mathcal{B}^c} , \primeset \not\Vdash A\). Finally, Proposition [prop:canbasmodmod] ensures that the \(\mathcal{B}^c\) belongs to the adequate class of models. ◻

4 Modular Models↩︎

In the classical setting, modular models [@artemov_ontology_2012] are epistemic models extending basic modular models with a modal accessibility relation to model the notion of knowledge. A key feature of these models is justification yields belief, which says that if a formula of the form \([\mathtt{t}] A\) holds at a world, then \(A\) must hold in all accessible worlds. This behaviour imitates that of the \(\Box_{}\) operator in modal logic and hence the feature promotes “backwards compatibility" from the justification logic to its corresponding modal logic.

In our setting, we must make several adaptations. First, satisfaction of a modal formula \(\Box_{}G\) is not defined locally, but globally along the intuitionistic pre-order, so the justification yields belief principle must account for this. Second, to deal with satisfiers we introduce satisfaction yield possibility, which says that if a formula of the form \(\langle \mathtt{m} \rangle A\) holds at a world, then \(A\) must hold in some accessible world. Finally, to promote “backwards compatibility", we have to ensure that the additional frame conditions of a birelational frame (Definition 2) [@fischer_servi_axiomatizations_1984] also hold.

4.1 Definition and Soundness↩︎

We define models for intuitionistic justification logic that bridge it with intuitionistic modal logic via the modal relation. To flesh out this connection, we make the interpretation of terms resonate with the modal relation by imposing conditions on the former using the latter and the notion of truth. To get there, we need to introduce preliminary structures on which we evaluate formulas.

Definition 13 (Intuitionistic quasi-model). An (intuitionistic) quasi-model is a tuple \(\mathcal{M}= (W, \leq, R, *)\) where \(\mathcal{B} = (W, \leq, *)\) is a basic model and \(R\) is a binary relation on \(W\).

Definition 14 (Truth in a quasi-model). For a quasi-model \(\mathcal{M}= (W, \leq, R, *)\), a point \(w\in W\) and a formula \(A\), we define the truth of \(A\) at \(w\) in \(\mathcal{M}\)* as: \({\mathcal{M}} , w \Vdash A\) iff \({\mathcal{B}} , w \Vdash A\) where \(\mathcal{B} = (W, \leq, *)\).*

As the notion of truth is the same in basic and quasi-models, the following obviously follows.

Lemma 7 (Monotonicity Lemma). Let \(\mathcal{M}= (W, \leq, R, *)\) be a quasi-model. Let \(w,v\in W\) such that \(w \leq v\). Let \(A\) be a formula. Then: \(\mathcal{M} , w \Vdash A \implies \mathcal{M} , v \Vdash A\)

Proof. By definition \(\mathcal{M} , w \Vdash A\) implies \({\mathcal{B}} , w \Vdash A\) where \(\mathcal{B} = (W, \leq, *)\). Using the Monotonicity Lemma 4 for basic modular models we get \({\mathcal{B}} , v \Vdash A\). By definition here again, we obtain \(\mathcal{M} , v \Vdash A\). ◻

Definition 14 exhibits the locality of truth [@marti_intutionistic_2016; @kuznets_logics_2019]. This notion in quasi-models helps us use these intermediate structures to bridge justification and modal logics: we obtain the adequate models by restricting the interpretation of terms by \(R\) and truth as shown in the next definition.

Definition 15 (Intuitionistic modular model). An (intuitionistic modular) model is a quasi-model \(\mathcal{M}= (W, \leq, R, *)\) such that \(\mathcal{M}_{\Box_{}} \colonequals (W, \leq, R, *_\mathsf{Prop})\) is a birelational intuitionistic model together with:

**Justification yields belief* (JYB) principle: for all proof terms \(\mathtt{t} \in \mathsf{PrfTm}\)*

\({\mathtt{t}}^{*}_{w} \subseteq\Box_{w} \colonequals \ifthenelse{\equal{A}{}} {\{\text{for all w', v' \in W with w \leq w' Rv', \mathcal{M} , v' \Vdash A}\}} {\{A \mid \text{for all w', v' \in W with w \leq w' Rv', \mathcal{M} , v' \Vdash A}\}}\)
**Satisfaction yields possibility* (SYP) principle: for all satisfiers \(\mathtt{m} \in \mathsf{SatTm}\)*

\({\mathtt{m}}^{*}_{w} \subseteq \Diamond_{w} \colonequals \ifthenelse{\equal{A}{}} {\{\text{there exists v \in W such that w Rv and \mathcal{M} , v \Vdash A}\}} {\{A \mid \text{there exists v \in W such that w Rv and \mathcal{M} , v \Vdash A}\}}\)

We write \(\vDash_\textsf{m}A\) if for any model \(\mathcal{M}\) and world \(w \in W\) we have \(\mathcal{M} , w \Vdash A\).

In contrast to the classical setting or other intuitionistic variants [@artemov_ontology_2012; @marti_intutionistic_2016; @pischke_intermediate_2023], the definition of (JYB) takes into account the global interpretation of \(\Box_{}\) via the pre-order \(\leq\).

Exploiting soundness with respect to basic models, the result follows for models.

Theorem 7 (Soundness of modular models). For any formula \(A\): \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A \implies \vDash_\textsf{m}{A}\).

Proof. Let \(\mathcal{M}= (W, \leq, R, *)\) be a modular model and \(w\) a world. Since \(\mathcal{B} = (W, \leq, *)\) is a basic modular model, we have \({\mathcal{B}} , w \Vdash A\) by Theorem 5. Hence, \(\mathcal{M} , w \Vdash A\) by Definition 15. ◻

The first epistemic models for classical justification logics were introduced by Fitting [@fitting_logic_2005]. These differ from Artemov’s modular models [@artemov_ontology_2012] on the definition of satisfaction for justification formulas of the form \([\mathtt{t}] A\). Fitting models additionally require \(A\) to hold in all modally accessible worlds, i.e., \(\mathcal{M} , w \Vdash[\mathtt{t}] A\) iff \(A \in {\mathtt{t}}^{*}_{w}\) and for all \(v \in W\) with \(w Rv\), \(\mathcal{M} , v \Vdash A\). In contrast, modular models make an ontological separation with the modal accessibility relation which plays no role on the satisfaction of formulas. Yet, both classes of models ensure “backwards compatibility" with modal logic [@kuznets_logics_2019]; in fact, they are equivalent [@kuznets_justifications_2012].

4.2 Completeness↩︎

We prove completeness w.r.t. the semantics on models, assuming that \(\mathsf{CS}\) is axiomatically appropriate.

Theorem 8 (Completeness). For any formula \(A\): \(\vDash_\textsf{m}{A} \implies \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\).

We construct once more a canonical model using the basic canonical model from Definition 12 as a basis. In essence, we aim to show that an adequate modal relation can be grafted onto this basic model.

We first need to define, for a given \(\Gamma\subseteq\mathcal{L}_{\mathsf{J}}\), certain sets of formulas: \(\hashprime[0] \colonequals \ifthenelse{\equal{A}{}} {\{\text{ for some } \mathtt{t} \in \mathsf{PrfTm},\,[\mathtt{t}] A \in \primeset[0] \}} {\{A \mid \text{ for some } \mathtt{t} \in \mathsf{PrfTm},\,[\mathtt{t}] A \in \primeset[0] \}}\) and \(\flatprime[0] \colonequals \ifthenelse{\equal{A}{}} {\{\text{for all } \mathtt{m} \in \mathsf{SatTm},\,\langle \mathtt{m} \rangle A \notin \primeset[0]\}} {\{A \mid \text{for all } \mathtt{m} \in \mathsf{SatTm},\,\langle \mathtt{m} \rangle A \notin \primeset[0]\}}\).

Definition 16 (Canonical intuitionistic modular model). Let \(\mathcal{M}^c\) be the tuple \((W^c, \leq^c, R^c, *^c)\) where \(\mathcal{B}^c = (W^c, \leq^c, *^c)\) is the canonical basic model, and \(\primeset[0] R^c\primeset[1]\) is defined as: if \([\mathtt{\mathtt{t}}] A \in \Gamma\) then \(A\in \Delta\) and for each \(A \in \Delta\) there exists \(\langle \mathtt{\mathtt{m}} \rangle A \in \Gamma\).

It is immediate that \(\mathcal{M}^c\) is a quasi-model, as \(\mathcal{B}^c\) is a basic model by Proposition [prop:canbasmodmod]. Utilising the locality of truth, this allows us to directly prove the Truth Lemma for \(\mathcal{M}^c\).

Lemma 8 (Truth Lemma). Let \(A\) be a formula and \(\primeset\) be a prime set. Then: \(A \in \primeset \iff {\mathcal{M}^c} , \primeset \Vdash A\).

Proof. As \(\mathcal{B}^c\) is a basic model, we have \({\mathcal{M}^c} , \primeset \Vdash A \iff {\mathcal{B}^c} , \primeset \Vdash A \iff A \in \primeset\) by Lemma 6. ◻

The canonical model also displays the following strong properties which ensure all collections of formulas made true by the same satisfier \(\mathtt{m}\) (or false by the same proof term \(\mathtt{t}\)) must be in fact true (or false, respectively) at the same world.

Lemma 9. Let \(\primeset[2] \subseteq\mathcal{L}_{\mathsf{J}}\) and \(\primeset\in W^c\).

If for all \(\mathtt{t} \in \mathsf{PrfTm}\) and for all \(A_1, \dots, A_n \in \primeset[2]\), \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)\), then there are \(\primeset', \primeset[1]'\in W^c\) such that \(\primeset \subseteq\primeset' R^c\primeset[1]'\) and \({\primeset[1]'} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[2]\).
If for some \(\mathtt{m} \in\mathsf{SatTm}\) and for all \(A_1, \dots, A_n \in \primeset[2]\), \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{m} \rangle (A_1 \mathbin{\wedge}\dots \mathbin{\wedge}A_n)\), then there is \(\primeset[1]\in W^c\) such that \(\primeset R^c\primeset[1]\) and \({\primeset[1]} \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\) for all \(A\in\primeset[2]\).

Proof. 1. Let \(\tilde{\primeset[2]} = \ifthenelse{\equal{[\mathtt{t}] (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)}{}} {\{\text{\mathtt{t}\in \mathsf{PrfTm} and A_1, \dots, A_n \in \primeset[2]}\}} {\{[\mathtt{t}] (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n) \mid \text{\mathtt{t}\in \mathsf{PrfTm} and A_1, \dots, A_n \in \primeset[2]}\}}\). Since for all \(\mathtt{t}\in\mathsf{PrfTm}\) and \(A_1, \dots, A_n \in \primeset[2]\) we have \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)\), we can establish that \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \tilde{\primeset[2]}\). Indeed, the primeness of \(\Gamma\) informs us that if it entailed a finite disjunction of elements of \(\tilde{\primeset[2]}\) then it would entail one of its disjuncts. Then, by the Prime Lemma 5 we get a maximal prime set \(\primeset'\) with \(\primeset \subseteq\primeset'\) and \(\primeset' \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \tilde{\primeset[2]}\). We can then show that \(\primeset'^{\sharp} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[2]\). Otherwise, there would be \(C_1, \dots, C_m \in \primeset'^{\#}\) with each \([\mathtt{t_i}] C_i \in \primeset'\) and \(A_1, \dots, A_n \in \primeset[2]\) such that \(C_1, \dots, C_m \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n\), which by the Lifting Lemma 2 would give \(\primeset' \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)\) for some \(\mathtt{t} \in \mathsf{PrfTm}\). Then, we can apply the Prime Lemma 5 again on \(\primeset'^{\sharp} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[2]\) to construct a prime set \(\primeset[1]'\) with \(\primeset'^{\sharp} \subseteq\primeset[1]'\) and \({\primeset[1]'} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \primeset[2]\).

Finally we need to check that \(\primeset' R^c\primeset[1]'\). Since \(\primeset'^{\sharp} \subseteq\primeset[1]'\) by construction we have that if \([\mathtt{\mathtt{t}}] A \in \Gamma'\) then \(A\in \Delta'\), hence it is enough to show that for each \(A \in \Delta'\) there exists \(\langle \mathtt{\mathtt{m}} \rangle A \in \Gamma'\). For such \(A \in \Delta'\), suppose for a contradiction that for all \(\mathtt{m} \in \mathsf{SatTm}\), \(\langle \mathtt{m} \rangle A \notin \Gamma'\). Then, for all \(A_1, \dots, A_n \in \primeset[2]\) we have \(\primeset', \langle \mathtt{m} \rangle A \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)\) for each \(\mathtt{m}\) and \(\mathtt{t}\), otherwise using the Deduction Theorem 2 and \(\mathsf{{jk}_{4}}\) we would have \(\primeset' \vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{\mathtt{m} \mathbin{\triangleright} \mathtt{t}}] (A \mathbin{\to}(A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n))\) and hence \(A \mathbin{\to}(A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n) \in \Gamma'^{\#} \subseteq\Delta'\), so we could deduce from \(A \in \Delta'\) and primeness of \(\Delta'\) that \(A_i \in \Delta'\) for some \(i\le n\). However, we have \(\Gamma' \subsetneq \Gamma' \cup \ifthenelse{\equal{}{}} {\{\langle \mathtt{m} \rangle A\}} {\{ \mid \langle \mathtt{m} \rangle A\}}\) and so the Prime Lemma 5 would give a strictly larger prime set satisfying the same conditions as \(\Gamma'\), contradicting its maximality – a similar use of maximality to e.g. [@fischer_servi_axiomatizations_1984].

2. Let us fix \(\mathtt{m} \in\mathsf{SatTm}\) such that for all \(A_1, \dots, A_n \in \primeset[2]\), \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{m} \rangle (A_1 \mathbin{\wedge}\dots \mathbin{\wedge}A_n)\), hence by deductive closure of \(\primeset\), \(\langle \mathtt{m} \rangle (A_1 \mathbin{\wedge}\dots \mathbin{\wedge}A_n)\in\primeset\). We first show that \({\primeset[2] \cup\hashprime} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \flatprime\). Otherwise, there would be \(A_1, \dots, A_l \in \primeset[2]\), \(B_1, \dots, B_n \in \hashprime\) with \([\mathtt{t_i}] B_i \in \primeset\) for some \(\mathtt{t_i}\), and \(C_1, \dots, C_p \in \flatprime\) such that \(A_1, \dots, A_l, B_1, \dots, B_n \vdash_{\mathsf{JIK}_{\mathsf{CS}}} C_1 \mathbin{\vee}\dots \mathbin{\vee}C_p\), and therefore \(A_1 \mathbin{\wedge}\ldots \mathbin{\wedge}A_l, B_1, \dots, B_n \vdash_{\mathsf{JIK}_{\mathsf{CS}}} C_1 \mathbin{\vee}\dots \mathbin{\vee}C_p\). By the Lifting Lemma 2 this yields some \(\mathtt{n}\in\mathsf{SatTm}\) such that \(\langle \mathtt{m} \rangle (A_1 \mathbin{\wedge}\ldots \mathbin{\wedge}A_l), [\mathtt{t_1}] B_1, \dots, [\mathtt{t_n}] B_n \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{n} \rangle (C_1 \mathbin{\vee}\dots \mathbin{\vee}C_p)\), hence \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{n} \rangle (C_1 \mathbin{\vee}\dots \mathbin{\vee}C_p)\). Now, using the \(\mathsf{{jk}_{3}}\) axiom as well as the deductive closure and primeness of \(\primeset\), we get \(\langle \mathtt{\mathtt{n}} \rangle C_j\in\Gamma\) for some \(j\le p\), which contradicts \(C_j\in\flatprime\). Then, we can apply the Prime Lemma 5 on \({\primeset[2] \cup\hashprime} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \flatprime\) to get a prime set \(\primeset[1] \supseteq\primeset[2] \cup\hashprime\) with \({\primeset[1]} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \flatprime\). Finally, \(\primeset R^c\primeset[1]\) because as \(\primeset^{\sharp} \subseteq\primeset[1]\) by construction we have that if \([\mathtt{\mathtt{t}}] A \in \Gamma\) then \(A\in \Delta\), and as \({\primeset[1]} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \flatprime\) we have that for each \(A \in \Delta\) there must exist \(\langle \mathtt{\mathtt{m}} \rangle A \in \Gamma\). ◻

As our next step in showing that \(\mathcal{M}^c\) is an intuitionistic modular model, we show that \(\mathcal{M}^c_{\Box_{}}\) is an intuitionistic birelational model. We therefore proceed to establish the confluence properties.

Lemma 10 (Forwards and backwards confluence in \(\mathcal{M}^c\)). Let \(\primeset, \primeset', \primeset[1]\in W^c\).

If \(\primeset \subseteq\primeset'\) and \(\primeset R^c\primeset[1]\), then there exists \(\primeset[1]'\in W^c\) with \(\primeset[1] \subseteq\primeset[1]'\) and \(\primeset' R^c\primeset[1]'\).
If \(\primeset R^c\primeset[1] \subseteq\primeset[1]'\), then there exists \(\primeset'\in W^c\) with \(\primeset \subseteq\primeset' R^c\primeset[1]'\).

Proof. While our proof is similar to the one for modal birelational models for \(\mathsf{IK}\) in [@fischer_servi_axiomatizations_1984], there are some subtleties in handling the satisfier terms. We expand on this point in the remark below. ◻

The use of proof terms in classical justification logic is known to introduce some non-normal behaviours of the modality [@artemov_why_2011; @artemov_justification_2024].

Similarly, in the intuitionistic setting, the \(\mathsf{IK}\) theorem \(\Diamond_{}(G_1 \mathbin{\wedge}\dots \mathbin{\wedge}G_n) \mathbin{\to}(\Diamond_{}G_1 \mathbin{\wedge}\dots \mathbin{\wedge}\Diamond_{}G_n)\) does not distinguish the information the distinct diamonds are carrying. The justification version of this theorem, \(\langle \mathtt{m} \rangle (A_1 \mathbin{\wedge}\dots \mathbin{\wedge}A_n) \mathbin{\to}(\langle \mathtt{\mathtt{t_1} \mathbin{\star} \mathtt{m}} \rangle A_1 \mathbin{\wedge}\dots \mathbin{\wedge}\langle \mathtt{\mathtt{t_n} \mathbin{\star} \mathtt{m}} \rangle A_n)\) where \(\mathtt{m}\) is a satisfier variable and each \(\mathtt{t_i}\) is a ground term obtained by applying the Lifting Lemma 2 to \(\vdash_{\mathsf{IK}} (A_1 \mathbin{\wedge}\dots \mathbin{\wedge}A_n) \mathbin{\to}A_i\), is more constrained due to the specific structure of the \(\mathtt{} \mathbin{\star} \mathtt{}\)-satisfier terms on the right-hand-side.

We finally establish that \(\mathcal{M}^c\) is a modular model by proving that it obeys the JYB and SYP principles. Justification yields belief is already achieved from the definition of \(R^c\), following the lines of [@marti_intutionistic_2016].

Lemma 11 (JYB in \(\mathcal{M}^c\)). Let \(\mathtt{t}\in\mathsf{PrfTm}\) and \(\primeset\in W^c\). Then:

\(A\in{\mathtt{t}}^{*^c}_{\primeset} \implies\) for all \(\primeset',\primeset[1]'\in W^c\) such that \(\primeset \subseteq\primeset' R^c\primeset[1]'\) we have \({\mathcal{M}^c} , \primeset[1]' \Vdash A\).

Proof. Suppose \(A \in {\mathtt{t}}^{*^c}_{\primeset}\), then \([\mathtt{t}] A \in \primeset\) by Definition 12. So, for \(\primeset' \supseteq\primeset\) we have \([\mathtt{t}] A \in \primeset'\) too. Hence, for \(\primeset[1]'\) with \(\primeset' R^c\primeset[1]'\), we have \(A \in \primeset[1]'\) by Definition 16. By the Truth Lemma 8, we have \({\mathcal{M}^c} , \primeset[1]' \Vdash A\). ◻

The remaining principle of satisfaction yields possibility is slightly more involved, as shown below.

Lemma 12 (SYP in \(\mathcal{M}^c\)). Let \(\mathtt{m}\in\mathsf{SatTm}\) and \(\primeset\in W^c\). Then:

\(A \in {\mathtt{m}}^{*^c}_{\primeset} \implies\) there exists \(\primeset[1] \in W^c\) such that \(\primeset R^c\primeset[1]\) and \({\mathcal{M}^c} , \primeset[1] \Vdash A\).

Proof. Suppose \(A \in {\mathtt{m}}^{*^c}_{\primeset}\), then \(\langle \mathtt{\mathtt{m}} \rangle A \in \primeset\) by definition. So, \(\primeset \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{\mathtt{m}} \rangle A\). Therefore, by Lemma [lem:extdiaexist] there is \(\primeset[1]\in W^c\) with \(\primeset R^c\primeset[1]\) and \({\primeset[1]} \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). By deductive closure \(A \in \primeset[1]\) and apply the Truth Lemma 8 for \(\mathcal{M}^c\) to get \({\mathcal{M}^c} , \primeset[1] \Vdash A\). ◻

The next proposition reveals the nature of \(\mathcal{M}^c\) by gathering our results.

\(\mathcal{M}^c\) is an intuitionistic modular model.

Proof. First, \(\mathcal{M}^c\) is a quasi-model as \(\mathcal{B}^c\) is a basic model by Proposition [prop:canbasmodmod]. Then, Lemma 10 shows that forwards and backwards confluence hold in \(\mathcal{M}^c\). Finally, Lemma 11 and Lemma 12 respectively prove that the properties JYB and SYP are satisfied in \(\mathcal{M}^c\). ◻

With this in hand, completeness follows.

Proof of Theorem 8. We reason contrapositively and assume \(\not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). The Prime Lemma 5 informs us of the existence of a prime set \(\primeset\) such that \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). So \(A \notin \primeset\), which gives \({\mathcal{M}^c} , \primeset \not\Vdash A\) by the Truth Lemma 8. Finally, Proposition [prop:canmodmod] ensures that the \(\mathcal{M}^c\) belongs to the adequate class of models. ◻

5 Realisation↩︎

We recall that our goal is to prove the following.

1. For schematic \(\mathsf{CS}\), there is a realisation map \(r\) such that for all \(G\in\mathcal{L}_{\Box_{}}\): \[\vdash_{\mathsf{IK}} G \implies \vdash_{\mathsf{JIK}_{\mathsf{CS}}} r(G).\]

This realisation function is constructed methodically in two steps:

Firstly, we reason semantically that a theorem \(G\) of \(\mathsf{IK}\) can be pre-realised into a disjunction of justification formulas which have “roughly” the same structure as \(G\);
Secondly, we condense a pre-realisation into a realisation by syntactical reasoning and substitutions to remove the extraneous content.

Our goal is more specifically to define normal realisation map which differentiates modalities based on their polarity. Recall that a subformula of \(G\) is positive if its position in the formula tree of \(G\) is reached from the root by following the left branch of an implication an even number of times; and call it negative otherwise.

Definition 17 (Normal realisation). A realisation map \(r : \mathcal{L}_{\Box_{}} \rightarrow \mathcal{L}_{\mathsf{J}}\) is normal* if, for any \(G \in \mathcal{L}_{\Box_{}}\), its negative modal subformulas \(\Box_{}F\) (or \(\Diamond_{}F\)) are realised as \([\mathtt{\mathtt{x}}] B\) (or \(\langle \mathtt{\mathtt{a}} \rangle B\)) with \(\mathtt{x}\in\mathsf{PrfVar}\) (or \(\mathtt{a}\in\mathsf{SatVar}\), respectively) occurring in \(r(G)\) exactly once.*

The choice of a normal realisation ensures that no independent subformulas are unintensionally identified. For example, the \(\mathsf{IK}\)-theorem \((\Diamond_{}p \mathbin{\vee}\Diamond_{}q) \mathbin{\to}\Diamond_{}(p \mathbin{\vee}q)\) can be realised as \[(\langle \mathtt{a} \rangle p \mathbin{\vee}\langle \mathtt{a} \rangle q) \mathbin{\to}\langle \mathtt{\mathtt{\mathtt{t_1} \mathbin{\star} \mathtt{a}} \mathbin{\sqcup} \mathtt{\mathtt{t_2} \mathbin{\star} \mathtt{a}}} \rangle (p \mathbin{\vee}q) \quad\text{or}\quad (\langle \mathtt{a} \rangle p \mathbin{\vee}\langle \mathtt{b} \rangle q) \mathbin{\to}\langle \mathtt{\mathtt{\mathtt{t_1} \mathbin{\star} \mathtt{a}} \mathbin{\sqcup} \mathtt{\mathtt{t_2} \mathbin{\star} \mathtt{b}}} \rangle (p \mathbin{\vee}q)\] where \(\mathtt{t_1}\) and \(\mathtt{t_2}\) are ground terms obtained by applying the Lifting Lemma 2 to \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} p \mathbin{\to}(p \mathbin{\vee}q)\) and \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} q \mathbin{\to}(p \mathbin{\vee}q)\), respectively. But, the first instance cannot be the result of a normal realisation.

For this reason, we need to do some bookkeeping on \(\Box_{}\)s and \(\Diamond_{}\)s: depending on their (positive or negative) polarity, they will be replaced by a variable in \(\mathsf{PrfVar}\cup\mathsf{SatVar}\) or a compound term in \(\mathsf{PrfTm}\cup\mathsf{SatTm}\). So, we first annotate by natural numbers \(\Box_{}\)s and \(\Diamond_{}\)s in the modal logic formulas. Each annotation is unique. Formally:

Definition 18 (Annotated modal formulas). An annotated modal formula* is built up like a standard modal formula but instead of single modalities \(\Box_{}\) and \(\Diamond_{}\), there is an infinite family of indexed modalities \(\Box_{k}\) and \(\Diamond_{k}\), for \(k\in\mathbb{N}\). We assume that no index occurs more than once in any given annotated formula.*

Example 2. Given the modal formula \(\Box_{}\Diamond_{}G \mathbin{\to}\Box_{}(\Diamond_{}J \mathbin{\wedge}\Diamond_{}\Box_{}(H \mathbin{\vee}I))\), a possible annotated version is \(\Box_{1}\Diamond_{2} G \mathbin{\to}\Box_{3}(\Diamond_{4} J \mathbin{\wedge}\Diamond_{5} \Box_{6} (H \mathbin{\vee}I))\).

Additionally, we need to track the signs of modal formulas.

Definition 19 (Signed modal formulas). **Signed modal formulas* are annotated modal formulas assigned with a polarity \(\mathsf{T}\) or \(\mathsf{F}\). We denote this as \(\mathsf{T}{G}\) or \(\mathsf{F}{G}\). The set of signed formulas is \(\mathcal{L}_{\Box_{}}^\mathsf{ann}\).*

We stress that these annotations do not add semantic information: they are bookkeeping devices. Where it is clear, we do not distinguish between a modal formula and its annotated version.

5.1 Pre-realisation↩︎

In this subsection, we adapt the methodology of [@fitting_logic_2005; @kuznets_logics_2019; @pischke_intermediate_2023] and reason semantically on both the canonical model \(\mathcal{M}^c\) and its induced birelational intuitionistic model \(\mathcal{M}^c_{\Box_{}}\) (recall Definition 15) to pre-realise modal formulas.

Definition 20 (Pre-realiser). The pre-realiser* is a function \(\@undefined\cdot \@undefined : \mathcal{L}_{\Box_{}}^\mathsf{ann} \rightarrow \mathcal{P}(\mathcal{L}_{\mathsf{J}})\) defined as:*

Definition 21. A modal formula \(G\) is pre-realisable* in \(\mathsf{JIK}_{\mathsf{CS}}\) if \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \@undefined\mathsf{F}{G} \@undefined\), i.e., there exist some \(A_1, \dots, A_n \in \@undefined\mathsf{F}{G} \@undefined\) such that \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n\).*

The following is the key result of this subsection and corresponds to the first step of the realisation proof described above and provides an initial but imperfect connection between theorems of \(\mathsf{IK}\) and theorems of \(\mathsf{JIK}_{\mathsf{CS}}\). It leverages the semantic machinery developed up to now.

Theorem 9 (Pre-realisation). Let \(\mathsf{CS}\) be axiomatically appropriate. For \(G\in\mathcal{L}_{\Box_{}}\), if \(\vdash_{\mathsf{IK}} G\), then \(G\) is pre-realisable* in \(\mathsf{JIK}_{\mathsf{CS}}\).*

This is shown through the semantic connection between a pre-realiser and its modal formula which is understood in the following:

Theorem 10. For every annotated modal formula \(G\). For a prime set \(\primeset\).

If for all \(A \in \@undefined\mathsf{T}{G} \@undefined\) we have \(\mathcal{M}^c , \primeset \Vdash A\), then \(\mathcal{M}^c_{\Box_{}} , \primeset \Vdash G\).
If for all \(A \in \@undefined\mathsf{F}{G} \@undefined\) we have \(\mathcal{M}^c , \primeset \not\Vdash A\), then \(\mathcal{M}^c_{\Box_{}} , \primeset \not\Vdash G\).

Proof. We prove both simultaneously by induction on \(G\). The cases when \(G = p, H \mathbin{\wedge}I, H \mathbin{\vee}I, H \mathbin{\to}I\) follow the argument in [@pischke_intermediate_2023]. We extend the proof with an adapted case for \(\Box_{}\) and a new one for \(\Diamond_{}\).

If \(G = \Box_{n} H\) then \(A\in\@undefined\mathsf{T}{G} \@undefined\) is of the form \([\mathtt{x_n}] B\) for \(B\in\@undefined\mathsf{T}{H} \@undefined\) and \(A\in\@undefined\mathsf{F}{G} \@undefined\) is of the form \([\mathtt{t}] (B_1 \mathbin{\vee}\dots \mathbin{\vee}B_m)\) for \(B_1,\dots,B_m\in\@undefined\mathsf{F}{H} \@undefined\) and \(\mathtt{t}\in\mathsf{PrfTm}\).

Suppose for all \(A \in \@undefined\mathsf{T}{G} \@undefined\), \(\mathcal{M}^c , \primeset \Vdash A\), that is, for all \(B \in \@undefined\mathsf{T}{H} \@undefined\), \(\mathcal{M}^c , \primeset \Vdash[\mathtt{\mathtt{x_{\mathnormal{n}}}}] B\). So, \(B\in{\mathtt{x_{\mathnormal{n}}}}^{*^c}_{\primeset}\) and by Lemma 11, for all \(\primeset', \primeset[1]'\) with \(\primeset \subseteq\primeset' R^c\primeset[1]'\), \(\mathcal{M}^c , \primeset[1]' \Vdash B\). By (IH) on 1., \(\mathcal{M}^c_{\Box_{}} , \primeset[1]' \Vdash H\) and therefore \(\mathcal{M}^c_{\Box_{}} , \primeset \Vdash\Box_{n} H\).
Suppose for all \(A \in \@undefined\mathsf{F}{G} \@undefined\), \(\mathcal{M}^c , \primeset \not\Vdash A\), that is, for all \(B_1, \dots, B_m \in \@undefined\mathsf{F}{H} \@undefined\) and \(\mathtt{t} \in \mathsf{PrfTm}\), \(\mathcal{M}^c , \primeset \not\Vdash[\mathtt{t}] (B_1 \mathbin{\vee}\dots \mathbin{\vee}B_m)\). So by the Truth Lemma 8, \([\mathtt{t}] (B_1 \mathbin{\vee}\dots \mathbin{\vee}B_m)\notin\primeset\), hence \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (B_1 \mathbin{\vee}\dots \mathbin{\vee}B_m)\). By Lemma 9, there exist \(\primeset', \primeset[1]'\in W^c\) such that \(\primeset \subseteq\primeset' R^c\primeset[1]'\) and \({\primeset[1]'} \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \@undefined\mathsf{F}{H} \@undefined\). So for all \(B \in \@undefined\mathsf{F}{H} \@undefined\), \(B\notin\primeset[1]'\) and by the Truth Lemma 8 again, \(\mathcal{M}^c , \primeset[1]' \not\Vdash B\) . By (IH) on 2., \(\mathcal{M}^c_{\Box_{}} , \primeset[1]' \not\Vdash H\), hence \(\mathcal{M}^c_{\Box_{}} , \primeset \not\Vdash\Box_{n} H\).

If \(G = \Diamond_{n} H\) then \(A\in\@undefined\mathsf{T}{G} \@undefined\) is of the form \(\langle \mathtt{\mathtt{a_{\mathnormal{n}}}} \rangle (B_1 \mathbin{\wedge}\dots \mathbin{\wedge}B_m)\) for \(B_1,\dots,B_m\in\@undefined\mathsf{T}{H} \@undefined\), and \(A\in\@undefined\mathsf{F}{G} \@undefined\) is of the form \(\langle \mathtt{m} \rangle B\) for \(B\in\@undefined\mathsf{F}{H} \@undefined\) and \(\mathtt{m}\in\mathsf{SatTm}\).

Suppose for all \(A \in \@undefined\mathsf{T}{G} \@undefined\), \(\mathcal{M}^c , \primeset \Vdash A\), that is, for all \(B_1, \dots, B_m \in \@undefined\mathsf{T}{H} \@undefined\), \(\mathcal{M}^c , \primeset \Vdash\langle \mathtt{\mathtt{a_{\mathnormal{n}}}} \rangle (B_1 \mathbin{\wedge}\dots \mathbin{\wedge}B_n)\). By Lemma [lem:extdiaexist], there exists \(\primeset[1]\) with \(\primeset R^c\primeset[1]\) and \({\primeset[1]} \vdash_{\mathsf{JIK}_{\mathsf{CS}}} B\) for all \(B \in \@undefined\mathsf{T}{H} \@undefined\). By deductive closure \(B \in \primeset[1]\) and by the Truth Lemma 8 we get \({\mathcal{M}^c} , \primeset[1] \Vdash B\) for all \(B \in \@undefined\mathsf{T}{H} \@undefined\). Hence, by (IH) on 1., \(\mathcal{M}^c_{\Box_{}} , \primeset[1] \Vdash H\) and so \(\mathcal{M}^c_{\Box_{}} , \primeset \Vdash\Diamond_{n} H\).
Suppose for all \(A \in \@undefined\mathsf{F}{G} \@undefined\), \(\mathcal{M}^c , \primeset \not\Vdash A\), that is, for all \(B \in \@undefined\mathsf{F}{H} \@undefined\) and \(\mathtt{m} \in \mathsf{SatTm}\), \(\mathcal{M}^c , \primeset \not\Vdash\langle \mathtt{m} \rangle B\), and by the Truth Lemma 8, \(\langle \mathtt{\mathtt{m}} \rangle B \notin \primeset\). By definition of \(R^c\) (Definition 16), it means, for all \(\primeset[1]\in W^c\) with \(\primeset R^c\primeset[1]\), that \(B \notin \primeset[1]\), and by the Truth Lemma 8 again, \(\mathcal{M}^c , \primeset[1] \not\Vdash B\) for all \(B \in \@undefined\mathsf{F}{H} \@undefined\). Hence, by (IH) on 2., \(\mathcal{M}^c_{\Box_{}} , \primeset[1] \not\Vdash H\) and so \(\mathcal{M}^c_{\Box_{}} , \primeset \not\Vdash\Diamond_{n} H\).

◻

Now we can prove the Pre-realisation Theorem 9.

Proof of Theorem 9. Suppose \(G\) is not pre-realisable. Then \(\not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \@undefined\mathsf{F}{G} \@undefined\). By the Prime Lemma 5, there exists a prime set \(\primeset\) such that \(\primeset \not\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \@undefined\mathsf{F}{G} \@undefined\). Hence, for all \(A \in \@undefined\mathsf{F}{G} \@undefined\), \(A \notin\primeset\), so by the Truth Lemma 8, \(\mathcal{M}^c , \primeset \not\Vdash A\). By Theorem 10, \(\mathcal{M}^c_{\Box_{}} , \primeset \not\Vdash G\), so \(G\) is not a theorem of \(\mathsf{IK}\). ◻

5.2 From Pre-realisation to Realisation↩︎

This subsection performs the second step of the realisation proof sketched above. From any finite subset of pre-realisers for a given modal formula \(G\), through a process called condensing [@fitting_modal_2016] which syntactically removes the extra disjunctions and conjunctions, we construct a justification formula that potentially realises \(G\), i.e. respects its syntax but not necessarily its semantics. Eventually, the realisation map, will choose a valid justification formula from the set of potential realisers, guided by the Pre-realisation theorem 9 from the previous section.

Definition 22 (Potential realiser). The potential realiser* is a map \(\llbracket \cdot \rrbracket : \mathcal{L}_{\Box_{}}^\mathsf{ann} \rightarrow \mathcal{P}(\mathcal{L}_{\mathsf{J}})\) defined as:*

\(\begin{array}{c@{\colonequals}l@{\quad}c@{\colonequals}l} \llbracket \mathsf{T}{p} \rrbracket & \ifthenelse{\equal{}{}} {\{p\}} {\{ \mid p\}} & \llbracket \mathsf{F}{p} \rrbracket & \ifthenelse{\equal{}{}} {\{p\}} {\{ \mid p\}} \\ \llbracket \mathsf{T}{G \mathbin{\wedge}H} \rrbracket & \ifthenelse{\equal{A \mathbin{\wedge}B}{}} {\{A \in \llbracket \mathsf{T}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} {\{A \mathbin{\wedge}B \mid A \in \llbracket \mathsf{T}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} & \llbracket \mathsf{F}{G \mathbin{\wedge}H} \rrbracket & \ifthenelse{\equal{A \mathbin{\wedge}B}{}} {\{A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{F}{H} \rrbracket\}} {\{A \mathbin{\wedge}B \mid A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{F}{H} \rrbracket\}} \\ \llbracket \mathsf{T}{G \mathbin{\vee}H} \rrbracket & \ifthenelse{\equal{A \mathbin{\vee}B}{}} {\{A \in \llbracket \mathsf{T}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} {\{A \mathbin{\vee}B \mid A \in \llbracket \mathsf{T}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} & \llbracket \mathsf{F}{G \mathbin{\vee}H} \rrbracket & \ifthenelse{\equal{A \mathbin{\vee}B}{}} {\{A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{F}{H} \rrbracket\}} {\{A \mathbin{\vee}B \mid A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{F}{H} \rrbracket\}} \\ \llbracket \mathsf{T}{G \mathbin{\to}H} \rrbracket & \ifthenelse{\equal{A \mathbin{\to}B}{}} {\{A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} {\{A \mathbin{\to}B \mid A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} & \llbracket \mathsf{F}{G \mathbin{\to}H} \rrbracket & \ifthenelse{\equal{A \mathbin{\to}B}{}} {\{A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} {\{A \mathbin{\to}B \mid A \in \llbracket \mathsf{F}{G} \rrbracket, B \in \llbracket \mathsf{T}{H} \rrbracket\}} \\ \llbracket \mathsf{T}{\Box_{n} G} \rrbracket & \ifthenelse{\equal{[\mathtt{\mathtt{x_{\mathnormal{n}}}}] A}{}} {\{A \in \llbracket \mathsf{T}{G} \rrbracket\}} {\{[\mathtt{\mathtt{x_{\mathnormal{n}}}}] A \mid A \in \llbracket \mathsf{T}{G} \rrbracket\}} & \llbracket \mathsf{F}{\Box_{n} G} \rrbracket & \ifthenelse{\equal{[\mathtt{t}] A}{}} {\{A \in \llbracket \mathsf{F}{G} \rrbracket, \mathtt{t} \in \mathsf{PrfTm}\}} {\{[\mathtt{t}] A \mid A \in \llbracket \mathsf{F}{G} \rrbracket, \mathtt{t} \in \mathsf{PrfTm}\}} \\ \llbracket \mathsf{T}{\Diamond_{n} G} \rrbracket & \ifthenelse{\equal{\langle \mathtt{\mathtt{a_{\mathnormal{n}}}} \rangle A}{}} {\{A \in \llbracket \mathsf{T}{G} \rrbracket\}} {\{\langle \mathtt{\mathtt{a_{\mathnormal{n}}}} \rangle A \mid A \in \llbracket \mathsf{T}{G} \rrbracket\}} & \llbracket \mathsf{F}{\Diamond_{n} G} \rrbracket & \ifthenelse{\equal{\langle \mathtt{\mathtt{m}} \rangle A}{}} {\{A \in \llbracket \mathsf{F}{G} \rrbracket, \mathtt{m} \in \mathsf{SatTm}\}} {\{\langle \mathtt{\mathtt{m}} \rangle A \mid A \in \llbracket \mathsf{F}{G} \rrbracket, \mathtt{m} \in \mathsf{SatTm}\}} \end{array}\)

The idea is that a realisation function on a modal formula \(G\) would choose a suitable justification formula \(A \in \llbracket \mathsf{F}{G} \rrbracket\). The choice of a formula from \(\llbracket \mathsf{F}{G} \rrbracket\), rather than \(\llbracket \mathsf{T}{G} \rrbracket\), ensures that for any negative subformula of \(A \in \llbracket \mathsf{F}{G} \rrbracket\) of the shape \([\mathtt{t}] B\) (or \(\langle \mathtt{m} \rangle B\)), we have \(\mathtt{t} \in \mathsf{PrfVar}\) (or \(\mathtt{m} \in \mathsf{SatVar}\) respectively), which is required to reach a normal realisation. The difference in the definition of \(\llbracket \mathsf{F}{G \mathbin{\to}H} \rrbracket\), \(\llbracket F{\Box_{n} G} \rrbracket\) and \(\llbracket \mathsf{T}{\Diamond_{n} G} \rrbracket\) compared to the pre-realiser ensures the justification formula does not contain additional conjunctions and disjunctions and exactly matches the structure of the modal formula. More formally:

Let \(G\) be an annotated modal formula. Then for every \(A \in \llbracket \mathsf{T}{G} \rrbracket \cup\llbracket \mathsf{F}{G} \rrbracket\), \({A}^{\mathsf{f}} = G\), where \({(\cdot)}^{\mathsf{f}} : \mathcal{L}_{\mathsf{J}} \rightarrow \mathcal{L}_{\Box_{}}\) is the forgetful projection from Definition 7.

Proof. This is a routine proof by induction on \(G\). ◻

The pre-realiser from Definition 20 is converted into a potential realiser using substitutions and syntactic reasoning – this process is called condensing by Fitting [@fitting_modal_2016].

To construct adequate substitutions we use the following auxiliary definitions.

Definition 23 (No new variable condition). Let \(\sigma\) be a substitution. The domain* of \(\sigma\) is the set \(\text{dom}(\sigma) \colonequals \ifthenelse{\equal{\mathtt{x_{\mathnormal{}}}\in \mathsf{PrfVar}}{}} {\{\mathtt{x_{\mathnormal{}}} \sigma \neq \mathtt{x_{\mathnormal{}}}\}} {\{\mathtt{x_{\mathnormal{}}}\in \mathsf{PrfVar} \mid \mathtt{x_{\mathnormal{}}} \sigma \neq \mathtt{x_{\mathnormal{}}}\}} \cup \ifthenelse{\equal{\mathtt{a_{\mathnormal{}}}\in \mathsf{SatVar}}{}} {\{\mathtt{a_{\mathnormal{}}} \sigma \neq \mathtt{a_{\mathnormal{}}}\}} {\{\mathtt{a_{\mathnormal{}}}\in \mathsf{SatVar} \mid \mathtt{a_{\mathnormal{}}} \sigma \neq \mathtt{a_{\mathnormal{}}}\}}\).*

A substitution \(\sigma\) meets the no new variable condition* if for each variable \(\mathtt{x_{\mathnormal{}}}\in \text{dom}(\sigma)\) (or \(\mathtt{a_{\mathnormal{}}}\in \text{dom}(\sigma)\)), \(\mathtt{x_{\mathnormal{}}} \sigma\) (or \(\mathtt{a_{\mathnormal{}}} \sigma\)) contains no other variables than \(\mathtt{x_{\mathnormal{}}}\) (or \(\mathtt{a_{\mathnormal{}}}\)).*

Definition 24 (Lives on). Let \(G\) be an annotated modal formula and \(\sigma\) be a substitution. We say that \(\sigma\) lives on* \(G\) if for every \(\mathtt{x_{\mathnormal{k}}} \in \text{dom}(\sigma)\), \(\Box_{k}\) occurs in \(G\) and for every \(\mathtt{a_{\mathnormal{k}}} \in \text{dom}(\sigma)\), \(\Diamond_{k}\) occurs in \(G\).*

With these definitions in hand, we tackle the condensing theorem.

Theorem 11 (Condensing Theorem). Let \(G\in\mathcal{L}_{\Box_{}}^\mathsf{ann}\).

For each collection \(A_1, \dots, A_n \in \@undefined\mathsf{T}{G} \@undefined\), there exist \(A \in \llbracket \mathsf{T}{G} \rrbracket\) and \(\sigma\) that lives on \(G\) and meets the no new variable condition such that \(A \vdash_{\mathsf{JIK}_{\mathsf{CS}}} (A_1 \mathbin{\wedge}\dots \mathbin{\wedge}A_n) \sigma\).
For each collection \(A_1, \dots, A_n \in \@undefined\mathsf{F}{G} \@undefined\), there exist \(A \in \llbracket \mathsf{F}{G} \rrbracket\) and \(\sigma\) that lives on \(G\) and meets the no new variable condition such that \((A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n) \sigma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\).

Proof. We prove both simultaneously by induction on \(G\). Except for diamonds, all cases are covered by Pischke [@pischke_intermediate_2023]. So, we are left to consider the case when \(G = \Diamond_{k} H\).

1. Let \(\langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A_1^1 \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_1}^1), \dots, \langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A_1^m \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_m}^m) \in \@undefined\mathsf{T}{\Diamond_{k}H} \@undefined\) with \(A_1^1, \dots, A_{n_1}^1, \dots, A_1^m, \dots, A_{n_m}^m \in \@undefined\mathsf{T}{H} \@undefined\). By the inductive hypothesis, there exist \(A \in \llbracket \mathsf{T}{H} \rrbracket\) and \(\sigma\) living on \(H\) which meets the no new variable condition such that \(A \vdash_{\mathsf{JIK}_{\mathsf{CS}}} (A_1^1 \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_1}^1 \mathbin{\wedge}\dots \mathbin{\wedge}A_1^m \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_m}^m ) \sigma\). So, for each \(i \le m\), \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A \mathbin{\to}(A_1^i \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_i}^i) \sigma\). By the Lifting Lemma 2, there exist ground terms \(\mathtt{t}_1, \dots, \mathtt{t}_n \in \mathsf{PrfTm}\) such that \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t_i}] (A \mathbin{\to}(A_1^i \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_i}^i) \sigma)\). Set \(\mathtt{t} \colonequals \mathtt{t_1} \mathbin{+} \mathtt{\mathtt{\dots} \mathbin{+} \mathtt{t_m}}\) which is also a ground term, and by repetitive use of \(\mathsf{j}{\mathtt{} \mathbin{+} \mathtt{}}_l\) and \(\mathsf{j}{\mathtt{} \mathbin{+} \mathtt{}}_r\), we have \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A \mathbin{\to}(A_1^i \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_i}^i) \sigma)\) for all \(i \le m\).

Now, define \(\sigma'\) as \(\sigma'(\mathtt{a_{\mathnormal{k}}}) = \mathtt{t} \mathbin{\star} \mathtt{\mathtt{a_{\mathnormal{k}}}}\) and as the identity otherwise – note as \(\mathtt{t}\) is a ground term, \(\sigma'\) meets the no new variable condition. By the Substitution Lemma 1, Definition 6 and the fact that \(\mathtt{t}\) is a ground term, so \(\mathtt{t} \sigma' = \mathtt{t}\), we have \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} [\mathtt{t}] (A \sigma' \mathbin{\to}(A_1^i \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_i}^i) \sigma \sigma')\) for all \(i = 1, \dots, m\). Using the \(\mathsf{{jk}_{2}}\) axiom and \(\hyperlink{rule:MP}{\mathsf{mp}}\): \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle A \sigma' \mathbin{\to}\langle \mathtt{\mathtt{t} \mathbin{\star} \mathtt{\mathtt{a_{\mathnormal{k}}}}} \rangle (A_1^i \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_i}^i) \sigma \sigma'\). Which can be rewritten as \(\langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A \sigma') \vdash_{\mathsf{JIK}_{\mathsf{CS}}} (\langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A_1^i \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_i}^i)) \sigma \sigma'\) since \(\mathtt{a_{\mathnormal{k}}} \sigma \sigma'= \mathtt{a_{\mathnormal{k}}} \sigma' = \mathtt{t} \mathbin{\star} \mathtt{\mathtt{a_{\mathnormal{k}}}}\). Propositional reasoning gives \(\langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A \sigma') \vdash_{\mathsf{JIK}_{\mathsf{CS}}} (\langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A_1^1 \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_1}^1) \mathbin{\wedge}\dots \mathbin{\wedge}\langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A_1^m \mathbin{\wedge}\dots \mathbin{\wedge}A_{n_m}^m)) \sigma \sigma'\) where indeed \(\sigma\sigma'\) is a substitution which lives on \(\Diamond_{k} H\), meets the no new variable condition and \(\langle \mathtt{\mathtt{a_{\mathnormal{k}}}} \rangle (A \sigma') \in \llbracket \mathsf{T}{\Diamond_{k} H} \rrbracket\).

2. Let \(\langle \mathtt{\mathtt{m}_1} \rangle A_1, \dots, \langle \mathtt{\mathtt{m}_n} \rangle A_n \in \@undefined\mathsf{F}{\Diamond_{k} H} \@undefined\) with \(A_1, \dots, A_n \in \@undefined\mathsf{F}{H} \@undefined\) and \(\mathtt{m}_1, \dots, \mathtt{m}_n \in \mathsf{SatTm}\). By Proposition 3, there exists a satisfier \(\mathtt{m} \in \mathsf{SatTm}\) such that \((*)\) \(\langle \mathtt{\mathtt{m}_1} \rangle A_1 \mathbin{\vee}\dots \mathbin{\vee}\langle \mathtt{\mathtt{m}_n} \rangle A_n \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{\mathtt{m}} \rangle (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)\). By the inductive hypothesis, there exist \(A \in \llbracket \mathsf{F}{H} \rrbracket\) and \(\sigma\) that lives on \(H\) (and meets the no new variable condition) such that \((**)\) \((A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n) \sigma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). Note that by definition \(\sigma\) also lives on \(\Diamond_{k} H\) trivially. By the Substitution Lemma 1 applied to \((*)\), we have \((\langle \mathtt{\mathtt{m}_1} \rangle A_1 \mathbin{\vee}\dots \mathbin{\vee}\langle \mathtt{\mathtt{m}_n} \rangle A_n) \sigma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} (\langle \mathtt{\mathtt{m}} \rangle (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)) \sigma\). By the Lifting Lemma 2 applied to \((**)\), there exists \(\mathtt{n} \in \mathsf{SatTm}\) such that \(\langle \mathtt{\mathtt{m} \sigma} \rangle (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n) \sigma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{\mathtt{n}} \rangle A\), equivalently (by Definition 6) \((\langle \mathtt{\mathtt{m}} \rangle (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n)) \sigma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{\mathtt{n}} \rangle A\). Hence, \((\langle \mathtt{\mathtt{m}_1} \rangle A_1 \mathbin{\vee}\dots \mathbin{\vee}\langle \mathtt{\mathtt{m}_n} \rangle A_n) \sigma \vdash_{\mathsf{JIK}_{\mathsf{CS}}} \langle \mathtt{\mathtt{n}} \rangle A\) where indeed \(\langle \mathtt{\mathtt{n}} \rangle A\in\llbracket \mathsf{F}{\Diamond_{k}H} \rrbracket\) and \(\sigma\) is a substitution living on \(\Diamond_{n} H\) and meets the no new variable condition. ◻

Finally, our central Realisation Theorem falls as a corollary of the results harvested this far: from pre-realisers which are semantically justified by the Pre-realisation theorem 9 we extract potential realisers which are also syntactically designed through the Condensing theorem 11 to follow precisely the original structure of the modal formula.

Proof of Theorem 4. Suppose \(\vdash_{\mathsf{IK}} G\). By the Pre-realisation Theorem 9, there exist \(A_1, \dots, A_n \in \@undefined\mathsf{F}{G} \@undefined\) such that \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n\). By the Condensing Theorem 11, there exists \(A \in \llbracket \mathsf{F}{G} \rrbracket\) and a substitution \(\sigma\) such that \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n) \sigma \mathbin{\to}A\). By the Substitution Lemma 1, \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} (A_1 \mathbin{\vee}\dots \mathbin{\vee}A_n) \sigma\) and so by modus ponens \(\vdash_{\mathsf{JIK}_{\mathsf{CS}}} A\). Let \(r(G) \colonequals A\) and we have \({r(G)}^{\mathsf{f}} = G\) by Proposition [prop:prelforget]. ◻

6 Conclusion↩︎

We have presented basic modular and modular models for the justification counterparts to \(\mathsf{IK}\) which let us derive an alternative semantic proof of the realisation theorem from \(\mathsf{IK}\) to \(\mathsf{JIK}\). This method could be further adapted on the one hand to sublogics of \(\mathsf{IK}\) such as the constructive modal logic \(\mathsf{CK}\) and on the other to extensions of \(\mathsf{IK}\) such as the other logics in the modal \(\mathsf{IS5}\) cube by following in the classical case [@artemov_logic_1999; @rubtsova_evidence_2006; @fitting_realization_2011; @kuznets_justifications_2012; @goetschi_realization_2012; @borg_realization_2015], or the family of Geach/Scott-Lemmon logics [@fitting_modal_2016]. For example, the modal logic \(\mathsf{IS4}\) extends \(\mathsf{IK}\) with the following axioms.

\(\mathsf{t}_{\Box_{}}\)

\(\Box_{}G \mathbin{\to}G\)

\(\mathsf{t}_{\Diamond_{}}\)

\(G \mathbin{\to}\Diamond_{}G\)

\(\mathsf{4}_{\Box_{}}\)

\(\Box_{}G \mathbin{\to}\Box_{}\Box_{}G\)

\(\mathsf{4}_{\Diamond_{}}\)

\(\Diamond_{}\Diamond_{}G \mathbin{\to}\Diamond_{}G\)

Semantically, this means imposing \(R\) is reflexive and transitive in any model \((W, \leq, R,*)\). In the corresponding justification logic [@marin_justification_2025], we add the following axioms to \(\mathsf{Base}\).

\(\mathsf{jt}_{\Box_{}}\)

\([\mathtt{t}] A \mathbin{\to}A\)

\(\mathsf{jt}_{\Diamond_{}}\)

\(A \mathbin{\to}\langle \mathtt{m} \rangle A\)

\(\mathsf{j4}_{\Box_{}}\)

\([\mathtt{t}] A \mathbin{\to}[\mathtt{{!}^{\mathnormal{}}\mathtt{t}}] [\mathtt{t}] A\)

\(\mathsf{j4}_{\Diamond_{}}\)

\(\langle \mathtt{m} \rangle \langle \mathtt{n} \rangle A \mathbin{\to}\langle \mathtt{n} \rangle A\)

An adaptation to the basic modular models in Section 3 in line with models for the justification counterpart to \(\mathsf{S4}\) [@mkrtychev_models_1997; @artemov_ontology_2012], and imposing \(R\) is reflexive and transitive, should be sufficient. Similarly, we conjecture that one can find justification counterparts to the family of logics defined by extending \(\mathsf{IK}\) with \(\Diamond_{}^k \Box_{}^l G \mathbin{\to}\Box_{}^m \Diamond_{}^n G\) where \(k,l,m,n \in \mathbb{N}\), by using the frame conditions given in [@plotkin_framework_1986]. The challenge could be defining additional operations on proof terms and satisfier terms.

Regarding sublogics such as \(\mathsf{CK}\), the canonical model construction for modular models would need to be generalised to build over not only prime sets, but pairs of prime sets and segments following the methodology introduced by [@wijesekera_constructive_1990] and developed for all the logics between \(\mathsf{CK}\) and \(\mathsf{IK}\) by [@GroShiClo25].

Some variants of intuitionistic justification logic can be seen as extending the typed \(\lambda\)-calculus with reflective capabilities [@artemov_unified_2002]. Applications of intuitionistic justification logic could extend to \(\lambda\)-calculi and type theory [@bellin_extended_2001], and lead to more expressive modal \(\lambda\)-calculi, notably for type constructors corresponding to the \(\Diamond_{}\) modality [@valliappan2025lax].

The third author has been supported by the UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.↩︎

Intuitionistic Justification Logic, Semantically

Abstract

1 Introduction↩︎

2 Preliminaries↩︎

2.2 Intuitionistic Justification Logic↩︎

2.3 Properties of Justification Logic↩︎

3 Basic Modular Models↩︎

3.1 Definition and Soundness↩︎

3.2 Completeness↩︎

4 Modular Models↩︎

4.1 Definition and Soundness↩︎

4.2 Completeness↩︎

5 Realisation↩︎

5.1 Pre-realisation↩︎

5.2 From Pre-realisation to Realisation↩︎

6 Conclusion↩︎

Subjects

Updated on Academus

Intuitionistic Justification Logic, Semantically

Abstract

1 Introduction↩︎

2 Preliminaries↩︎

2.1 Intuitionistic Modal Logic↩︎

2.2 Intuitionistic Justification Logic↩︎

2.3 Properties of Justification Logic↩︎

2.4 From Modal to Justification – and back↩︎

3 Basic Modular Models↩︎

3.1 Definition and Soundness↩︎

3.2 Completeness↩︎

4 Modular Models↩︎

4.1 Definition and Soundness↩︎

4.2 Completeness↩︎

5 Realisation↩︎

5.1 Pre-realisation↩︎

5.2 From Pre-realisation to Realisation↩︎

6 Conclusion↩︎

Subjects

Updated on Academus