\section{Introduction}\label{section:Introduction}
\paragraph{Subject matter} The subject matter of this paper is
	normal modal logic of internalised monotonic interactive proofs, i.e.,\xspace
		a novel super-intuitionistic normal modal logic of
			internalised intuitionistic (and thus disjunctive and monotonic) interactive proofs (LIiP) as well as
		an existing classical normal modal logic of
			internalised classical monotonic (and thus non-disjunctive) interactive proofs (LiP) \cite{LiP,KramerICLA2013}.
(We abbreviate interactivity-related adjectives with lower-case letters.)
Recall from \cite{sep-logic-intuitionistic} that
	a super-intuitionistic propositional logic is
		any consistent collection of propositional formulas
			that contains all the axioms of Intuitionistic Propositional Logic (IL) and
			that is closed under \emph{modus ponens} and substitution of arbitrary formulas for proposition letters.
Note however that the \emph{language} of IL is a strict subset of the (propositionally modal) language of LIiP.

\paragraph{Goal} Our goal here is to produce LIiP axiomatically as well as semantically from LiP.
The process of constructing LIiP from LiP is presented for the sake of gaining insight into
	the semantic connection between intuitionistic and classical interactive proofs, respectively.
LIiP, the result of the construction, however is independent of LiP.
Further note that like in \cite{LiP}, \cite{LiiP,KramerICLA2013}, and \cite{LDiiP,KramerIMLA2013},
	we still understand interactive proofs as \emph{sufficient evidence} for
		intended resource-unbounded proof-checking agents (who are though unable to guess), and
			leave probabilistic and polynomial-time resource bounded agents
				for future work.
Finally note that
	we choose our meta-logic to be classical
		(singleton meta-universe or meta-world unicity, cf.\  Section~\ref{section:IL}).

\subsection{Motivation}
Our immediate motivation for LIiP is to complete
	the picture of
		our above-mentioned resource-unbounded propositional normal modal logics of
			interactive proofs with
					the missing variant of intuitionistic interactive proofs---see Table~\ref{table:picture}.
\begin{sidewaystable}
\centering
\caption{Proof-term properties}
\smallskip
\begin{tabular}{@{}|>{\bf}>{\centering}p{0.075\textwidth}|c|>{\centering}p{0.3\textwidth}|>{\centering}p{0.15\textwidth}|c|@{}}
	\cline{2-5}
	\multicolumn{1}{c|}{} &
		\bf classicality &
		\bf communality &
		\bf disjunctivity (constructivity) &
		\bf monotonicity \\
	\hline
	\rowcolor[gray]{0.75}
	LIiP &
		\textbf{\emph{intuitionistic}} &
		non-communal
			(\emph{communication-medium}\\ or \emph{-adversary} centred\\
				\cite[Chapter~16]{ComputerSecurity}) &
		\emph{disjunctive,} negation-\emph{in}complete &
		monotonic \\
	\hline
	LiP \textmd{\cite{LiP,KramerICLA2013}} &
		classical &
		common knowledge
			(security-infrastructure or \emph{meta}-modelling:
				clocks \cite[Chapter~16]{CryptographyEngineering},
				names \cite[Chapter~6]{SecurityEngineering},
				PKIs \cite[Chapter~18--20]{CryptographyEngineering}) &
		non-disjunctive, negation-\emph{in}complete &
		monotonic \\
	\hline
	LiiP
	\textmd{\cite{LiiP,KramerICLA2013}} &
		classical &
		common belief\\
			(security \emph{object}-models:
				access control
					\cite[Chapter~4]{SecurityEngineering},
					\cite[Chapter~5, 20]{ComputerSecurity};
				data-base security \cite[Chapter~9]{ComputerSecurity};
				communication protocols
					\cite[Chapter~3]{SecurityEngineering},
					\cite[Chapter~16]{ComputerSecurity},
					\cite[Chapter~13]{CryptographyEngineering}) &
		non-disjunctive, negation-\emph{in}complete &
		non-monotonic \\
	\hline
	LDiiP
	\textmd{\cite{LDiiP,KramerIMLA2013}} &
		classical &
		non-communal
			(\emph{arbitrary-single-agent centred:}
				\emph{network}-adversaries
					\cite[Chapter~21]{SecurityEngineering},
					\cite[Chapter~17]{ComputerSecurity};
				reference monitors \cite[Chapter~6]{ComputerSecurity}) &
		\emph{disjunctive,} \textbf{\emph{negation-complete}} &
		non-monotonic \\
	\hline
\end{tabular}
\label{table:picture}
\end{sidewaystable}
The overarching motivation for LIiP is to serve in
	an intuitionistic foundation of interactive computation.
See \cite{LiP} for a programmatic motivation.
Table~\ref{table:picture} displays characteristic properties of
	our interactive proofs as internalised in
		their respective resource-unbounded propositional normal modal logic together with
			typical applications in information security.
The logics themselves, in contrast to their internalised proof terms, except LIiP are classical, i.e.,\xspace
	monotonic and non-disjunctive (and thus negation-incomplete).
As a confirmation,
	notice that disjunctivity is a necessary but not sufficient condition for intuitionism.

We recall and explain all this logical terminology in the next subsections, and thereby
draw some inspiration from the quite different intuitionistic logic of
	intuitionistic non-interactive proofs \cite{LIPArtemov}\label{page:LIP:1} and
	from the informational views on modal and intuitionistic logic expressed in
		\cite{ModalLogicInformation,InformationIL}.

\subsubsection{Intuitionistic Logic (IL)}\label{section:IL}
\paragraph{Definition}
From \cite{sep-logic-intuitionistic},
			recall that
				Intuitionistic Propositional Logic (IL) can be succinctly described as
					Classical Propositional Logic without the Aristotelian law of excluded middle (LEM):
						$(A \vee \neg A)$, but with the law of contradiction
						$(\neg A \rightarrow (A \rightarrow B))$, and that
		intuitionistically, \emph{Reductio ad absurdum} only proves negative statements,
			since $(\neg\neg A\rightarrow A)$ does not hold in general.
(If it did, LEM would follow by \emph{modus ponens} from
	the intuitionistically provable $\neg\neg(A\lor\neg A)$.)
Semantically,
	IL (and LIiP) is perhaps best viewed as a modal logic \cite{KripkeSemanticsIL}
		(cf.\  Definition~\ref{definition:KripkeModel} and Table~\ref{table:SatisfactionRelation}).
