\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}