Therein,
	\begin{itemize}
	\item the valuation function on atomic propositions is constrained to be
			monotonic with respect to a partial order on system states (possible worlds);\footnote{%
				Incidentally, this monotonicity makes intuitionistic logic incompatible with
					hybrid logic, whose
						nominals are atomic propositions true at a single state \cite{HybridLogics},
							at least in the basic case where
								the intuitionistic-logical universe of worlds coincides with
								the hybrid-logical one.
				For more complex cases, see for example the work of Torben Bra\"uner and Valeria de Paiva.}
	\item the positive intuitionistic connectives (conjunction, disjunction) are interpreted as
			their classical counterparts
				(which conserve the monotonicity of atomic propositions) on
					the current state;
	\item the negative intuitionistic connectives (negation, implication) are interpreted as
			their non-monotonic classical counterparts on
					\emph{the upset of} the current state \emph{with respect to
						the partial order}
							(and thus \emph{are made to} conserve the monotonicity of atomic propositions).\label{page:Monotonicity}
	\end{itemize}
Hence first,
	intuitionistic negation and implication can be viewed as
		classical negation and implication prefixed by a (unary) modality that is interpreted by
			a (binary) partial-order accessibility relation (e.g.,\xspace a temporal reachability relation),
				respectively; and
	second, intuitionistic facts, be they positive or negative, are necessarily
		monotonic (durable, forward invariant, lasting, persistent, stable) in the state space \cite{InformationIL}.\label{page:invariants}
(Intuitionistic double negation can be interpreted temporally as
	the forward invariant ``at some future time.'')
Plain classical logic is also but trivially monotonic, as
	it can be viewed as a modal logic over a singleton state space.
From this modal viewpoint,
	one immediately recognises why $(\neg\neg A\rightarrow A)$
	(``true at some future time implies true now'') is valid classically.

\paragraph{Properties}
In the previous paragraph,
	we saw that
		IL has the monotonicity property (``\emph{intuitionistic} implies \emph{monotonic}'').
IL has also the important disjunction property (``\emph{intuitionistic} implies \emph{disjunctive}'').
That is,
	any external intuitionistic notion of proof $\vdash_{I}$ has
		the property that
			$\vdash_{I} A\lor B$ implies $\vdash_{I} A$ or $\vdash_{I} B$.
Recall that
	disjunctivity is a necessary but not sufficient condition for intuitionism, and that
	plain classical notions of proof do not have the disjunction property.
Now note that when internalised in an object-logical language,
	\begin{itemize}
		\item an external intuitionistic notion of proof, say $\vdash_{I_{1}}$, becomes
			a unary necessity modality, say $[M]$,
				parametrised with a proof term $M\,;$
		\item the disjunction property of $\vdash_{I_{1}}$ becomes
				a disjunctive property of
					the internalising external notion of proof, say $\vdash_{I_{2}}$, that
						$\vdash_{I_{2}}[M](\phi\lor\phi')\rightarrow([M]\phi\lor[M]\phi')\,;$
		\item the monotonicity property becomes
				the similar property that
					$\vdash_{I_{2}}[M]\phi\rightarrow[(M,M')]\phi$, where
						$(M,M')$ is the term pair constructed from $M$ and $M'$ with
							$M'$ representing the additional data allowed by the monotonicity.
	\end{itemize}
Further note that
	a normal modal logic that internalises an intuitionistic notion of proof is necessarily intuitionistic itself:
		assume that
			the external notion of proof, say $\vdash$, is classical, i.e.,\xspace $\vdash\phi\lor\neg\phi$, and
			deduce $\vdash[M](\phi\lor\neg\phi)$ by the normal-modal rule schema of necessitation that
				$\vdash \phi$ implies $\vdash[M]\phi\,.$
So the internalised notion of proof $[M]$ is classical too.
Even a non-normal modal logic like \cite{LIPArtemov}\label{page:LIP:2} must be intuitionistic itself in order to
		be able to internalise an intuitionistic notion of proof, because
			already \cite{LIPArtemov}'s weaker form of necessitation---that
				$\vdash_{\text{ILP}} F$ implies that
				\emph{there is a} proof term $t$ such that
					$\vdash_{\text{ILP}} t:F$---forces external intuitionism.
Finally note that
	IL is algorithmically decidable \cite{ILcomplexity}.

\subsubsection{Negation-complete logics}
\paragraph{Definition}
Recall that
	a notion of proof, say $\vdash_{1}$, is \emph{negation-complete} by definition if and only if
		$\vdash_{1}A$ or $\vdash_{1}\neg A$.
When internalised in an object language with an external notion of proof, say $\vdash_{2}$,
	negation completeness becomes
		$\vdash_{2}[M]\phi\lor[M]\neg\phi$.
Though conveniently classical (LEM),
	negation-complete logics have also
		the property of having constructive and computational content.

\paragraph{Properties}
From the detailed reminder in Section~1.1.1 of \cite{LDiiP,KramerIMLA2013},
	recall that
		first,
			the negation-completeness property implies
				the discussed disjunction property (``\emph{negation-complete} implies \emph{disjunctive}'');
		second, any internalised negation-complete notion of proof $\vdash_{2}$ is non-monotonic, that is,
				$\vdash_{2}[M]\phi\lor[M]\neg\phi$ implies
				$\not\vdash_{2}[M]\phi\rightarrow[(M,M')]\phi$
					(``\emph{negation-complete} implies \emph{non-monotonic}'');
		third, negation completeness and intuitionism are incompatible properties; and
		fourth, negation completeness implies algorithmic decidability.

\subsubsection{Communality}
In LDiiP, LiiP, LiP, and LIiP,
	our so-far \emph{ad hoc} modal notation $[M]\phi$ becomes
				$\decides{M}{}{a}{}\phi\,,$
				$\proves{M}{}{a}{\mathcal{C}}\phi\,,$
				$\pproves{M}{}{a}{\mathcal{C}}\phi\,,$ and
				$\Iproves{M}{}{\mathtt{CM}}{}\phi\,,$ respectively, where
					$a$ and $\mathcal{C}$ is an additional parameter for
						a peer-reviewing agent $a$
							(such as the as-an-agent-imagined communication medium $\mathtt{CM}$) and
						a finite agent-community $\mathcal{C}$ of peers, respectively.
The intended meaning of these modalities is
	``$M$ can classically and disjunctively but only non-monotonically prove to $a$ that $\phi$ [is true],''
	``$M$ can classically and non-monotonically prove to $a$ that $\phi$ and
		this fact is common belief in $\mathcal{C}\cup\set{a}$,''
	``$M$ can classically and monotonically prove to $a$ that $\phi$ and
		this fact is common knowledge in $\mathcal{C}\cup\set{a}$,'' and
	``$M$ can intuitionistically (and thus disjunctively and monotonically) prove to $\mathtt{CM}$ that $\phi$,'' respectively.
(Recall from
	\cite{Epistemic_Logic,MultiAgents},
		that knowledge implies belief.)
In all these logics,
	the proof potential is such that
		if my peer reviewer knew my proof
		then she would know that its proof goal is true.
Notice that
	what is accepted as a potential proof $M$
		may depend on a community $\mathcal{C}\cup\set{a}$ of peers if and only if
			the proof is non-disjunctive.
This is the (non-)communality of $M$ mentioned in Table~\ref{table:picture}.

\subsection{Contribution}\label{section:Contribution}
Our contribution in this paper is five-fold:
\begin{enumerate}
	\item We produce the intuitionistic Logic of Intuitionistic interactive Proofs (LIiP)
		(cf.\  Theorem~\ref{theorem:Adequacy}) from its classical counter-part LiP.
		%
		LIiP internalises necessarily \emph{communication-medium-centred}
			(or \emph{communication-adversary-centred})\footnote{
										In communication security,
											the communication medium is usually
												assumed adversarial (as an agent) and
												called Eve (the eavesdropper).} intuitionistic proof theories,
			enjoying the disjunction property.
		%

		%
		As notable \emph{\textbf{syntactic} novelties} in intuitionistic modal logic,
			LIiP provides:
			\begin{enumerate}
				\item a non-primitive
					\begin{enumerate}
						\item possibility modality that
				is \emph{doubly macro-definable} within the language of LIiP:
					in terms of double negation and
					\begin{enumerate}
						\item communication-medium knowledge (cf.\  Page~\pageref{page:PossibilityModality}),
						\item its corresponding primitive necessity modality
					(though \emph{not} in the classical modal terms $\Diamond\phi\leftrightarrow\neg\Box\neg\phi$, cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.58);
					\end{enumerate}
						\item necessitation rule that
								is derivable from
									the primitive modal monotonicity axiom schema $\phi\rightarrow\Box\phi$ and
									the primitive \emph{modus ponens} deduction rule
										(cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.0);
					\end{enumerate}
				\item the two insights that in interactive settings,
					\begin{enumerate}
						\item the intuitionistic truths are those of the communication medium
								(cf.\  Remark~\ref{remark:IntuitionisticTruths}),
						\item intuitionistic proofs induce perfect and thus disjunctive knowledge
								in the communication medium, and only in that
									(cf.\  Remark~\ref{remark:PerfectKnowledge}).
					\end{enumerate}
			\end{enumerate}
			That is, we put forward
				\emph{LIiP as a modal-logical characterisation of
						the concept of message-passing communication medium.}
	\item We provide a standard but also oracle-computational and set-theoretically constructive Kripke-semantics for LIiP
		(cf.\  Section~\ref{section:Semantically}):
		\begin{itemize}
	\item Like in \cite{LiiP,KramerICLA2013} and \cite{LDiiP,KramerIMLA2013},
		we endow the proof modality with a standard Kripke-semantics \cite{ModalLogicSemanticPerspective}, but first define its
			accessibility relation $\access{M}{\mathtt{CM}}{}$
				constructively in terms of
					elementary set-theoretic constructions,\footnote{in loose analogy with
							the set-theoretically constructive rather than
							the purely axiomatic definition of
								numbers \cite{TheNumberSystems} or
								ordered pairs (e.g.,\xspace the now standard definition by Kuratowski,
									and other well-known definitions \cite{NotesOnSetTheory})}
							namely as $\pAccess{M}{\mathtt{CM}}{}$ (cf.\  Section~\ref{section:Concretely}),
				and then match it to an abstract semantic interface in standard form (which
					abstractly stipulates the characteristic properties of the accessibility relation
						\cite{ModalProofTheory}).
	%
	We will say that $\pAccess{M}{\mathtt{CM}}{}$ \emph{exemplifies}
		(or \emph{realises}) $\access{M}{\mathtt{CM}}{}$ (cf.\  Section~\ref{section:Abstractly}).
	%
	(A simple example of a set-theoretically constructive but non-intuitionistic definition of a modal accessibility is
		the well-known definition of epistemic accessibility as
			state indistinguishability defined in terms of
				equality of state-projection functions \cite{Epistemic_Logic}.)

	\item 	Our Kripke-semantics is oracle-computational in the sense that
		the individual proof knowledge (say $M$) can be thought of as being provided by
			a computation oracle (cf.\  Definition~\ref{definition:SemanticIngredients}), which thus acts as a
				hypothetical provider and imaginary epistemic source of our interactive proofs.
	\end{itemize}
	As notable \emph{\textbf{semantic} novelties} in intuitionistic modal logic,
		LIiP is:
		\begin{enumerate}
			\item \emph{doubly constructive:}
			LIiP is an intuitionistic (and thus constructive) logic and additionally
			offers a set-theoretically constructive Kripke-semantics in the form of
				the concrete accessibility relation $\pAccess{M}{\mathtt{CM}}{}\,;$
			\item \emph{parametrically mono-relational:}
			We may freely choose between
				the abstract accessibility $\access{M}{\mathtt{CM}}{}$ and
				its concrete exemplification (or realisation) $\pAccess{M}{\mathtt{CM}}{}$ as
					the accessibility relation in
						LIiP's Kripke-semantics, but
							$\pAccess{\mathtt{CM}}{\mathtt{CM}}{}$ has also the property of
								being a partial order with
									$\mathtt{CM}$ designating the communication medium.
		%
		Hence LIiP's essentially mono-relational models subsume
			seminal bi-relational models of intuitionistic modal logics \cite[Page~59]{PhDThesisSimpson}
				by absorbing the partial order $\pAccess{\mathtt{CM}}{\mathtt{CM}}{}$ for the Kripke-semantics of LIiP's intuitionistic connectives
					as a mere instance of the accessibility relation $\pAccess{M}{\mathtt{CM}}{}$ for the Kripke-semantics of LIiP's proof modality\label{page:PartialOrder},
						thanks to being parametric (and thus generic).
		\end{enumerate}
	\item We prove a \emph{modal-depth result} applying both to
			LIiP's necessity as well as
			its corresponding possibility modality (cf.\  Corollary~\ref{corollary:ModalDepth}).
	\item We prove that
		our CM-centred notion of proof is also
			a \emph{disjunctive explicit} refinement of standard KD45-belief, and yields also such
			a refinement of standard S5-knowledge and S4-provability
				(cf.\  Corollary~\ref{corollary:DEB} and \ref{corollary:DEP}).
	\item We prove
		the \emph{finite-model property} (cf.\  Theorem~\ref{theorem:FiniteModelProperty}) and therefrom
		the \emph{algorithmic decidability} of LIiP (cf.\   Corollary~\ref{corollary:AlgorithmicDecidability}).
\end{enumerate}
As a side-effect of our work on LIiP,
			we offer an internalised,
				three-line two-axiom proof of
					the Disjunction Property of
						Intuitionistic Logic (IL)
							originally proved by G\"odel.
			%
			The two axioms
				are modal internalisations of two fundamental properties of IL, namely
					the truthfulness of its proofs and
					Kripke's Monotonicity Lemma for his semantics of IL.
			%
			Surprisingly,
				they jointly
					trivialise the corresponding box modality `$\Box$' (though \emph{not} the one of LIiP) in a technical sense, and thus also,
						in a non-technical sense,
							G\"odel's (non-trivial) proof of IL's Disjunction Property.
			%
			The truthfulness of intuitionistic proofs corresponds to
				the well-known modal T-law $\Box\phi\rightarrow\phi$ and
			Kripke's Monotonicity Lemma to
				the law $\phi\rightarrow\Box\phi$
				(not to be confused with the mentioned monotonicity of proof terms,
					cf.\  Page~\pageref{page:Monotonicity} and Remark~\ref{remark:Monotonicity}).
			%
			Jointly,
				they imply $\Box(\phi\lor\varphi)\rightarrow(\Box\phi\lor\Box\varphi)$ in any modal logic:
				\begin{enumerate}
					\item $\vdash\Box(\phi\lor\varphi)\rightarrow(\phi\lor\varphi)$\hfill T
					\item $\vdash(\phi\lor\varphi)\rightarrow(\Box\phi\lor\Box\varphi)$\hfill
							$\vdash\phi\rightarrow\Box\phi$,
							$\vdash\varphi\rightarrow\Box\varphi$, IL
					\item $\vdash\Box(\phi\lor\varphi)\rightarrow(\Box\phi\lor\Box\varphi)$\hfill 1, 2, IL.
				\end{enumerate}

\subsection{Roadmap}
In the next section,
	we introduce our Logic of Intuitionistic interactive Proofs (LIiP) axiomatically by means of
		a compact closure operator that induces the Hilbert-style proof system that we seek.
We then prove
	a substantial number of useful, deducible structural and logical laws
		(cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleStructuralLaws} and
						\ref{theorem:SomeUsefulDeducibleLogicalLaws}) within the obtained system, and
	therefrom important corollaries
		(Corollary~\ref{corollary:Combinator}--\ref{corollary:DEP}), some of which
			count as our aforementioned contributions in this paper.
Next, we
	introduce the concretely constructed semantics
	as well as the standard abstract semantic interface for LIiP (cf.\  Section~\ref{section:Semantically}), and
	prove the axiomatic adequacy of the proof system with respect to this interface
		(cf.\  Theorem~\ref{theorem:Adequacy}).
In the construction of the semantics, we again make use of a closure operator, but
	this time on sets of proof terms.
Finally,
	we prove
		the finite-model property
			(cf.\  Theorem~\ref{theorem:FiniteModelProperty}) and
		the algorithmic decidability
			(cf.\  Corollary~\ref{corollary:AlgorithmicDecidability}) of LDiiP.

\section{LIiP}
\subsection{Syntactically}
The Logic of Intuitionistic interactive Proofs (LIiP) provides
	a modal \emph{formula language} over a generic message \emph{term language}.
The formula language offers
		the propositional constructors,
		a relational symbol
			`$\knows{}{}$'
			for constructing atomic propositions about
				so-called individual knowledge (e.g.,\xspace $\knows{a}{M}$), and
		a modal constructor `$\Iproves{}{}{}{}$' for propositions about proofs
			(e.g.,\xspace $\Iproves{M}{\phi}{\mathtt{CM}}{}$).
The message language
	offers a term constructor for message \emph{pairing} and
	can accommodate arbitrary other term constructors, e.g.,\xspace for cryptography (cf.\  \cite{LiP}).
The single term constructor of pairing is sufficient for
	internalising \emph{modus ponens} into the message language
		(cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.1) and
			thus for internalising the single deduction rule of intuitionistic logic into it.
\emph{Modus ponens} can be regarded as a minimal requirement for a system to count as a proof system.
And so in the context of LIiP,
	all other term constructors can be regarded as application-specific, and
		LIiP-theories with such constructors as applied LIiP-theories.
These however are not the subject matter of our present paper about basic (or pure) LIiP.
(Message signing has no essential role in LIiP as opposed to LiP.)
In brief, LIiP is a minimal modular extension of IL with an
interactively generalised
	additional operator
	(the proof modality) and
	proof-term language (only one, binary built-in constructor; \emph{agents as proof-checkers}).
Alternatively,
	LIiP can be viewed as a refinement (due to its parameterised modality) and extension (due to additional laws) of
			Fischer Servi's \cite{IK:FischerServi} or, equivalently,
			Plotkin and Stirling's \cite{IK:PlotkinStirling}
		basic intuitionistic modal logic IK,
			promoted in \cite{PhDThesisSimpson} as ``the true intuitionistic analogue of K.''
See \cite{BasicConstructiveModality} for a recent
	discussion of this purported truth and
	alternative contribution in the form of the so-called basic constructive modal logic CK, which
		can be embedded into IK \cite{CKembeddedIntoIK}.
Note that the formula language of LIiP is identical to the one of LiP \cite{LiP}
	modulo
	the term language and
	the proof-modality notation.
The term language of LIiP is strictly included in the term language of LiP but may be arbitrarily extended.
The proof-modality notation in LIiP is `$\Iproves{}{}{}{}$' whereas it is `$\pproves{}{}{}{}$' in LiP.

In the sequel, grey-shading indicates essential differences to LiP.
\begin{definition}[The language of LIiP]\label{definition:LIiPLanguage}
	Let
	\begin{itemize}
		\item $\mathcal{A}$ designate a finite set of
			\emph{agent names} $a$, $b$, $c$, etc.\xspace \colorbox[gray]{0.75}{such that $\mathtt{CM}\in\mathcal{A}$,}
				where $\mathtt{CM}$ designates the communication medium
					(admissible also in LiP);
		\item $\mathcal{M} \ni M \mathrel{::=} a \ \big| \  B \ \big| \  \pair{M}{M}$
			designate our language of
				\emph{message terms} $M$ \emph{over} $\mathcal{A}$ with
				(transmittable) agent names $a\in\mathcal{A}$,
				application-specific data $B$ (left blank here), and
				message-term pairs $\pair{M}{M}\,;$

			(Messages must be grammatically well-formed, which
				yields an induction principle.
				So agent names $a$ are logical term constants,
				the meta-variable $B$ just signals the possibility of an extended term language $\mathcal{M}$, and
				$\pair{\cdot}{\cdot}$ is a binary functional symbol.
				For other term constructors, see \cite{LiP}.)
		\item $\mathcal{P}$ designate a denumerable set of \emph{propositional variables} $P$ constrained such that
			for all $a\in\mathcal{A}$ and $M\in\mathcal{M}$,
				$(\knows{a}{M})\in\mathcal{P}$
					(for ``$a$ knows $M$'')
					is a distinguished variable, i.e.,\xspace
						an \emph{atomic proposition},
							(for \emph{individual} knowledge);
			%
			(So, for $a\in\mathcal{A}$, $\knows{a}{\cdot}$
				is a unary relational symbol.)
		\item $\mathcal{L}\ni\phi \mathrel{::=} P \ \big| \
				\phi\land\phi \ \big| \
				\phi\lor\phi \ \big| \
				\neg\phi \ \big| \
				\phi\rightarrow\phi \ \big| \
				\colorbox[gray]{0.75}{$\Iproves{M}{\phi}{\mathtt{CM}}{}$}$
				designate our language of \emph{logical formulas} $\phi$, where
					the modal-necessity formula $\Iproves{M}{\phi}{\mathtt{CM}}{}$ reads as
					``$M$ can intuitionistically prove that $\phi$ (is true) to $\mathtt{CM}$.''
	\end{itemize}
\end{definition}
\noindent
Note the following macro-definitions:
	$\text{true} \mathrel{:=} \knows{\mathtt{CM}}{\mathtt{CM}}$,
	$\text{false} \mathrel{:=} \neg \text{true}$,
	$\phi \leftrightarrow \phi' \mathrel{:=} (\phi \rightarrow \phi') \land (\phi' \rightarrow \phi)$,
	\colorbox[gray]{0.75}{$\blacksquare\phi\mathrel{:=}\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}$}
		(see also Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.8),
	$\Diamond\phi\mathrel{:=}\neg\neg\phi$, and
	\colorbox[gray]{0.75}{$\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}\mathrel{:=}\Diamond(\knows{\mathtt{CM}}{M}\land\phi)$}
		(\emph{double negation as modal possibility} rather than necessity, unlike in
		\cite{IntuitionisticDoubleNegationAsNecessity}\label{page:PossibilityModality};
			see also Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.58).
Recall that
	whereas
		conjunction and disjunction connectives as well as
		necessitation and possibility modalities
			are dually inter-definable in classical modal logic by means of negation,
				they are not necessarily so in intuitionistic modal logic
					\cite[Requirement~5]{PhDThesisSimpson}.
However,
	as our above macro-definition of $\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$ in terms of a double negation and individual knowledge foreshadows,
		$\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$ fortunately is not necessary as a primitive modality in the language of LIiP.
(\cite{LIPArtemov}\label{page:LIP:4} remain silent as to the dual of their intuitionistic-proof modality.)

Then, LIiP has the following axiom and deduction-rule schemas.
\begin{definition}[The axioms and deduction rules of LIiP]\label{definition:AxiomsRules}
Let
	\begin{itemize}
		\item $\Gamma_{0}$ designate an adequate set of axioms for \colorbox[gray]{0.75}{intuitionistic} propositional logic
		\item $\Gamma_{1} \mathrel{:=} \Gamma_{0} \cup \{$
			\begin{itemize}
				\item $\knows{a}{a}$\quad(knowledge of one's own name string)
				\item $(\knows{a}{M}\land\knows{a}{M'})\leftrightarrow\knows{a}{\pair{M}{M'}}$\quad([un]pairing)
				\item $\Iproves{M}{\knows{\mathtt{CM}}{M}}{\mathtt{CM}}{}$\quad(self-knowledge)
				\item $(\Iproves{M}{(\phi\rightarrow\phi')}{\mathtt{CM}}{})\rightarrow
				((\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{})$%
				\quad(K)
				\item $(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow(\knows{\mathtt{CM}}{M}\rightarrow\phi)$\quad(epistemic T, ET)
				\item \colorbox[gray]{0.75}{$
							(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}
						\text{\quad(intuitionistic D, ID)}$}%
				\item \colorbox[gray]{0.75}{$\phi\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$
						\quad(modal monotonicity, MM)}
				\}
			\end{itemize}
			 %
			designate a set of \emph{axiom schemas.}
	\end{itemize}
	Then, $\colorbox[gray]{0.75}{$\mathrm{LIiP}\mathrel{:=}\Clo{}{}(\emptyset)$}\mathrel{:=}\bigcup_{n\in\mathbb{N}}\Clo{}{n}(\emptyset)$, where
		for all $\Gamma\subseteq\mathcal{L}:$
		\begin{eqnarray*}
					\Clo{}{0}(\Gamma) &\mathrel{:=}& \Gamma_{1}\cup\Gamma\\
					\Clo{}{n+1}(\Gamma) &\mathrel{:=}&
						\begin{array}[t]{@{}l@{}}
							\Clo{}{n}(\Gamma)\ \cup\\
							\setst{\phi'}{\set{\phi,\phi\rightarrow\phi'}\subseteq\Clo{}{n}(\Gamma)}\cup
								\quad\text{(\emph{modus ponens}, MP)}\\

							\setst{(\Iproves{M'}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}}{(\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'})\in\Clo{}{n}(\Gamma)}\\
							\quad\text{(epistemic antitonicity, EA)}.\label{page:EpistemicAntitonicity}
						\end{array}
				\end{eqnarray*}

		We call $\mathrm{LIiP}$ a \emph{base theory,} and
		$\Clo{}{}(\Gamma)$ an \emph{LIiP-theory} for any $\Gamma\subseteq\mathcal{L}$.
\end{definition}
\noindent
Notice the
	logical order of LIiP, which like LiP's is,
		due to propositions about (proofs of) propositions, \emph{higher-order propositional}.
\paragraph{Inherited laws}
From LiP \cite{LiP},
	we recall the discussion of
		the (un)pairing axiom,
		Kripke's law (K),
		the laws of
			epistemic T (ET) and

			epistemic antitonicity (EA):
We assume the existence of a pairing mechanism modelling finite sets.
Such a mechanism is required by the important application of
	communication (not only cryptographic) protocols \cite[Chapter~3]{SecurityEngineering}, in which
		concatenation of high-level data packets is associative, commutative, and idempotent.
The key to the validity of K is that
	we understand interactive proofs as sufficient evidence for
		intended resource-unbounded proof-checking agents (who are though still unable to guess).
Clearly for such agents,
	if
		$M$ is sufficient evidence for $\phi\rightarrow\phi'$ and $\phi$
	then so is $M$ for $\phi'$.
Then, the significance of ET
	(which as opposed to the standard T-law is conditioned on individual knowledge) to interactivity is that
	in truly distributed multi-agent systems,
		not all proofs are known by all agents, i.e.,\xspace
			agents are not omniscient with respect to messages.
Otherwise, why communicate with each other?
So there being a proof does not imply knowledge of that proof.
When an agent $a$ does not know the proof and
the agent cannot generate the proof \emph{ex nihilo} herself by guessing it,
only communication from a peer, who thus acts as an oracle, can entail the knowledge of the proof with $a$.
Finally,
	note that
		the law of self-knowledge is a theorem but not an axiom in LiP, and
	observe that EA is a rule of \emph{logical modularity} that
			allows the modular generation of structural modal laws from
				implication term laws
					(cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleStructuralLaws}).

\paragraph{New laws} We continue to discuss the new laws of LIiP, which are all axiom schemas:
In contrast to LiP \cite{LiP},
	LIiP must have an \emph{intuitionistic} rather than a classical propositional axiom base $\Gamma_{0}$ as
		already explained at the end of Section~\ref{section:IL}.
Next, ID says that intuitionistic necessity (``box'') implies intuitionistic possibility (``diamond'').
As opposed to its classical-modal-logic equivalent D,
	ID cannot be alternatively stated in the shape of
		$\vdash\Box\phi\rightarrow\neg\Box\neg\phi$.
Then, the law of modal monotonicity MM reflects
	the semantic fact mentioned in Section~\ref{section:Contribution} that
		LIiP's Kripke-model absorbs
			the partial order for
				the Kripke-semantics of LIiP's intuitionistic connectives as
					a mere instance of the accessibility relation for
				the Kripke-semantics of LIiP's proof modality,
		thanks to being parametric (and thus generic, cf.\  Section~\ref{section:Semantically}).
Thus we adopt formulas of the shape $\phi\rightarrow\Box\phi$ as axioms MM in
	our intuitionistic modal logical system LIiP,
		like Do\v{s}en in his intuitionistic modal logical system $\mathit{Hdn\Box}$
			\cite{IntuitionisticDoubleNegationAsNecessity}, where
				he adopts formulas of that form as axioms \emph{dn2}.
To our knowledge,
	$\mathit{Hdn\Box}$ and LIiP are the only intuitionistic modal logics with such axioms.
Finally,
	we could add
		admissible but not derivable rules and
		their corresponding internalising axioms to
			LIiP in the style of \cite{LIPArtemov}.\label{page:LIP:5}
(Recall from \cite{sep-logic-intuitionistic} that
	the admissible rules of a theory are the rules under which the theory is closed.
	%
	Hence the set of primitive and derivable rules is a subset of the set of admissible rules,
		and [but not] vice versa in classical [intuitionistic] logic.
	%
	[IL is \emph{structurally incomplete}.]
	%
	See \cite{jerabek:independent-bases} for suitable \emph{bases} of admissible rules.)
However,
	since the addition of admissible but not derivable rules to a theory
		does not change the theory, such
			an addition can be considered as unnecessary,
				at least in our base theory.

In the sequel, ``:iff'' abbreviates ``by definition, if and only if''.
\begin{proposition}[Hilbert-style proof system]\label{proposition:Hilbert}
	Let
		\begin{itemize}
			\item $\Phi\vdash_{\LIiP}\phi$ \text{:iff} if $\Phi\subseteq\mathrm{LIiP}$ then $\phi\in\mathrm{LIiP}$
			\item $\phi\mathrel{{\dashv}{\vdash}_{\LIiP}}\phi'$ \text{:iff} $\set{\phi}\vdash_{\LIiP}\phi'$ and $\set{\phi'}\vdash_{\LIiP}\phi$
			\item $\vdash_{\LIiP}\phi$ \text{:iff} $\emptyset\vdash_{\LIiP}\phi.$
		\end{itemize}
		%
		In other words, ${\vdash_{\LIiP}}\subseteq\powerset{\mathcal{L}}\times\mathcal{L}$ is a \emph{system of closure conditions} in the sense of
				\cite[Definition~3.7.4]{PracticalFoundationsOfMathematics}.
		%
		For example:
			\begin{enumerate}
				\item for all axioms $\phi\in\Gamma_{1}$, $\vdash_{\LIiP}\phi$
				\item for \emph{modus ponens}, $\set{\phi,\phi\rightarrow\phi'}\vdash_{\LIiP}\phi'$

				\item for epistemic antitonicity,

					$\set{\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'}}\vdash_{\LIiP}
						(\Iproves{M'}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$.
			\end{enumerate}
		%
		(In the space-saving, horizontal Hilbert-notation ``$\Phi\vdash_{\LIiP}\phi$'',
			$\Phi$ is not a set of hypotheses but a set of premises, cf.\
				\emph{modus ponens} and epistemic antitonicity.)

	Then, $\vdash_{\LIiP}$ can be viewed as being defined by
		a $\Clo{}{}$-induced Hilbert-style proof system.
	%
	In fact
			${\Clo{}{}}:\powerset{\mathcal{L}}\rightarrow\powerset{\mathcal{L}}$ is a \emph{standard consequence operator,} i.e.,\xspace
				a \emph{substitution-invariant compact closure operator.}
\end{proposition}
\begin{proof}
	Like in \cite{LiP}.
	That a Hilbert-style proof system can be viewed as induced by
		 a compact closure operator is well-known (e.g.,\xspace see \cite{WhatIsALogicalSystem});
	that $\Clo{}{}$ is indeed such an operator can be verified by
		inspection of the inductive definition of $\Clo{}{}$; and
	substitution invariance follows from our definitional use of axiom \emph{schemas}.\footnote{%
		Alternatively to axiom schemas,
		we could have used
			axioms together with an
			additional substitution-rule set
				$\setst{\sigma[\phi]}{\phi\in\Clo{}{n}(\Gamma)}$
		in the definiens of $\Clo{}{n+1}(\Gamma)$.}
\end{proof}

\begin{corollary}[Normality]\label{corollary:Normality}
		LIiP is a normal modal logic.
\end{corollary}
\begin{proof}
	Jointly by
		Kripke's law and
		\emph{modus ponens} (by definition),
		necessitation (cf.\  proof of Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.0), and
		substitution invariance (cf.\  Proposition~\ref{proposition:Hilbert}).
\end{proof}
\noindent

We are now going to present some useful
	deducible \emph{structural} laws of LIiP,
		including the deducible non-structural rule of epistemic bitonicity,
			used in the deduction of some of them.
Here,
	``structural'' means
	``deducible exclusively from term axioms.''
The laws are enumerated in a (total) order that respects (but cannot reflect) their respective proof prerequisites.
The laws are also deducible in LiP, in the same order and
	without non-intuitionistic machinery \cite{LiP}.
\begin{theorem}[Some useful deducible structural laws]\label{theorem:SomeUsefulDeducibleStructuralLaws}\
	\begin{enumerate}
		\item $\vdash_{\LIiP}\knows{a}{\pair{M}{M'}}\rightarrow\knows{a}{M}
		\\(left projection,
			1-way $\mathtt{K}$-combinator property)
		\item $\vdash_{\LIiP}\knows{a}{\pair{M}{M'}}\rightarrow\knows{a}{M'}$\quad(right projection)
		\item $\vdash_{\LIiP}\knows{a}{\pair{M}{M}}\leftrightarrow\knows{a}{M}$\quad(pairing idempotency)
		\item $\vdash_{\LIiP}\knows{a}{\pair{M}{M'}}\leftrightarrow\knows{a}{\pair{M'}{M}}$\quad(pairing commutativity)
		\item $\vdash_{\LIiP}(\knows{a}{M}\rightarrow\knows{a}{M'})\leftrightarrow(\knows{a}{\pair{M}{M'}}\leftrightarrow\knows{a}{M})
		\\(neutral pair elements)
		\item $\vdash_{\LIiP}\knows{a}{\pair{M}{a}}\leftrightarrow\knows{a}{M}$\quad(self-neutral pair element)
		\item $\vdash_{\LIiP}\knows{a}{\pair{M}{\pair{M'}{M''}}}\leftrightarrow\knows{a}{\pair{\pair{M}{M'}}{M''}}$\quad(pairing associativity)
		\item $\set{\knows{\mathtt{CM}}{M}\leftrightarrow\knows{\mathtt{CM}}{M'}}\vdash_{\LIiP}
					(\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M'}{\phi}{\mathtt{CM}}{}$\quad(epistemic bitonicity)
		\item $\vdash_{\LIiP}(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{\pair{M'}{M}}{\phi}{\mathtt{CM}}{}$\quad(proof extension, left)
		\item $\vdash_{\LIiP}(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{\pair{M}{M'}}{\phi}{\mathtt{CM}}{}$\quad(proof extension, right)
		\item $\vdash_{\LIiP}((\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproves{M'}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{\pair{M}{M'}}{\phi}{\mathtt{CM}}{}$\quad(proof extension)
		\item $\vdash_{\LIiP}(\Iproves{\pair{M}{M}}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$\quad(proof idempotency)
		\item $\vdash_{\LIiP}(\Iproves{\pair{M}{M'}}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{\pair{M'}{M}}{\phi}{\mathtt{CM}}{}$\quad(proof commutativity)
	\item $\set{\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'}}\vdash_{\LIiP}(\Iproves{\pair{M}{M'}}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}
	\\(neutral proof elements)
		\item $\vdash_{\LIiP}(\Iproves{\pair{M}{\mathtt{CM}}}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$\quad(self-neutral proof element)
		\item $\vdash_{\LIiP}(\Iproves{\pair{M}{\pair{M'}{M''}}}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{\pair{\pair{M}{M'}}{M''}}{\phi}{\mathtt{CM}}{}
		\\(proof associativity)
	\end{enumerate}
\end{theorem}
\begin{proof}
	Like in \cite{LiP}---no non-intuitionistic machinery is required.
\end{proof}
\noindent
For a discussion of these LIiP laws,
		consider our discussion of their analogs in LiP \cite{LiP} and the following remark.
\begin{remark}[Monotonicity---Proof \& Truth]\label{remark:Monotonicity}
The law of proof extension captures
	the monotonicity of the \emph{proof terms} in LIiP mentioned in Table~\ref{table:picture},
		as does its analog in LiP.
In contrast,
	the law of modal monotonicity (cf.\  Definition~\ref{definition:AxiomsRules}),
		which does not hold in LiP,
			captures the monotonicity of the \emph{local truths} in LIiP.
Recall from Section~\ref{section:Introduction} that in an intuitionistic (modal) universe (such as LIiP's),
	all, i.e.,\xspace positive or negative (whence the notation `$\Iproves{}{}{\mathtt{CM}}{}$\negthinspace'), (local) truths are monotonic.
Whereas in a classical (modal) universe (such as LiP's),
	not all (local) truths need be monotonic.
If a proof term is monotonic then its proof goal is.
If a proof goal is monotonic then its proof must be.
In LIiP,
	all proof goals are monotonic,
		thanks to LIiP being intuitionistic, which is what
			forces them to be so.
However in LiP,
	not all proof goals need be monotonic,
		because of LiP being classical as well as modal, which is what
			frees them from being so.
\end{remark}
\begin{corollary}[$\mathtt{S}$-combinator property]\label{corollary:Combinator}\
	\begin{enumerate}
		\item $\vdash_{\LIiP}\knows{a}{\pair{\pair{M}{M'}}{M''}}\leftrightarrow\knows{a}{\pair{M}{\pair{M''}{\pair{M'}{M''}}}}$
		\item $\vdash_{\LIiP}(\Iproves{\pair{\pair{M}{M'}}{M''}}{\phi}{\mathtt{CM}}{})\leftrightarrow
						\Iproves{\pair{M}{\pair{M''}{\pair{M'}{M''}}}}{\phi}{\mathtt{CM}}{}$
	\end{enumerate}
\end{corollary}
\begin{proof}
	Like in \cite{LiP}---again, no non-intuitionistic machinery is required.
\end{proof}

We are going to present also some useful, deducible \emph{logical} laws of LIiP.
Here,
	``logical'' means
	``not structural'' in the previously defined sense.
Also these laws are enumerated in an order that respects their respective proof prerequisites.

Grey-shading indicates special interest for
	intuitionistic modal logic in general and for LIiP as opposed to (the classical) LiP in particular.
Three important themes therein are:
	first, intuitionistic negation (single `$\neg$' and double `$\neg\neg$') and
	second, individual knowledge ($\knows{\mathtt{CM}}{M}$), and their import for
		the relation between
			$\Iproves{M}{\phi}{\mathtt{CM}}{}$ and its dual
			$\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$, which
				is normally not one of identity nor dual definability in intuitionistic modal logic; and
	third, the internalised disjunction property (IDP), which
		does not hold in LiP.
(\cite{LIPArtemov}\label{page:LIP:7} remain silent about the deducibility of an IDP in their logic, which, given that they internalise standard IL, is intriguing.)
Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws} has four important corollaries, among which there is
	a modal-depth result,
	the relation of LIiP to
		Fischer Servi's \cite{IK:FischerServi} and
		Plotkin and Stirling's \cite{IK:PlotkinStirling} seminal work on intuitionistic modal logic, and
	the relation of LIiP to standard
		doxastic \cite{MultiAgents} and
		epistemic logic \cite{MultiAgents,Epistemic_Logic,EpistemicLogicFiveQuestions}.
The number of intermediate results required to obtain the corollaries,
	reflected in the length of Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws},
		may be indicative of the exponential blow-up in proof length of
			intuitionistic over classical logic \cite{LowerProofComplexityIL}.
The non-intuitionistically inclined reader may want to skip them except
	Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.58.
Whereas the intuitionistically inclined reader may want to prove them herself,
	in order and as milestones for proving their corollaries.
\begin{theorem}[Some useful deducible logical laws]\label{theorem:SomeUsefulDeducibleLogicalLaws}\
		\begin{enumerate}\setcounter{enumi}{-1}
		\item $\{\phi\}\vdash_{\LIiP}\Iproves{M}{\phi}{\mathtt{CM}}{}$\quad(necessitation, N)
		\item $\vdash_{\LIiP}(\Iproves{M}{(\phi\rightarrow\phi')}{\mathtt{CM}}{})\rightarrow
				((\Iproves{M'}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{\pair{M}{M'}}{\phi'}{\mathtt{CM}}{})$\\
				\quad(generalised Kripke-law, GK)
		\item $\set{\phi\rightarrow\phi'}\vdash_{\LIiP}(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{}$\quad(regularity, R)
		\item $\set{\phi\leftrightarrow\phi'}\vdash_{\LIiP}(\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{}$\quad(R \emph{bis})
		\item $\set{\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'},\phi\rightarrow\phi'}\vdash_{\LIiP}(\Iproves{M'}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{}$\\
		\quad(epistemic regularity, ER)
		\item $\set{\knows{\mathtt{CM}}{M}\leftrightarrow\knows{\mathtt{CM}}{M'},\phi\leftrightarrow\phi'}\vdash_{\LIiP}(\Iproves{M'}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{}$\quad(ER \emph{bis})
		\item $\vdash_{\LIiP}\Iproves{M}{\text{true}}{\mathtt{CM}}{}$\quad(anything can prove tautological truth)
		\item $\vdash_{\LIiP}\Iproofdiamond{M}{\text{true}}{\mathtt{CM}}{}$\quad(anything can disprove tautological falsehood)
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\blacksquare\phi\leftrightarrow\phi$\quad(TMM)}
		\item $\phi\mathrel{{\dashv}{\vdash}_{\LIiP}}\blacksquare\phi$\quad(TMM \emph{bis})
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\knows{\mathtt{CM}}{M}\rightarrow((\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\phi)$\quad(ET \emph{bis})}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\neg\neg(\knows{\mathtt{CM}}{M})$\quad(CM message communicability, CMMC)}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\neg\neg((\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\phi)$\quad(possible TMM, PTMM)}
		\item $\vdash_{\LIiP}\neg\phi\rightarrow\neg(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})$\\
				(falsehood implies falsehood non-disprovability, FIFND)
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}\neg(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\neg(\Iproves{M}{\phi}{\mathtt{CM}}{})$\\
				(falsehood non-disprovability equals truth unprovability, FNDETU)\end{tabular}}
		\item $\vdash_{\LIiP}\neg\phi\rightarrow\neg(\Iproves{M}{\phi}{\mathtt{CM}}{})$\\
				(falsehood implies truth unprovability, FITU)
		\item $\vdash_{\LIiP}\neg\neg\phi\rightarrow\neg(\Iproofdiamond{M}{\neg\phi}{\mathtt{CM}}{})$\quad(FIFND \emph{bis})
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\neg(\Iproofdiamond{M}{\neg\phi}{\mathtt{CM}}{})\leftrightarrow\neg(\Iproves{M}{\neg\phi}{\mathtt{CM}}{})$\quad(FNDETU \emph{bis})}
		\item $\vdash_{\LIiP}\neg\neg\phi\rightarrow\neg(\Iproves{M}{\neg\phi}{\mathtt{CM}}{})$\quad(FITU \emph{bis})
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}l@{}}
				$\vdash_{\LIiP}$&$(\phi\lor(\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\rightarrow$\\
					&$(\neg\neg\phi\land\neg(\Iproofdiamond{M}{\neg\phi}{\mathtt{CM}}{})\land\neg(\Iproves{M}{\neg\phi}{\mathtt{CM}}{}))$\\ \multicolumn{2}{@{}l}{(extended weak double-negation law, EWDN)}
				\end{tabular}}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}(\neg\neg\phi\rightarrow\phi')\rightarrow
						((\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{})$\\
				(conditional functionality, CF)
				\end{tabular}}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
					$\vdash_{\LIiP}(\neg\neg\phi\rightarrow\phi)\rightarrow
						((\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{\phi}{\mathtt{CM}}{})$\\
				(local classicality implies modal equivalence, LCIME)
				\end{tabular}}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}(\knows{\mathtt{CM}}{M}\land\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow(\neg\neg\phi\rightarrow\phi)$\\
				(proof knowledge implies local classicality, PKILC)
				\end{tabular}}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}(\knows{\mathtt{CM}}{M}\land\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow((\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{\phi}{\mathtt{CM}}{})$\\
				(proof knowledge implies modal equivalence, PKIME)
				\end{tabular}}
		\item $\vdash_{\LIiP}\neg(\Iproves{M}{\text{false}}{\mathtt{CM}}{})$\quad(nothing can prove tautological falsehood)
		\item $\vdash_{\LIiP}\neg(\Iproofdiamond{M}{\text{false}}{\mathtt{CM}}{})$\quad(nothing can disprove tautological truth)
		\item $\vdash_{\LIiP}\phi\rightarrow\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$\quad(weak MM, WMM)
		\item $\set{\knows{\mathtt{CM}}{M}\rightarrow\phi}\mathrel{{\dashv}{\vdash}_{\LIiP}}\Iproves{M}{\phi}{\mathtt{CM}}{}$\quad(epistemic N, EN)
		\item $\set{\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'}}\mathrel{{\dashv}{\vdash}_{\LIiP}}\Iproves{M}{\knows{\mathtt{CM}}{M'}}{\mathtt{CM}}{}$\quad(EN \emph{bis})
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\Iproves{M}{((\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\phi)}{\mathtt{CM}}{}$\quad(ET \emph{bis} self-proof)}
		\item $\vdash_{\LIiP}(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$\quad(4)
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\neg(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\neg(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$\quad(5)}
		\item $\vdash_{\LIiP}((\Iproves{M}{\phi}{\mathtt{CM}}{})\land\Iproves{M'}{\phi'}{\mathtt{CM}}{})\rightarrow
						\Iproves{\pair{M}{M'}}{(\phi\land\phi')}{\mathtt{CM}}{}$\\
						\quad(proof conjunctions)
		\item $\vdash_{\LIiP}((\Iproves{M}{\phi}{\mathtt{CM}}{})\land\Iproves{M}{\phi'}{\mathtt{CM}}{})\leftrightarrow
						\Iproves{M}{(\phi\land\phi')}{\mathtt{CM}}{}$
						\quad(proof conjunctions \emph{bis})
		\item $\vdash_{\LIiP}((\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproves{M'}{\phi'}{\mathtt{CM}}{})\rightarrow
						\Iproves{\pair{M}{M'}}{(\phi\lor\phi')}{\mathtt{CM}}{}$\quad(proof disjunctions)
		\item $\vdash_{\LIiP}((\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproves{M}{\phi'}{\mathtt{CM}}{})\rightarrow
						\Iproves{M}{(\phi\lor\phi')}{\mathtt{CM}}{}$\quad(proof disjunctions \emph{bis})
		\item $\vdash_{\LIiP}(\Iproves{M}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\leftrightarrow
				\Iproves{M}{\phi}{\mathtt{CM}}{}$\quad(modal idempotency, MI)
		\item $\vdash_{\LIiP}(\Iproofdiamond{M}{(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\leftrightarrow
				\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$\quad(MI \emph{bis})
		\item \colorbox[gray]{0.75}{
				\begin{tabular}[t]{@{}l@{}}
					$\vdash_{\LIiP}(\phi\lor(\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproofdiamond{M}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$\\
					(nested MM, NMM)
				\end{tabular}}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}(\Iproves{M}{(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\rightarrow\Iproofdiamond{M}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$\quad(modal swap, MS)}
		\item \colorbox[gray]{0.75}{
				\begin{tabular}[t]{@{}l@{}}
					$\vdash_{\LIiP}\knows{\mathtt{CM}}{M}\rightarrow((\Iproves{M}{(\phi\lor\phi')}{\mathtt{CM}}{})\rightarrow((\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproves{M}{\phi'}{\mathtt{CM}}{}))$\\
					(epistemic internalised disjunction property, EIDP)
				\end{tabular}}
		\item \colorbox[gray]{0.75}{
				\begin{tabular}[t]{@{}l@{}}
					$\vdash_{\LIiP}\Iproves{M}{((\Iproves{M}{(\phi\lor\phi')}{\mathtt{CM}}{})\rightarrow((\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproves{M}{\phi'}{\mathtt{CM}}{}))}{\mathtt{CM}}{}$\\
					(IDP self-proof)
				\end{tabular}}
		\item $\vdash_{\LIiP}(\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{(\knows{\mathtt{CM}}{M}\land\phi)}{\mathtt{CM}}{}$
				\quad(epistemic idempotency, EI)
		\item $\vdash_{\LIiP}(\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\Iproves{M}{(\knows{\mathtt{CM}}{M}\land\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$
				\quad(EI \emph{bis})
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}(\Iproofdiamond{M}{(\phi\lor\phi')}{\mathtt{CM}}{})\leftrightarrow
				((\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\lor\Iproofdiamond{M}{\phi'}{\mathtt{CM}}{})$\\
				(Plotkin-Stirling 4, PS4)
				\end{tabular}}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}(\Iproves{M}{(\phi\rightarrow\phi')}{\mathtt{CM}}{})\rightarrow
				((\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproofdiamond{M}{\phi'}{\mathtt{CM}}{})$\\
					(Plotkin-Stirling 2, PS2)
					\end{tabular}}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}((\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{})\rightarrow
				\Iproves{M}{(\phi\rightarrow\phi')}{\mathtt{CM}}{}$\\
					(Plotkin-Stirling 5, PS5)
				\end{tabular}}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}(\neg\neg\phi\rightarrow\phi')\rightarrow
				\Iproves{M}{(\phi\rightarrow\phi')}{\mathtt{CM}}{}$\quad(CFPS5)}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}l@{}}
				$\vdash_{\LIiP}$&$((\neg\neg\phi\rightarrow\phi')\land(\neg\neg\phi'\rightarrow\phi))\rightarrow$\\
						&$((\Iproves{M}{(\phi\lor\phi')}{\mathtt{CM}}{})\rightarrow((\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproves{M}{\phi'}{\mathtt{CM}}{}))$\\
				\multicolumn{2}{@{}l}{(conditional IDP, CIDP)}
				\end{tabular}}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}(\phi\lor(\Iproves{M}{\phi}{\mathtt{CM}}{})\lor\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$\quad(NMM \emph{bis})}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}(\Iproofdiamond{M}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\rightarrow
					\Iproves{M}{(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$\quad(MS \emph{bis})}
		\item \colorbox[gray]{0.75}{\begin{tabular}[t]{@{}l@{}}
				$\vdash_{\LIiP}(\Iproves{M}{(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\leftrightarrow
							\Iproofdiamond{M}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{}$\\
								(modal commutativity, MC)
								\end{tabular}}
		\item \colorbox[gray]{0.75}{
					\begin{tabular}[t]{@{}l}
						$\vdash_{\LIiP}(\Iproofdiamond{M}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\leftrightarrow\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$\\
							(mixed modal idempotency, MMI)
							\end{tabular}}
		\item \colorbox[gray]{0.75}{
				$\vdash_{\LIiP}(\Iproves{M}{(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\leftrightarrow
							\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$\quad(MMI \emph{bis})}
		\item $\vdash_{\LIiP}(\Iproves{M}{\neg\neg\phi}{\mathtt{CM}}{})\rightarrow
							\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$\quad(double-negation absorption, DNA)
		\item $\vdash_{\LIiP}(\Iproves{M}{\neg\neg\phi}{\mathtt{CM}}{})\rightarrow
							\neg\neg(\Iproves{M}{\phi}{\mathtt{CM}}{})$\quad(double-negation extrusion, DNE)
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\neg(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\rightarrow
							\Iproofdiamond{M}{\neg\phi}{\mathtt{CM}}{}$\quad(weak negation completeness, WNC)}					\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}\neg(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow
							\Iproofdiamond{M}{\neg\phi}{\mathtt{CM}}{}$\quad(WNC \emph{bis})}
		\item \colorbox[gray]{0.75}{$\boxed{\vdash_{\LIiP}(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})\leftrightarrow
										\neg\neg(\Iproves{M}{\phi}{\mathtt{CM}}{})}$\quad(modal double negation, MDN)}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}((\Iproves{M}{\phi}{\mathtt{CM}}{})\land
							\Iproofdiamond{M}{(\phi\rightarrow\phi')}{\mathtt{CM}}{})\rightarrow
								\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}$\quad(Wiv)}
		\item \colorbox[gray]{0.75}{$\vdash_{\LIiP}(\Iproofdiamond{M}{(\phi\land\neg\phi')}{\mathtt{CM}}{})\rightarrow
								(\phi\land\neg\phi')$\quad(Wv)}
\end{enumerate}
\end{theorem}
\begin{proof}
	See Appendix~\ref{appendix:Proofs:LogicalLaws}.
\end{proof}
\noindent
The following remark flags a non-trivial insight, also explicated
	in Section~\ref{section:Semantically}.
\begin{remark}[Intuitionistic truths]\label{remark:IntuitionisticTruths}
	Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.8
		means that
			in interactive settings,
				the intuitionistic truths are those of the communication medium.
\end{remark}
\noindent
The reader is invited to
	compare Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.8 to its global counterpart
			Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.27,
				whose analog also holds in LiP but was not stated there.
\begin{corollary}[Modal-depth result]\label{corollary:ModalDepth}\
	Let $\heartsuit_{1}\cdots\heartsuit_{n}\phi\in\mathcal{L}$ such that
		for all $1\leq i\leq n$,
			$\heartsuit_{i}\in\set{\text{`}\Iproves{M}{}{\mathtt{CM}}{}\negthickspace\text{'}\,,\text{`}\Iproofdiamond{M}{}{\mathtt{CM}}{}\negthickspace\text{'}\;}$.
	Then, if the prefix `\,$\heartsuit_{1}\cdots\heartsuit_{n}$\negthinspace' contains
		\begin{enumerate}
			\item only occurrences of the `$\Iproves{M}{}{\mathtt{CM}}{}$\negthickspace'-modality
					then $$\vdash_{\LIiP}(\heartsuit_{1}\cdots\heartsuit_{n}\phi)\leftrightarrow
									\Iproves{M}{\phi}{\mathtt{CM}}{}\,;$$
			\item at least one occurrence of the `$\Iproofdiamond{M}{}{\mathtt{CM}}{}$\negthickspace'-modality
					then $$\vdash_{\LIiP}(\heartsuit_{1}\cdots\heartsuit_{n}\phi)\leftrightarrow
									\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}\,.$$
		\end{enumerate}
\end{corollary}
\begin{proof}
	For 1, apply MI.
	%
	For 2,
		apply MI, MI \emph{bis}, MMI, and MMI \emph{bis}.
\end{proof}

\begin{corollary}[Intuitionistic Modal Logic]\label{corollary:IK}
	LIiP is a refinement (due to its parameterised modality) and extension (due to additional laws) of
		Fischer Servi's \cite{IK:FischerServi} and
		Plotkin and Stirling's \cite{IK:PlotkinStirling}
	intuitionistic modal logic IK.

	Similarly is
		LIiP a refinement and extension of
			the propositional fragment of
				Wijesekera's system of first-order constructive modal logic \cite[Section~1.5]{ConstructiveModalLogicI}.
\end{corollary}
\begin{proof}
	In fact,
		Plotkin and Stirling's axiomatisation of IK, which
			is equivalent to Fischer Servi's,
				consists of the axioms of IL and the laws K, MP, N as well as the axiom analogs of
					Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.25 and
					\ref{theorem:SomeUsefulDeducibleLogicalLaws}.44--\ref{theorem:SomeUsefulDeducibleLogicalLaws}.46; and
		the propositional fragment of Wijesekera's system consists of the axioms of IL and the laws K, MP, N as well as the axiom analogs of
					Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.45,
					\ref{theorem:SomeUsefulDeducibleLogicalLaws}.59 and
					\ref{theorem:SomeUsefulDeducibleLogicalLaws}.60.
\end{proof}

The following corollary asserts that
	our disjunctive proof modality is also
		an \emph{explicit refinement} of the standard (implicit) belief modality \cite{MultiAgents}.
\begin{corollary}[Disjunctive Explicit Belief]\label{corollary:DEB}\
	`$\Iproves{M}{\cdot}{\mathtt{CM}}{}$' is
				a \emph{disjunctive KD45-modality} of explicit agent belief,
	where
		$M$ represents the explicit evidence term that can justify the agent $\mathtt{CM}$'s belief.
	Additionally,
		the communication medium $\mathtt{CM}$ is a truth-believing agent in the sense that
			$\vdash_{\LIiP}\phi\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$.

\end{corollary}
\begin{proof}
	Consider that
		`$\Iproves{M}{\cdot}{\mathtt{CM}}{}$' satisfies
			the K-law (cf.\  Definition~\ref{definition:AxiomsRules}),
			the D-law (called ID in Definition~\ref{definition:AxiomsRules}),
			the 4-law (cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.30),
			the 5-law (cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.31),
			IDP self-proof (cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.41),
			the MM-law (cf.\  Definition~\ref{definition:AxiomsRules}), and
			the N-law (cf.\  Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.0).
\end{proof}
Thanks to Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.10,
	$\knows{\mathtt{CM}}{M}$ is a sufficient condition for `$\Iproves{M}{\cdot}{\mathtt{CM}}{}$' to
		behave like a standard S5-modality of \emph{perfect knowledge}\label{page:PerfectKnowledge}
		(in a technical sense) \cite{MultiAgents,Epistemic_Logic,EpistemicLogicFiveQuestions}, which
			in addition to being a KD45-modality not only obeys the D-law but also the stronger T-law (knowledge, not only belief) and the MM-law (\emph{perfect} knowledge):
				$$\vdash_{\LIiP}\knows{\mathtt{CM}}{M}\rightarrow((\Iproves{M}{\phi}{\mathtt{CM}}{})\leftrightarrow\phi).$$
\begin{remark}[Perfect knowledge]\label{remark:PerfectKnowledge}
In interactive settings,
	only the communication medium $\mathtt{CM}$,
		through which all messages have to pass,
			can attain perfect knowledge
				(the other agents having only
					partial visibility of the network,
						cf.\  Definition~\ref{definition:SemanticIngredients}).
However note that
	LIiP being propositionally modal-intuitionistic,
	this perfect knowledge is of propositional invariants of
		the communication network only (cf.\  Page~\pageref{page:invariants}).
So the epistemic perfection of the communication medium is only within a certain \emph{grain} (propositional) and \emph{scope} (invariants).
\end{remark}

In the following corollary,
	we construct also
		a disjunctive explicit refinement of (implicit) S4-provability.
\begin{corollary}[Disjunctive Explicit Provability]\label{corollary:DEP}
	`\,$\knows{\mathtt{CM}}{M}\land\Iproves{M}{\cdot}{\mathtt{CM}}{}$' is
		a \emph{disjunctive S4-modality} of explicit agent provability, where
			$M$ represents the explicit evidence term that does justify agent $\mathtt{CM}$'s knowledge.
\end{corollary}
\begin{proof}
	By Corollary~\ref{corollary:DEB},
		Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.10, and
		Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.40:
			The T-law
				$\vdash_{\LDiiP}(\knows{\mathtt{CM}}{M}\land\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\phi$ for
					the modality `$\knows{\mathtt{CM}}{M}\land\Iproves{M}{\cdot}{\mathtt{CM}}{}$' can be recognised by
						inspecting Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.10, and
			the disjunctivity $\vdash_{\LDiiP}(\knows{\mathtt{CM}}{M}\land\Iproves{M}{(\phi\lor\phi')}{\mathtt{CM}}{})\rightarrow
				((\knows{\mathtt{CM}}{M}\land\Iproves{M}{\phi}{\mathtt{CM}}{})\lor(\knows{\mathtt{CM}}{M}\land\Iproves{M}{\phi'}{\mathtt{CM}}{}))$
		by inspecting Theorem~\ref{theorem:SomeUsefulDeducibleLogicalLaws}.40.
\end{proof}

\subsection{Semantically}\label{section:Semantically}
We continue to present
	the concretely constructed semantics as well as
	the standard abstract semantic interface for LIiP, and
prove the axiomatic adequacy of the proof system with respect to this interface.
The core ingredient of the concrete semantics of LIiP are so-called \emph{input histories,} which
	were introduced in \cite{LDiiP,KramerIMLA2013} and
	could also be used in an even more concrete semantics of LiP.
Input histories
	are finite words of input events and
	serve as concrete states $s\in\mathcal{S}$ in
		the state space $\mathcal{S}$, on which
			the concrete and abstract accessibility relation
				${\pAccess{M}{\mathtt{CM}}{}}\subseteq\mathcal{S}\times\mathcal{S}$ and
				${\access{M}{\mathtt{CM}}{}}\subseteq\mathcal{S}\times\mathcal{S}$ for LIiP is defined, respectively.
The reader of \cite{LiP,KramerICLA2013} will recognise
	similar but simpler definitions here;
		the one of ${\pAccess{M}{\mathtt{CM}}{}}$ could be even simpler (cf.\  Fact~\ref{fact:identities}.2), but
			is as now in order to allow for
				a simpler, pattern-matching comparison with
					the corresponding one in \cite{LiP,KramerICLA2013}.
(We wanted to show how to produce LIiP from LiP.)

\subsubsection{Concretely}\label{section:Concretely}

\begin{definition}[Semantic ingredients]\label{definition:SemanticIngredients}
For the set-theoretically constructive, model-theoretic study of LIiP let
\begin{itemize}
	\item $\mathcal{S}\ni s\mathrel{::=}\mathtt{0}\ \big| \  \gscc{a}{M}(s)$ designate the concrete state space $\mathcal{S}$ of
			\emph{input histories} $s$, where
				$\mathtt{0}$ designates the empty input history
					(i.e.,\xspace a zero data point, e.g.,\xspace an initial state) and
				$\gscc{a}{M}$ can be read as ``agent $a$ receives message $M$''
					(e.g.,\xspace from some other agent acting as an oracle for $a$); and
					$\star:(\mathcal{S}\times\mathcal{S})\to\mathcal{S}$ monoidal concatenation on $\mathcal{S}$
						(with neutral element $\mathtt{0}$);
	\item $\pi_{a}:\mathcal{S}\rightarrow\mathcal{S}$ designate (local) \emph{state projection on $a$'s view} such that
			\begin{align*}
				\pi_{a}(\mathtt{0}) &\mathrel{:=} \mathtt{0}\\
				\pi_{a}(\gscc{b}{M}(s)) &\mathrel{:=}
					\begin{cases}
						\gscc{b}{M}(\pi_{a}(s)) & \text{if $a\in\set{b,\mathtt{CM}}$, and}\\
						\pi_{a}(s) & \text{otherwise;}
					\end{cases}
			\end{align*}
			(The communication medium $\mathtt{CM}$ sees any agent's $b$ [including its own] input events, i.e.,\xspace
				$\mathtt{CM}$ has a global view on the current global state $s$.)
	\item $\msgs{}:\mathcal{S}\rightarrow\powerset{\mathcal{M}}$ designate \emph{raw-data extraction} such that
			\begin{align*}
				\msgs{}(\mathtt{0}) &\mathrel{:=} \emptyset\\
				\msgs{}(\gscc{a}{M}(s)) &\mathrel{:=} \msgs{}(s)\cup\set{M}\,;
			\end{align*}
	\item $\msgs{a}\mathrel{:=}\msgs{}\circ\pi_{a}$ designate (local) \emph{raw-data extraction by $a\,;$}
		\item $\clo{a}{s}:\powerset{\mathcal{M}}\rightarrow\powerset{\mathcal{M}}$ designate a \emph{data-mining operator} such that \label{page:DataMining}
			$\clo{a}{s}(\mathcal{D})\mathrel{:=}\clo{a}{}(\msgs{a}(s)\cup\mathcal{D})\mathrel{:=}\bigcup_{n\in\mathbb{N}}\clo{a}{n}(\msgs{a}(s)\cup\mathcal{D})$, where for all $\mathcal{D}\subseteq\mathcal{M}:$
				\begin{eqnarray*}
					\clo{a}{0}(\mathcal{D}) &\mathrel{:=}& \set{a}\cup\mathcal{D}\\
					\clo{a}{n+1}(\mathcal{D}) &\mathrel{:=}&
						\begin{array}[t]{@{}l@{}}
							\clo{a}{n}(\mathcal{D})\ \cup\\
							\setst{\pair{M}{M'}}{\set{M,M'}\subseteq\clo{a}{n}(\mathcal{D})}\cup\quad\text{(pairing)}\\
							\setst{M, M'}{\pair{M}{M'}\in\clo{a}{n}(\mathcal{D})}\quad\text{(unpairing)}
						\end{array}
				\end{eqnarray*}
				($\clo{a}{s}(\emptyset)$ can be viewed as $a$'s \emph{individual-knowledge base} in $s$.
					For application-specific terms such as signing and encryption,
					we would have to add here the closure conditions corresponding to their characteristic term axioms.)
	\item ${\sqsubseteq_{a}}\subseteq\mathcal{S}\times\mathcal{S}$ designate
		the (local) \emph{state \textbf{pre-}order of $a$} such that
			for all $s,s'\in\mathcal{S}$,
				$s\sqsubseteq_{a} s'$ :iff
					there is $s''\in\mathcal{S}$ such that
						$\pi_{a}(s)\star\pi_{a}(s'')=\pi_{a}(s')\,;$
	\item ${\sqsubseteq}\mathrel{:=}{\sqsubseteq_{\mathtt{CM}}}$ designate the (global) \emph{state \textbf{partial} order}
			serving as the concrete accessibility relation in the Kripke-semantics for the I-fragment of LIiP;

			($\sqsubseteq$ is partial thanks to
				$\mathtt{CM}$ seeing any agent's input events.)
	\item ${\equiv_{a}}\mathrel{:=}{\sqsubseteq_{a}}\cap(\sqsubseteq_{a})^{-1}$ designate the (local) \emph{state equivalence of $a$;}
	\item ${\pAccess{M}{\mathtt{CM}}{}}\subseteq\mathcal{S}\times\mathcal{S}$ designate
		the \emph{\textbf{concretely constructed} accessibility relation}---short, \emph{\textbf{concrete} accessibility}---for LIiP such that for all $s,s'\in\mathcal{S}$,
			\begin{eqnarray*}
				s\pAccess{M}{\mathtt{CM}}{}s' &\mbox{:iff}&
								s'\in\hspace{-3.25ex}
					\bigcup_{\scriptsize
					\begin{array}{@{}c@{}}
						\text{$s\sqsubseteq_{\mathtt{CM}}{}\tilde{s}$ and
						}\\[0.5\jot]
						M\in\clo{\mathtt{CM}}{\tilde{s}}(\emptyset)
					\end{array}
					}\hspace{-3.25ex}
					[\tilde{s}]_{\indist{\mathtt{CM}}{}{}}\\
				&\text{(iff}&
					\text{there is $\tilde{s}\in\mathcal{S}$ s.t.\
							$s\sqsubseteq_{\mathtt{CM}}{}\tilde{s}$ and
							$M\in\clo{\mathtt{CM}}{\tilde{s}}(\emptyset)$ and
							$\indist{\mathtt{CM}}{\tilde{s}}{s'}$).}
			\end{eqnarray*}
\end{itemize}
\end{definition}

Note that
	the data-mining operator
		$\clo{a}{}:\powerset{\mathcal{M}}\rightarrow\powerset{\mathcal{M}}$ is a compact closure operator, which
		induces a \emph{data-derivation relation} ${\derives{a}{}{}}\subseteq\powerset{\mathcal{M}}\times\mathcal{M}$ such that $\derives{a}{M}{\mathcal{D}}$ :iff $M\in\clo{a}{}(\mathcal{D})$, which
	(1) has the compactness and (2) the cut property,
	(3) is decidable in deterministic polynomial time in the size of $\mathcal{D}$ and $M$, and
	(4) induces a Scott information system of information tokens $M$ \cite{LiP}.
\begin{fact}\label{fact:identities}\
	\begin{enumerate}
		\item ${\equiv_{\mathtt{CM}}}=\mathrm{Id}_{\mathcal{S}}$
		\item $s\pAccess{M}{\mathtt{CM}}{}s'$ if and only if
							($s\sqsubseteq s'$ and
							 $M\in\clo{\mathtt{CM}}{s'}(\emptyset)$)
		\item ${\pAccess{\mathtt{CM}}{\mathtt{CM}}{}}={\sqsubseteq}$
	\end{enumerate}
\end{fact}
\begin{proof}
	By inspection of definitions.
\end{proof}
\noindent
Fact~\ref{fact:identities}.1 is important, because
	thanks to it
		the communication medium $\mathtt{CM}$ can have perfect knowledge,
			as asserted on Page~\pageref{page:PerfectKnowledge};
and Fact~\ref{fact:identities}.3 is, because
	thanks to it
		the partial order $\sqsubseteq$ for the Kripke-semantics of LIiP's intuitionistic connectives is absorbed as
		a mere instance $\pAccess{\mathtt{CM}}{\mathtt{CM}}{}$ of the accessibility relation $\pAccess{M}{\mathtt{CM}}{}$ for the Kripke-semantics of LIiP's proof modality, as announced on Page~\pageref{page:PartialOrder}.
Fact~\ref{fact:identities}.2 captures the intuition of the concrete accessibility of LIiP.
Spelled out,
	this intuition is that
		$\mathtt{CM}$ can access
			an input history $s'$ from
			the current input history $s$ with respect to a piece of data $M$ in question
				if and only if
					$s'$ is an extension of $s$ such that
						$M$ is in $\mathtt{CM}$'s individual-knowledge base at $s'$.
A simple example is that
	$\mathtt{0}\pAccess{\mathtt{CM}}{M}{}\gscc{a}{M}(\mathtt{0})$, because
		$\mathtt{0}\sqsubseteq\gscc{a}{M}(\mathtt{0})$ and
		$M\in\clo{\mathtt{CM}}{\gscc{a}{M}(\mathtt{0})}(\emptyset)$.
A slightly more complex example is that
	$\mathtt{0}\pAccess{\mathtt{CM}}{M'}{}\gscc{b}{\pair{M}{M'}}(\gscc{a}{M}(\mathtt{0}))$, because
		$\mathtt{0}\sqsubseteq\gscc{b}{\pair{M}{M'}}(\gscc{a}{M}(\mathtt{0}))$ and
		$M'\in\clo{\mathtt{CM}}{\gscc{b}{\pair{M}{M'}}(\gscc{a}{M}(\mathtt{0}))}(\emptyset)$.

We need the following auxiliary definition for
	the proposition following it.
\begin{definition}[Message pre-ordering \cite{LiP,KramerICLA2013}]\label{definition:MessagePreordering}\
	\begin{itemize}
		\item $M\sqsubseteq_{a}^{s}M'$ :iff
			if $M\in\clo{a}{s}(\emptyset)$ then $M'\in\clo{a}{s}(\emptyset)$
		\item $M\sqsubseteq_{a}M'$ :iff for all $s\in\mathcal{S}$, $M\sqsubseteq_{a}^{s}M'$
	\end{itemize}
\end{definition}
\noindent
Notice the definitional overloading of the notation $\sqsubseteq_{a}$, i.e.,\xspace
	once as ${\sqsubseteq_{a}}\subseteq\mathcal{S}\times\mathcal{S}$ in Definition~\ref{definition:SemanticIngredients} and once as ${\sqsubseteq_{a}}\subseteq\mathcal{M}\times\mathcal{M}$ in the previous Definition~\ref{definition:MessagePreordering}.

\begin{proposition}[Concrete accessibility]\label{proposition:ConcreteAccessibility}\
\begin{enumerate}
	\item If $s\pAccess{M}{\mathtt{CM}}{}s'$ then $M\in\clo{\mathtt{CM}}{s'}(\emptyset)$\quad(epistemic image)
	\item If $M\in\clo{\mathtt{CM}}{s}(\emptyset)$ then
			$s\pAccess{M}{\mathtt{CM}}{}s$\quad(conditional reflexivity)
	\item there is $s'\in\mathcal{S}$ such that $s\pAccess{M}{\mathtt{CM}}{}s'$\quad(seriality)
	\item ${\pAccess{M}{\mathtt{CM}}{}}\subseteq{\pAccess{\mathtt{CM}}{\mathtt{CM}}{}}={\sqsubseteq}$
				\quad(MIAR-inclusion)
	\item $({\pAccess{\mathtt{CM}}{\mathtt{CM}}{}}\circ{\pAccess{M}{\mathtt{CM}}{}})\subseteq{\pAccess{M}{\mathtt{CM}}{}}$
				\quad(special transitivity)
	\item If $M\sqsubseteq_{\mathtt{CM}}M'$
			then ${\pAccess{M}{\mathtt{CM}}{}}\subseteq{\pAccess{M'}{\mathtt{CM}}{}}$\quad
				(proof monotonicity)
\end{enumerate}
\end{proposition}
\begin{proof}
	For 1, inspect Fact~\ref{fact:identities}.2.
	%
	For 2, inspect Fact~\ref{fact:identities}.2 and \ref{fact:identities}.3 and
		the definition of $\sqsubseteq$ (to see that $\sqsubseteq$ is reflexive).
	%
	For 3,
		inspect Fact~\ref{fact:identities}.2 and
		let $s\in\mathcal{S}$.
		%
		Then choose $s'=\gscc{\mathtt{CM}}{M}(s)\in\mathcal{S}$, which implies that
			$s\sqsubseteq s'$ and
			$M\in\clo{\mathtt{CM}}{s'}(\emptyset)$.
	For 4, inspect Fact~\ref{fact:identities}.2 and \ref{fact:identities}.3 and
		the definitional fact that $\mathtt{CM}\in\clo{\mathtt{CM}}{s'}(\emptyset)$.
	%
	For 5,
		let $s,s'\in\mathcal{S}$ and
		suppose that $s\mathrel{({\pAccess{\mathtt{CM}}{\mathtt{CM}}{}}\circ{\pAccess{M}{\mathtt{CM}}{}})}s'$.
	%
	That is,
		there is $s''\in\mathcal{S}$ such that
			$s\pAccess{\mathtt{CM}}{\mathtt{CM}}{}s''$ and $s''\pAccess{M}{\mathtt{CM}}{}s'$.
	%
	Hence,
		$s\sqsubseteq s''$ and $\mathtt{CM}\in\clo{\mathtt{CM}}{s''}(\emptyset)$ as well as
		$s''\sqsubseteq s'$ and $M\in\clo{\mathtt{CM}}{s'}(\emptyset)$, by
			Fact~\ref{fact:identities}.2.
	%
	Hence
		$s\sqsubseteq s'$ by the transitivity of $\sqsubseteq$.
	%
	Hence $s\pAccess{M}{\mathtt{CM}}{}s'$ by Fact~\ref{fact:identities}.2.
	%
	For 6,
		let $M,M'\in\mathcal{M}$ and
		suppose that $M\sqsubseteq_{\mathtt{CM}}M'$.
		%
		Further,
			let $s,s'\in\mathcal{S}$ and
			suppose that $s\pAccess{M}{\mathtt{CM}}{}s'$.
		%
		Hence
			$M\sqsubseteq_{\mathtt{CM}}^{s'}M'$, and also
			$s\sqsubseteq s'$ and $M\in\clo{\mathtt{CM}}{s'}(\emptyset)$ by Fact~\ref{fact:identities}.2.
		%
		Hence $M'\in\clo{\mathtt{CM}}{s'}(\emptyset)$.
		%
		Hence $s\pAccess{M'}{\mathtt{CM}}{}s'$ by Fact~\ref{fact:identities}.2.
\end{proof}
\noindent
Note that ``MIAR'' stands for ``modal-intuitionistic-accessibility-relation.''

\subsubsection{Abstractly}\label{section:Abstractly}

\begin{definition}[Kripke-model]\label{definition:KripkeModel}
We define the \emph{satisfaction relation} $\models$ for
		LIiP in Table~\ref{table:SatisfactionRelation},
	\begin{table}[t]
	\centering
	\caption{Satisfaction relation}
	\smallskip
	\fbox{$\begin{array}{@{}rcl@{}}
		(\mathfrak{S}, \mathcal{V}), s\models P &\text{:iff}& s\in\mathcal{V}(P)\\[\jot]
		(\mathfrak{S}, \mathcal{V}), s\models\phi\lor\phi' &\text{:iff}& \text{$(\mathfrak{S}, \mathcal{V}), s\models\phi$ or $(\mathfrak{S}, \mathcal{V}), s\models\phi'$}\\[\jot]
		(\mathfrak{S}, \mathcal{V}), s\models\phi\land\phi' &\text{:iff}& \text{$(\mathfrak{S}, \mathcal{V}), s\models\phi$ and $(\mathfrak{S}, \mathcal{V}), s\models\phi'$}\\[\jot]
		(\mathfrak{S}, \mathcal{V}), s\models\neg\phi &\text{:iff}&
			\text{for all $s'\in\mathcal{S}$,
				if $s\sqsubseteq s'$
				then not $(\mathfrak{S}, \mathcal{V}), s'\models\phi$}\\[\jot]
		(\mathfrak{S}, \mathcal{V}), s\models\phi\rightarrow\phi' &\text{:iff}&
			\text{for all $s'\in\mathcal{S}$,
				if $s\sqsubseteq s'$
				then
					\begin{tabular}{@{}r@{}l@{}}
						(&not $(\mathfrak{S}, \mathcal{V}), s'\models\phi$\\
						 &or $(\mathfrak{S}, \mathcal{V}), s'\models\phi'$)
					\end{tabular}}\\[\jot]
		(\mathfrak{S}, \mathcal{V}), s\models\Iproves{M}{\phi}{\mathtt{CM}}{} &\text{:iff}&
			\begin{array}[t]{@{}l@{}}
				\text{for all $s'\in\mathcal{S}$, }
			 	\text{if $s\access{M}{\mathtt{CM}}{}s'$ then $(\mathfrak{S}, \mathcal{V}), s'\models\phi$}
			\end{array}
	\end{array}$}
	\label{table:SatisfactionRelation}
	\end{table}
where
	\begin{itemize}
		\item $\mathcal{V}:\mathcal{P}\rightarrow\powerset{\mathcal{S}}$ designates a usual \emph{valuation function,} yet
			\begin{itemize}
				\item \emph{partially predefined} such that for all $a\in\mathcal{A}$ and $M\in\mathcal{M}$,
							$$\mathcal{V}(\knows{a}{M})\mathrel{:=}\setst{s\in\mathcal{S}}{M\in\clo{a}{s}(\emptyset)}\,;$$

							(If agents are Turing-machines
							then $a$ knowing $M$ can be understood as $a$ being able to parse $M$ on its tape.)
				\item \emph{constrained} such that for all $s,s'\in\mathcal{S}$,
						$$\text{if $s\in\mathcal{V}(P)$ and $s\sqsubseteq s'$ then $s'\in\mathcal{V}(P)\,;$}$$
						(following Kripke's semantics for IL)
			\end{itemize}
		\item $\mathfrak{S}\mathrel{:=}(\mathcal{S},\sqsubseteq,\set{\access{M}{\mathtt{CM}}{}}_{M\in\mathcal{M}})$
			designates an intuitionistic modal \emph{frame} for LIiP with
		a usual partial order ${\sqsubseteq}\subseteq\mathcal{S}\times\mathcal{S}$ for the intuitionistic part as well as
		an \emph{\textbf{abstractly constrained} accessibility relation}---short, \emph{\textbf{abstract}  accessibility}---${\access{M}{\mathtt{CM}}{}}\subseteq\mathcal{S}\times\mathcal{S}$ for
			LIiP such that---the \emph{semantic interface:}\label{page:AbstractProofAccessibility}
			\begin{itemize}
				\item If $s\access{M}{\mathtt{CM}}{}s'$ then $M\in\clo{\mathtt{CM}}{s'}(\emptyset)$
				\item If $M\in\clo{\mathtt{CM}}{s}(\emptyset)$ then
						$s\access{M}{\mathtt{CM}}{}s$
				\item there is $s'\in\mathcal{S}$ such that $s\access{M}{\mathtt{CM}}{}s'$
				\item ${\access{M}{\mathtt{CM}}{}}\subseteq{\access{\mathtt{CM}}{\mathtt{CM}}{}}={\sqsubseteq}$
				\item $({\access{\mathtt{CM}}{\mathtt{CM}}{}}\circ{\access{M}{\mathtt{CM}}{}})\subseteq{\access{M}{\mathtt{CM}}{}}$
				\item If $M\sqsubseteq_{\mathtt{CM}}M'$
						then ${\access{M}{\mathtt{CM}}{}}\subseteq{\access{M'}{\mathtt{CM}}{}}$
			\end{itemize}
	\item $(\mathfrak{S},\mathcal{V})$ designates an intuitionistic modal \emph{model} for LIiP.
	\end{itemize}
\end{definition}
\noindent
Looking back,
	we recognise that
		Proposition~\ref{proposition:ConcreteAccessibility}
	actually establishes the important fact that
		our concrete accessibility $\pAccess{M}{\mathtt{CM}}{}$ in
		Definition~\ref{definition:SemanticIngredients} realises
			all the properties stipulated by
		our abstract accessibility $\access{M}{\mathtt{CM}}{}$ in Definition~\ref{definition:KripkeModel};
		we say that
		$$\text{$\pAccess{M}{\mathtt{CM}}{}$ \emph{exemplifies} (or \emph{realises}) $\access{M}{\mathtt{CM}}{}$\,.}$$
Further, observe that
	LIiP (like LiP) has a Herbrand-style semantics, i.e.,\xspace
			logical constants (agent names) and
			functional symbols (pairing) are self-interpreted rather than
		interpreted in terms of (other, semantic) constants and functions.
This simplifying design choice spares our framework from
	the additional complexity that would arise from term-variable assignments \cite{FOModalLogic}, which in turn
		keeps our models propositionally modal.
Our choice is admissible because our individuals (messages) are finite.
(Infinitely long ``messages'' are non-messages; they can never be completely received, e.g.,\xspace
	transmitting irrational numbers as such is impossible.)

\begin{definition}[Truth \& Validity \cite{ModalLogicSemanticPerspective}]\label{definition:TruthValidity}\
	\begin{itemize}
	\item The formula $\phi\in\mathcal{L}$ is \emph{true} (or \emph{satisfied})
		in the model $(\mathfrak{S},\mathcal{V})$ at the state $s\in\mathcal{S}$
			:iff $(\mathfrak{S},\mathcal{V}), s\models\phi$.
	%
	\item The formula $\phi$ is \emph{satisfiable} in the model $(\mathfrak{S},\mathcal{V})$
			:iff there is $s\in\mathcal{S}$ such that
				$(\mathfrak{S},\mathcal{V}), s\models\phi$.
	%
	\item The formula $\phi$ is \emph{globally true} (or \emph{globally satisfied})
		in the model $(\mathfrak{S},\mathcal{V})$,
			written $(\mathfrak{S},\mathcal{V})\models\phi$, :iff
				for all $s\in\mathcal{S}$, $(\mathfrak{S},\mathcal{V}),s\models\phi$.
	%
	\item The formula $\phi$ is \emph{satisfiable}
			:iff there is a model $(\mathfrak{S},\mathcal{V})$ and a state $s\in\mathcal{S}$ such that
				$(\mathfrak{S},\mathcal{V}),s\models\phi$.
	%
	\item The formula $\phi$ is \emph{valid}, written $\models\phi$, :iff
			for all models $(\mathfrak{S},\mathcal{V})$, $(\mathfrak{S},\mathcal{V})\models\phi$.
	\end{itemize}
\end{definition}
\noindent
The following lemma is a \emph{passage oblig\'{e}} in the construction of
	a Kripke-semantics for any intuitionistic logic, modal or not, and thus also for ours.
\begin{lemma}[Monotonicity Lemma]
	For all LIiP-models $(\mathfrak{S},\mathcal{V})$, $s,s'\in\mathcal{S}$, and $\phi\in\mathcal{L}$,
		if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi$
		then $(\mathfrak{S},\mathcal{V}),s'\models\phi$.
\end{lemma}
\begin{proof}
	Let $(\mathfrak{S},\mathcal{V})$ designate an arbitrary LIiP-model and let $s,s'\in\mathcal{S}$.
	%
	Then let us proceed by induction on the structure of $\phi\in\mathcal{L}:$
	\begin{itemize}
		\item Base case ($\phi\mathrel{:=} P$ for an arbitrary $P\in\mathcal{P}\subseteq\mathcal{L}$).
				%
				Suppose that $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models P$.
				%
				Thus $s\in\mathcal{V}(P)$, by definition.
				%
				Hence $s'\in\mathcal{V}(P)$, by the definitional constraint on $\mathcal{V}$.
				%
				Thus $(\mathfrak{S},\mathcal{V}),s'\models P$, by definition.
		\item Inductive steps:
			\begin{itemize}
				\item $\phi\mathrel{:=} \phi'\lor\phi''$ for arbitrary $\phi',\phi''\in\mathcal{L}$.
						%
						For the sake of the induction, suppose
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi'$ and
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi''$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi''$.
						%
						Further suppose that
							$s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'\lor\phi''$.
						%
						Thus
							$(\mathfrak{S},\mathcal{V}),s\models\phi'$ or
							$(\mathfrak{S},\mathcal{V}),s\models\phi''$, by definition.
						%
						Let us proceed by disjunctive case analysis:
						\begin{itemize}
							\item Suppose that $(\mathfrak{S},\mathcal{V}),s\models\phi'$.
									%
									Hence $(\mathfrak{S},\mathcal{V}),s'\models\phi'$, by induction hypothesis.
									%
									Hence
										$(\mathfrak{S},\mathcal{V}),s'\models\phi'$ or
										$(\mathfrak{S},\mathcal{V}),s'\models\phi''$, by
											meta-level (classical) propositional logic.
									%
									Thus
										$(\mathfrak{S},\mathcal{V}),s'\models\phi'\lor\phi''$, by definition.
							\item Suppose that $(\mathfrak{S},\mathcal{V}),s\models\phi''$, and
									proceed symmetrically to the previous case.
						\end{itemize}
				\item $\phi\mathrel{:=} \phi'\land\phi''$ for arbitrary $\phi',\phi''\in\mathcal{L}$.
						%
						For the sake of the induction, suppose
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi'$ and
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi''$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi''$.
						%
						Further suppose that
							$s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'\land\phi''$.
						%
						Thus
							$(\mathfrak{S},\mathcal{V}),s\models\phi'$ and
							$(\mathfrak{S},\mathcal{V}),s\models\phi''$, by definition.
						%
						Hence
							$(\mathfrak{S},\mathcal{V}),s'\models\phi'$ and
							$(\mathfrak{S},\mathcal{V}),s'\models\phi''$, by the induction hypotheses.
						%
						Thus
							$(\mathfrak{S},\mathcal{V}),s'\models\phi'\land\phi''$, by definition.
				\item $\phi\mathrel{:=} \neg\phi'$ for an arbitrary $\phi'\in\mathcal{L}$.
						%
						For the sake of the induction, suppose
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi'$.
						%
						Further suppose that
							$s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\neg\phi'$.
						%
						Thus
							for all $s''\in\mathcal{S}$,
								if $s\sqsubseteq s''$ then not $(\mathfrak{S},\mathcal{V}),s''\models\phi'$,
									by definition.
						%
						Now,
							let $s''\in\mathcal{S}$ and
							further suppose that $s'\sqsubseteq s''$.
						%
						Hence $s\sqsubseteq s''$, by the transitivity of $\sqsubseteq$.
						%
						Hence not $(\mathfrak{S},\mathcal{V}),s''\models\phi'$.
						%
						Hence for all $s''\in\mathcal{S}$,
							if $s'\sqsubseteq s''$ then not $(\mathfrak{S},\mathcal{V}),s''\models\phi'$.
						%
						Thus $(\mathfrak{S},\mathcal{V}),s'\models\neg\phi'$, by definition.
						%
						(Observe that
							the induction hypothesis turns out to be irrelevant for this case.)
				\item $\phi\mathrel{:=} \phi'\rightarrow\phi''$ for arbitrary $\phi',\phi''\in\mathcal{L}$.
						%
						For the sake of the induction, suppose
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi'$ and
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi''$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi''$.
						%
						Further suppose that
							$s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'\rightarrow\phi''$.
						%
						Thus
							for all $s''\in\mathcal{S}$,
								if $s\sqsubseteq s''$ then
									(not $(\mathfrak{S},\mathcal{V}),s''\models\phi'$ or
									$(\mathfrak{S},\mathcal{V}),s''\models\phi''$), by definition.
						%
						Now,
							let $s''\in\mathcal{S}$ and
							further suppose that $s'\sqsubseteq s''$.
						%
						Hence $s\sqsubseteq s''$, by the transitivity of $\sqsubseteq$.
						%
						Hence,
							not $(\mathfrak{S},\mathcal{V}),s''\models\phi'$ or
							$(\mathfrak{S},\mathcal{V}),s''\models\phi''$.
						%
						Hence for all $s''\in\mathcal{S}$,
							if $s'\sqsubseteq s''$
							then (not $(\mathfrak{S},\mathcal{V}),s''\models\phi'$ or
										$(\mathfrak{S},\mathcal{V}),s''\models\phi''$).
						%
						Thus $(\mathfrak{S},\mathcal{V}),s'\models\phi'\rightarrow\phi''$, by definition.
						%
						(Observe that
							the induction hypotheses turn out to be irrelevant for this case.)
				\item $\phi\mathrel{:=} \Iproves{M}{\phi'}{\mathtt{CM}}{}$ for an arbitrary $\phi'\in\mathcal{L}$.
						%
						For the sake of the induction, suppose
							that
								if $s\sqsubseteq s'$ and $(\mathfrak{S},\mathcal{V}),s\models\phi'$
								then $(\mathfrak{S},\mathcal{V}),s'\models\phi'$.
						%
						Further suppose that
							$s\sqsubseteq s'$ and
							$(\mathfrak{S},\mathcal{V}),s\models\Iproves{M}{\phi'}{\mathtt{CM}}{}$.
						%
						Thus on the one hand,
							$s\access{\mathtt{CM}}{\mathtt{CM}}{}s'$, by MIAR-inclusion, and
						also, on the other hand,
							for all $s''\in\mathcal{S}$,
								if $s\access{M}{\mathtt{CM}}{}s''$
								then $(\mathfrak{S},\mathcal{V}),s''\models\phi'$,
									by definition.
						%
						Now,
							let $s''\in\mathcal{S}$ and
							further suppose that $s'\access{M}{\mathtt{CM}}{}s''$.
						%
						Hence $s\access{M}{\mathtt{CM}}{}s''$, by special transitivity.
						%
						Hence $(\mathfrak{S},\mathcal{V}),s''\models\phi'$.
						%
						(Observe that
							the induction hypothesis turns out to be irrelevant for this case.)
			\end{itemize}
	\end{itemize}
\end{proof}
\noindent
Observe that
	the induction hypothesis in the proof turns out to be irrelevant for
		all negative connectives and the modality, which
			are made to conserve the monotonicity of atomic propositions
				(cf.\  Page~\pageref{page:Monotonicity}).

\begin{proposition}[Concrete LIiP-models]\label{proposition:InputHistoryModel}\
	Let $\mathfrak{M}$ designate an arbitrary concrete LIiP-model, i.e.,\xspace a model with
		ingredients like in Definition~\ref{definition:SemanticIngredients}, and
	let $\phi\in\mathcal{L}$.

	Then,
		$$\text{$\mathfrak{M},\mathtt{0}\models\phi$ if and only if $\mathfrak{M}\models\phi$\,.}$$
\end{proposition}
\begin{proof}
	The only-if direction follows from the definition of global satisfaction (cf.\  Definition~\ref{definition:TruthValidity}).
	For the if-direction,
		consider that the concrete state space $\mathcal{S}=\setst{s\in\mathcal{S}}{\mathtt{0}\sqsubseteq s}$ and
		apply the antecedent Monotonicity Lemma.
\end{proof}

\begin{proposition}[Admissibility of LIiP-specific axioms and rules]\label{proposition:AxiomAndRuleAdmissibility}\
	\begin{enumerate}
		\item $\models\knows{a}{a}$
		\item $\models(\knows{a}{M}\land\knows{a}{M'})\leftrightarrow\knows{a}{\pair{M}{M'}}$
		\item $\models\Iproves{M}{\knows{\mathtt{CM}}{M}}{\mathtt{CM}}{}$
		\item $\models(\Iproves{M}{(\phi\rightarrow\phi')}{\mathtt{CM}}{})\rightarrow
				((\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi'}{\mathtt{CM}}{})$
		\item $\models(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow(\knows{\mathtt{CM}}{M}\rightarrow\phi)$
		\item $\models(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow(\Iproofdiamond{M}{\phi}{\mathtt{CM}}{})$
		\item $\models\phi\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$
		\item If $\models\phi$ then $\models\Iproves{M}{\phi}{\mathtt{CM}}{}$
		\item If $\models\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'}$ then
					$\models(\Iproves{M'}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$.
	\end{enumerate}
\end{proposition}
\begin{proof}
	1 and 2 are immediate;
	4 and 8 hold by the fact that LIiP has a standard Kripke-semantics;
	3 follows directly from the epistemic-image property of $\access{M}{\mathtt{CM}}{}$,
	5 from the conditional reflexivity of $\access{M}{\mathtt{CM}}{}$, and
	9 from the proof-monotonicity property of $\access{M}{\mathtt{CM}}{}$.
	%
	6 follows from
		the seriality of $\access{M}{\mathtt{CM}}{}$ and
		the MIAR-inclusion and
		the epistemic-image property of $\access{M}{\mathtt{CM}}{}$ as follows:
		%
		Let $(\mathfrak{S},\mathcal{V})$ designate an arbitrary LIiP-model and let $s\in\mathcal{S}$.
		Further let $s'\in\mathcal{S}$ and suppose that $s\sqsubseteq s'$.
		Now suppose that $(\mathfrak{S},\mathcal{V}),s'\models\Iproves{M}{\phi}{\mathtt{CM}}{}$.
		%
		Further let $s''\in\mathcal{S}$ and suppose that $s'\sqsubseteq s''$.
		%
		Hence $(\mathfrak{S},\mathcal{V}),s''\models\Iproves{M}{\phi}{\mathtt{CM}}{}$ by the Monotonicity Lemma.
		%
		That is,
			for all $s'''\in\mathcal{S}$,
				if $s''\access{M}{\mathtt{CM}}{}s'''$ then $(\mathfrak{S},\mathcal{V}),s'''\models\phi$.
		%
		But by the seriality of $\access{M}{\mathtt{CM}}{}$,
			there is indeed an $s'''\in\mathcal{S}$ such that $s''\access{M}{\mathtt{CM}}{}s'''$.
		Hence,
			$(\mathfrak{S},\mathcal{V}),s'''\models\phi$, and also
			$s''\sqsubseteq s'''$ by the MIAR-inclusion property, and yet also
			$M\in\clo{\mathtt{CM}}{s'''}(\emptyset)$ by the epistemic-image property.
		Thus $(\mathfrak{S},\mathcal{V}),s'''\models\knows{\mathtt{CM}}{M}\land\phi$.
		Hence $(\mathfrak{S},\mathcal{V}),s'\models\neg\neg(\knows{\mathtt{CM}}{M}\land\phi)$ and
		thus $(\mathfrak{S},\mathcal{V}),s\models(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\neg\neg(\knows{\mathtt{CM}}{M}\land\phi)$.
	%
	Finally,
		7 follows from
			the MIAR-inclusion property of $\access{M}{\mathtt{CM}}{}$ and
			the Monotonicity Lemma (which in turn holds thanks to
				the special transitivity and the MIAR-inclusion property of $\access{M}{\mathtt{CM}}{}$) as follows:
		%
		Let $(\mathfrak{S},\mathcal{V})$ designate an arbitrary LIiP-model and let $s\in\mathcal{S}$.
		Further let $s'\in\mathcal{S}$ and suppose that $s\sqsubseteq s'$.
		Now suppose that $(\mathfrak{S},\mathcal{V}),s'\models\phi$.
		Additionally, let $s''\in\mathcal{S}$ and suppose that $s'\access{M}{\mathtt{CM}}{}s''$.
		Hence $s'\sqsubseteq s''$ by MIAR-inclusion.
		Hence $(\mathfrak{S},\mathcal{V}),s''\models\phi$ by the Monotonicity Lemma.
		Thus,
			$(\mathfrak{S},\mathcal{V}),s'\models\Iproves{M}{\phi}{\mathtt{CM}}{}$, and then
			$(\mathfrak{S},\mathcal{V}),s\models\phi\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}$.
\end{proof}

\begin{theorem}[Axiomatic adequacy]\label{theorem:Adequacy}\
	$\vdash_{\LIiP}$ is \emph{adequate} for $\models$, i.e.,\xspace:
	\begin{enumerate}
		\item if $\vdash_{\LIiP}\phi$ then $\models\phi$\quad(axiomatic soundness)
		\item if $\models\phi$ then $\vdash_{\LIiP}\phi$\quad(semantic completeness).
	\end{enumerate}
\end{theorem}
\begin{proof}
	Both parts can be proved with standard means:
	%
	axiomatic soundness follows from
		the admissibility of the axioms and rules
			(cf.\  Propostion~\ref{proposition:AxiomAndRuleAdmissibility}) as usual, and
	semantic completeness follows by means of a construction of canonical models that
		is appropriate for intuitionistic normal modal logic as follows.

	Let
		\begin{itemize}
			\item $\mathcal{W}$ designate the set of all prime LIiP-consistent sets\footnote{*
				A set $W$ of LIiP-formulas is prime LIiP-consistent :iff
					$W$ is LIiP-consistent and
					$W$ is prime.
				%
				A set $W$ of LIiP-formulas is LIiP-consistent :iff
					$W$ is not LIiP-inconsistent.
				%
				A set $W$ of LIiP-formulas is LIiP-inconsistent :iff
					there is a finite $W'\subseteq W$ such that $((\bigwedge W')\rightarrow\text{false})\in\mathrm{LIiP}$.
				%
				A set $W$ of LIiP-formulas is prime :iff
						first, $W$ is deductively closed, that is,
							there is a finite $W'\subseteq W$ such that
								for all $\phi\in\mathcal{L}$,
									if $((\bigwedge W')\rightarrow\phi)\in\mathrm{LIiP}$ then $\phi\in W$, and
						second, $W$ has the disjunction property, that is,
							for all $\phi,\phi'\in\mathcal{L}$,
								if $\phi\lor\phi'\in W$
								then $\phi\in W$ or $\phi'\in W$.
				%
				Similar to a classical Lindenbaum construction
					(extending consistent sets to \emph{maximal} consistent sets)
						any LIiP-consistent set can be extended to
							a \emph{prime} LIiP-consistent set.}
			\item $w\sqsubseteq w'$ :iff $w\subseteq w'$
			\item for all $w,w'\in\mathcal{W}$,
				$w\canrel{M}{\mathtt{CM}}{}w'$ :iff $\setst{\phi\in\mathcal{L}}{\Iproves{M}{\phi}{\mathtt{CM}}{}\in w}\subseteq w'$
			\item for all $w\in\mathcal{W}$, $w\in\mathcal{V}_{\mathsf{C}}(P)$ :iff $P\in w$.
		\end{itemize}
	Then
		$\mathfrak{M}_{\mathsf{C}}\mathrel{:=}
			(\mathcal{W},\sqsubseteq,\set{\canrel{M}{\mathtt{CM}}{}}_{M\in\mathcal{M}},\mathcal{V}_{\mathsf{C}})$
		designates the \emph{canonical model} for LIiP.

	Following standard practice common to all intuitionistic normal modal logics,
		the following useful property of $\mathfrak{M}_{\mathsf{C}}$,
			the so-called \emph{Truth Lemma,}
			$$\text{for all $\phi\in\mathcal{L}$ and $w\in\mathcal{W}$,
				$\phi\in w$ if and only if $\mathfrak{M}_{\mathsf{C}},w\models\phi$}$$
		can be proved by induction on the structure of $\phi$.

	With this lemma,
		it can then be proved that
			for all $\phi\in\mathcal{L}$,
				if $\not\vdash_{\LIiP}\phi$ then $\not\models\phi$.
	%
	Let
		$\phi\in\mathcal{L}$, and
	suppose that
		$\not\vdash_{\LIiP}\phi$.
	%
	Thus,
		$\set{\neg\phi}$
			is LIiP-consistent, and
			can be extended to a prime LIiP-consistent set $w$, i.e.,\xspace
				$\neg\phi\in w\in\mathcal{W}$.
	%
	Hence
		$\mathfrak{M}_{\mathsf{C}},w\models\neg\phi$, by the Truth Lemma.
	%
	Thus:
		$\mathfrak{M}_{\mathsf{C}},w\not\models\phi$,
		$\mathfrak{M}_{\mathsf{C}}\not\models\phi$, and
		$\not\models\phi$.
	%
	That is,
			$\mathfrak{M}_{\mathsf{C}}$ is a
				\emph{universal} (for \emph{all} $\phi\in\mathcal{L}$)
				\emph{counter-model} (if $\phi$ is a non-theorem then $\mathfrak{M}_{\mathsf{C}}$ falsifies $\phi$).

	The only proof obligation specific to the semantic-completeness proof for LIiP is to prove that
		$\mathfrak{M}_{\mathsf{C}}$ is also an \emph{LIiP-model}.
	%
	So let us instantiate our data-mining operator $\clo{a}{}$ (cf.\  Page~\pageref{page:DataMining}) on $\mathcal{W}$
		by letting for all $w\in\mathcal{W}$
			$$\msgs{a}(w)\mathrel{:=}\setst{M}{\knows{a}{M}\in w},$$ and let us prove that:
					\begin{enumerate}
				\item If $w\canrel{M}{\mathtt{CM}}{}w'$ then $M\in\clo{\mathtt{CM}}{w'}(\emptyset)$
				\item If $M\in\clo{\mathtt{CM}}{w}(\emptyset)$ then
						$w\canrel{M}{\mathtt{CM}}{}w$
				\item there is $w'\in\mathcal{W}$ such that $w\canrel{M}{\mathtt{CM}}{}w'$
				\item ${\canrel{M}{\mathtt{CM}}{}}\subseteq{\canrel{\mathtt{CM}}{\mathtt{CM}}{}}={\sqsubseteq}$
				\item $({\canrel{\mathtt{CM}}{\mathtt{CM}}{}}\circ{\canrel{M}{\mathtt{CM}}{}})\subseteq{\canrel{M}{\mathtt{CM}}{}}$
				\item If $M\sqsubseteq_{\mathtt{CM}}M'$
						then ${\canrel{M}{\mathtt{CM}}{}}\subseteq{\canrel{M'}{\mathtt{CM}}{}}$
					\end{enumerate}
	For (1),
		let $w,w'\in\mathcal{W}$ and
		suppose that $w\canrel{M}{\mathtt{CM}}{}w'$.
	%
	That is,
		for all $\phi\in\mathcal{L}$,
			if $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$
			then $\phi\in w'$.
	%
	Since $w$ is deductively closed,
		$$\text{$\Iproves{M}{\knows{\mathtt{CM}}{M}}{\mathtt{CM}}{}\in w$\quad(self-knowledge).}$$
	%
	Hence
		$\knows{\mathtt{CM}}{M}\in w'$.
	%
	Thus
		$M\in\clo{\mathtt{CM}}{w'}(\emptyset)$ by the definition of $\clo{\mathtt{CM}}{w'}$.

	For (2),
		let $w\in\mathcal{W}$ and
		suppose that
			$M\in\clo{\mathtt{CM}}{w}(\emptyset)$.
	%
	Hence $\knows{\mathtt{CM}}{M}\in w$ due to the deductive closure of $w$.
	%
	Further suppose that $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$.
	%
	Since $w$ is deductively closed,
		$$\text{$(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow(\knows{\mathtt{CM}}{M}\rightarrow\phi)\in w$\quad(ET).}$$
	%
	Hence,
		$\knows{\mathtt{CM}}{M}\rightarrow\phi\in w$, and
		$\phi\in w$, by consecutive  \emph{modus ponens.}

	For (3),
		let $w\in\mathcal{W}$ and $\phi\in\mathcal{L}$, and
		suppose that $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$.
	%
	Since $w$ is deductively closed,
		$$\text{$(\Iproves{M}{\phi}{\mathtt{CM}}{})\rightarrow\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}\in w$\quad(ID).}$$
	%
	Hence, $\Iproofdiamond{M}{\phi}{\mathtt{CM}}{}\in w$ by \emph{modus ponens.}
	%
	That is,
		$\neg\neg(\knows{\mathtt{CM}}{M}\land\phi)\in w$ by definition.
	%
	Since $w$ is deductively closed,
		$\neg\neg(\knows{\mathtt{CM}}{M}\land\phi)\rightarrow\neg\neg\phi\in w$.
	%
	Hence
		$\neg\neg\phi\in w$ by \emph{modus ponens.}
	%
	Hence $\mathfrak{M}_{\mathsf{C}}, w\models\neg\neg\phi$ by the Truth Lemma.
	%
	Hence for all $w'\in\mathcal{W}$,
		if $w\sqsubseteq w'$ then
		there is $w''\in\mathcal{W}$ such that
			$w'\sqsubseteq w''$ and
			$\mathfrak{M}_{\mathsf{C}}, w''\models\phi$ by definition.
	%
	Hence $\phi\in w''$ by the Truth Lemma.

	For (4),
		let us first prove that ${\canrel{\mathtt{CM}}{\mathtt{CM}}{}}={\sqsubseteq}$\,.
	%
	So let $w,w'\in\mathcal{W}$ and
	suppose that $w\canrel{\mathtt{CM}}{\mathtt{CM}}{}w'$.
	%
	That is,
		for all $\phi\in\mathcal{L}$,
			if $\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}\in w$
			then $\phi\in w'$.
	Further
		let $\phi\in\mathcal{L}$ and
		suppose that $\phi\in w$.
	%
	Hence if $\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}\in w$ then $\phi\in w'$.
	%
	Since $w$ is deductively closed,
		$$(\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{})\leftrightarrow\phi\in w\quad\text{(TMM)}$$
	%
	Hence $\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}\in w$ by LIiP-\emph{modus ponens}.
	%
	Hence $\phi\in w'$ by meta-level \emph{modus ponens}.
	%
	Thus $w\subseteq w'$, and then $w\sqsubseteq w'$.
	%
	Conversely, suppose that $w\sqsubseteq w'$.
	%
	That is, $w\subseteq w'$.
	%
	Further
		let $\phi\in\mathcal{L}$ and
		suppose that $\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}\in w$.
	%
	Hence $\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}\in w'$.
	%
	Since $w'$ is deductively closed,
		$$(\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{})\leftrightarrow\phi\in w'\quad\text{(TMM)}$$
	%
	Hence $\phi\in w'$ by LIiP-\emph{modus ponens}.
	%
	Second, let us prove that ${\canrel{M}{\mathtt{CM}}{}}\subseteq{\canrel{\mathtt{CM}}{\mathtt{CM}}{}}$\,.
	%
	So let $w,w'\in\mathcal{W}$ and
	suppose that $w\canrel{M}{\mathtt{CM}}{}w'$.
	%
	That is,
		for all $\phi\in\mathcal{L}$,
			if $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$
			then $\phi\in w'$.
	Further
		let $\phi\in\mathcal{L}$ and
		suppose that $\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}\in w$.
	%
	Since $w$ is deductively closed,
		$$(\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{})\leftrightarrow\phi\in w\quad\text{(TMM)}$$
	%
	Hence $\phi\in w$ by LIiP-\emph{modus ponens}.
	%
	Since $w$ is deductively closed,
		$$\phi\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}\in w\quad\text{(MM)}$$
	%
	Hence $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$ by LIiP-\emph{modus ponens}.
	%
	Hence $\phi\in w'$ by meta-level \emph{modus ponens}.

	For (5),
		let $w,w'\in\mathcal{W}$ and
		suppose that $w\mathrel{(\canrel{\mathtt{CM}}{\mathtt{CM}}{}\circ\canrel{M}{\mathtt{CM}}{})}w'$.
	%
	That is,
		there is $w''\in\mathcal{W}$ such that
			$w\canrel{\mathtt{CM}}{\mathtt{CM}}{}w''$ and
			$w''\canrel{M}{\mathtt{CM}}{}w'$.
	%
	Thus,
		(for all $\phi\in\mathcal{L}$,
			if $\Iproves{\mathtt{CM}}{\phi}{\mathtt{CM}}{}\in w$
			then $\phi\in w''$) and
		(for all $\phi\in\mathcal{L}$,
			if $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w''$
			then $\phi\in w'$).
	%
	Further let $\phi\in\mathcal{L}$ and suppose that $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$.
	%
	Since $w$ is deductively closed,
		$$(\Iproves{\mathtt{CM}}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\leftrightarrow
			\Iproves{M}{\phi}{\mathtt{CM}}{}\in w\quad\text{(TMM)}$$
	%
	Hence $(\Iproves{\mathtt{CM}}{(\Iproves{M}{\phi}{\mathtt{CM}}{})}{\mathtt{CM}}{})\in w$.
	%
	Hence $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w''$ by the first hypothesis.
	%
	Hence $\phi\in w'$ by the second hypothesis.
	%
	Thus $w\canrel{M}{\mathtt{CM}}{}w'$.

	For (6),
		suppose that
			$M\sqsubseteq_{\mathtt{CM}}M'$.
	%
	That is,
		for all $w\in\mathcal{W}$,
			if $M\in\clo{\mathtt{CM}}{w}(\emptyset)$ then $M'\in\clo{\mathtt{CM}}{w}(\emptyset)$.
	%
	Hence for all $w\in\mathcal{W}$,
		if $\knows{\mathtt{CM}}{M}\in w$ then $\knows{\mathtt{CM}}{M'}\in w$
				due to the deductive closure of $w$, which
					contains all the term axioms corresponding to the defining clauses of $\clo{\mathtt{CM}}{w}$.
	%
	Hence for all $w\in\mathcal{W}$,
			if $\mathfrak{M}_{\mathsf{C}}, w\models\knows{\mathtt{CM}}{M}$ then $\mathfrak{M}_{\mathsf{C}}, w\models\knows{\mathtt{CM}}{M'}$, by the Truth Lemma.
	%
	Hence also,
		for all $w\in\mathcal{W}$, $\mathfrak{M}_{\mathsf{C}}, w\models\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'}$ by
			the definition of $\sqsubseteq$.
	%
	Hence for all $w\in\mathcal{W}$,
		$\knows{\mathtt{CM}}{M}\rightarrow\knows{\mathtt{CM}}{M'}\in w$ by the Truth Lemma.
	%
	Hence the following intermediate result, called IR,
			$$\text{for all $w\in\mathcal{W}$ and $\phi\in\mathcal{L}$,
			$(\Iproves{M'}{\phi}{\mathtt{CM}}{})\rightarrow\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$,}$$ by EA.
	%
	Now,
		let $w,w'\in\mathcal{W}$ and
		suppose that $w\canrel{M}{\mathtt{CM}}{}w'$.
	%
	That is,
		for all $\phi\in\mathcal{L}$,
			if $\Iproves{M}{\phi}{\mathtt{CM}}{}\in w$
			then $\phi\in w'$.
	%
	Hence,
		for all $\phi\in\mathcal{L}$,
					if $\Iproves{M'}{\phi}{\mathtt{CM}}{}\in w$
					then $\phi\in w'$ by IR.
	%
	Hence $w\canrel{M'}{\mathtt{CM}}{}w'$ by definition.
\end{proof}

\begin{theorem}[Finite-model property]\label{theorem:FiniteModelProperty}
	For any LIiP-model $\mathfrak{M}$,
	if $\mathfrak{M}, s\models\phi$
	then there is a finite LIiP-model $\mathfrak{M}_{\mathrm{fin}}$ such that
		$\mathfrak{M}_{\mathrm{fin}}, s\models\phi$.
\end{theorem}
\begin{proof}
	By the fact that
		the \emph{minimal filtration} \cite{ModalModelTheory}
			$$\mathfrak{M}_{\mathrm{flt}}^{\mathrm{min},\Gamma}\mathrel{:=}
				(\mathcal{S}/_{\sim_{\Gamma}},
					\sqsubseteq^{\mathrm{min},\Gamma},
					\set{\access{M}{\mathtt{CM}}{\mathrm{min},\Gamma}}_{M\in\mathcal{M}},\mathcal{V}_{\Gamma})$$ of
			any LIiP-model $\mathfrak{M}\mathrel{:=}(\mathcal{S},\sqsubseteq,\set{\access{M}{\mathtt{CM}}{}}_{M\in\mathcal{M}},\mathcal{V})$
			through a finite $\Gamma\subseteq\mathcal{L}$ is a finite LIiP-model such that
				for all $\gamma\in\Gamma$,
					$\mathfrak{M},s\models\gamma$ if and only if
					$\mathfrak{M}_{\mathrm{flt}}^{\mathrm{min},\Gamma},[s]_{\sim_{\Gamma}}\models\gamma$.
			%
			Following \cite{ModalModelTheory} for our setting,
				we define
				\begin{eqnarray*}
					{\sim_{\Gamma}}&\mathrel{:=}&
						\setst{(s,s')\in\mathcal{S}\times\mathcal{S}}{\text{for all $\gamma\in\Gamma$,
							$\mathfrak{M},s\models\gamma$ iff $\mathfrak{M},s'\models\gamma$}}\\
					{\sqsubseteq^{\mathrm{min},\Gamma}} &\mathrel{:=}&
						\setst{([s]_{\sim_{\Gamma}},[s']_{\sim_{\Gamma}})}{(s,s')\in{\sqsubseteq}}\\
					{\access{M}{\mathtt{CM}}{\mathrm{min},\Gamma}} &\mathrel{:=}&
						\setst{([s]_{\sim_{\Gamma}},[s']_{\sim_{\Gamma}})}{(s,s')\in{\access{M}{\mathtt{CM}}{}}}\\
					\mathcal{V}_{\Gamma}(P)&\mathrel{:=}&
							\setst{[s]_{\sim_{\Gamma}}}{s\in\mathcal{V}(P)}\,.
				\end{eqnarray*}
			We further fix
				$M\in\clo{\mathtt{CM}}{[s]_{\sim_{\Gamma}}}(\emptyset)$ :iff
				$[s]_{\sim_{\Gamma}}\in\mathcal{V}_{\Gamma}(\knows{\mathtt{CM}}{M})$, and
				choose $\Gamma$ to be the (finite) sub-formula closure of $\phi$.
			%
			Hence, we are left to prove that
				$\mathfrak{M}_{\mathrm{flt}}^{\mathrm{min},\Gamma}$ is indeed an LIiP-model, which
				means that we are left to prove that
						$\sqsubseteq^{\mathrm{min},\Gamma}$ and ${\access{M}{a}{\mathrm{min},\Gamma}}$ have
					all the properties stipulated by the semantic interface of LIiP;
					this is straightforward and therefore relegated to
						Appendix~\ref{appendix:FiniteModelProperty}.
\end{proof}

\begin{corollary}[Algorithmic decidability]\label{corollary:AlgorithmicDecidability}
	LIiP is algorithmically decidable.
\end{corollary}
\begin{proof}
	In order to algorithmically decide whether or not $\phi\in\mathrm{LIiP}$
	(that is, $\vdash_{\LIiP}\phi$) for some $\phi\in\mathcal{L}$ (and the current choice of $\mathcal{M}$),
		axiomatic adequacy allows us to check whether or not $\neg\phi$ is locally satisfiable (That is,
			whether or not $\mathfrak{M},s\models\neg\phi$ for
				some LIiP-model $\mathfrak{M}$ and state $s$.
					Also, $M\in\clo{\mathtt{CM}}{s}(\emptyset)$ on the currently chosen
						message language $\mathcal{M}$ is obviously decidable;
						for other, more complex message languages including cryptographic messages,
							see for example \cite{TGJ} and \cite{BaskarJamSuresh2010}).
	%
	But then, the finite-model property of LIiP allows us
		to enumerate all finite LIiP-models $\mathfrak{M}_{\mathrm{fin}}$ up to a size of at most 2 to the power
			of the size $n$ of the sub-formula closure of $\neg\phi$ and
		to check whether or not $\mathfrak{M}_{\mathrm{fin}},s\models\neg\phi$.
	%
	(First, there are at most $2^n$ equivalence classes for $n$ formulas.
	 Second,
		checking intuitionistic negation, which
			is checking classical negation within the up-set of the state $s$ with respect to $\sqsubseteq$,
				within a finite model is also a finite task.)
\end{proof}
Note that
	the algorithmic complexity of LIiP will depend on
		the specific choice of $\mathcal{M}$ and the correspondingly chosen term axioms.

\section{Conclusion}
We have produced LIiP from LiP with
	as main contributions those described in Section~\ref{section:Contribution}.
In future work,
	we shall work out
	dynamic and first-order extensions of LIiP.
As roughly related work,
	we
		have already mentioned \cite{LIPArtemov}
			(cf.\  Page~\pageref{page:LIP:1},
						\pageref{page:LIP:2},
						\pageref{page:LIP:4}, and

						\pageref{page:LIP:7}) and
		can further mention
			\cite{PouliasisPrimieroIMLA2013} and
			\cite{SterenBonelliIMLA2013}.
In \cite{PouliasisPrimieroIMLA2013},
	a fragment of an intuitionistic version of the minimal Justification Logic \cite{JustificationLogic} (mJL) is introduced in
		the context of an ambitious Curry-Howard isomorphism for modular programming.
A similar appreciation can be made of \cite{SterenBonelliIMLA2013}, which
	introduced an intuitionistic fragment of
		the Logic of (non-interactive) Proofs (extending mJL) \cite{LIPArtemov}.
The main contribution of
	\cite{PouliasisPrimieroIMLA2013} as well as \cite{SterenBonelliIMLA2013} seems to be
		a programming calculus for an axiomatically defined intuitionistic modal logic rather than
			logic itself, whereas
		ours is an intuitionistic modal logic
			with an axiomatics and a set-theoretically constructive semantics.

\paragraph{Acknowledgements}
I thank Olga Grinchtein for spotting a few typos.

\bibliographystyle{alpha}