Let S be a propositional modal logic system (extension of K, or even E) with a single unary modal operator and defined by a single non-iterative axiom (i.e. of modal degree 1). 


Is it true that for such a system S, every theorem that is a non-iterative formula has a proof consisting only of non-iterative formulas? 


If yes, can anyone provide a reference where I can find this result?  

If no, can you provide a counterexample?


EDIT: Adding clarification of where this comes from.


Denote by P the property in question. A slightly stronger property P' requires all the formulas in the proof to also not exceed N propositional variables, where N is the maximum between the number of variables in the non-iterative axiom and the number of variables in the non-iterative theorem to prove. So basically we are trying to prove a theorem without increasing the modal degree nor the number of propositional variables during the proof (with a possible exception for PC formulas; for example one may use $p \rightarrow p \lor q$ to infer that $\square p \rightarrow \square p \lor \lozenge p$ and this would not count as an increase in the number of variables).


It looks like for a system defined by a combination of iterative and non-iterative axioms these properties do not hold (universally). For example, see Hughes and Cresswell pp 58, in order to prove $\square p\rightarrow \square \square p$ in S5, one must use formulas of modal degree 3 during the proof. The same thing appears to be the case when proving that T+B+S4 implies S5. I also suspect that increasing the number of variables does not help in avoiding the increase in modal degree in these cases, therefore the distinction between P and P'. 


However, P and even P' seem to hold for non-iterative systems. Given that these systems are relatively simple (i.e. they have FMP and a number of other "nice" properties), I was thinking that P and/or P' may be known results, but I cannot find them.


An algebraic explanation would be interesting for me too. (But I do not see a tag for algebraic-logic.)



Non-iterative modal logics
$\let\ET\bigwedge\let\LOR\bigvee\let\EQ\Leftrightarrow$The property is true for extensions of K (i.e., normal modal logics). You didn’t really describe the proof system you are interested in, but based on the discussion in the question, I will assume it is a Hilbert-style proof system with the rules of modus ponens and necessitation, and substitution instances of a fixed set of axioms, including a complete axiomatization of classical propositional logic, and the distributivity axiom of K. (It seems that you also allow substitution to be used as a rule. I prefer the formulation I gave with no substitution rule, but axioms schemata closed under substitution, because it has nicer structural properties. Of course, one can simulate schemata in the other system by an explicit application of substitution on the base form of the axiom.)


First, note that the “stronger property” putting a bound on the number of variables is trivially equivalent to the original formulation: given a proof of a formula $A$, you can uniformly substitute a fixed formula (e.g., $\bot$ if it’s in the language, or a variable from $A$) in all formulas in the proof for each variable which does not occur in $A$, obtaining a proof of $A$ which only involves variables from $A$.


Let me define a *Boolean substitution* to be a substitution $\sigma$ such that $\sigma(p)$ is a Boolean formula (i.e., $\Box$-free) for every variable $p$.



> 
> **Theorem:** Let $S\cup\{A\}$ be a set of formulas of modal degree $\le1$. If $\vdash\_{\mathrm K\oplus S}A$, then $A$ has a derivation using
> 
> 
> 1. (degree-$1$ instances of) classical propositional tautologies, and the rule of modus ponens,
> 2. axioms $\Box B$, where $B$ is a $\Box$-free classical tautology, and Boolean substitution instances of $\Box(p\to q)\to(\Box p\to\Box q)$,
> 3. Boolean substitution instances of $B\in S$.
> 
> 
> Moreover, all formulas in the proof use only variables occurring in $A$.
> 
> 
> 


**Proof:**
Assume that the conclusion fails. Unless stated otherwise, all formulas below are required to use only the variables from $A$. By the completeness of classical propositional logic, there exists a Boolean assignment $v$ to variables and boxed Boolean formulas such that $v(A)=0$, but $v(B)=1$ for every axiom of type (2), (3). We will construct a Kripke model based on an $S$-frame where $A$ is false.


Let $\{p\_0,\dots,p\_{n-1}\}$ be an enumeration of all variables occurring in $A$, and if $e$ is any Boolean assignment $e\colon\{p\_i:i<n\}\to\{0,1\}$, put
$$p^e:=\ET\_{e(p\_i)=1}p\_i\land\ET\_{r(p\_i)=0}\neg p\_i.$$
We can write an arbitrary Boolean formula $B$ in the full conjunctive normal form
$$\vdash\_{\mathrm{CPC}}B\leftrightarrow\ET\_{e(B)=0}\neg p^e.$$
Since $v$ makes true all axioms of type (2), we have
$$\tag{$\*$}v(\Box B)=v\Bigl(\ET\_{e(B)=0}\Box\neg p^e\Bigr).$$
Let $e\_0$ be the restriction of $v$ to variables, and put
$$E=\{e:v(\Box\neg p^e)=0\}.$$
Define a Kripke model $M=\langle W,R,\models\rangle$ by
\begin{align\*}
W&=E\cup\{e\_0\},\\
e\mathrel R e'&\EQ\begin{cases}
 e'\in E&\text{if $e=e\_0$,}\\
 e=e'&\text{otherwise,}
\end{cases}\\
e\models p\_i&\EQ e(p\_i)=1.
\end{align\*}
In other words, $M$ is a tree of height $\le2$ with root $e\_0$, and reflexive leaves $e\in E\smallsetminus\{e\_0\}$. The root is reflexive iff $e\_0\in E$. It follows immediately from $(\*)$ and the definition that
$$\tag{$\*{\*}$}v(B)=1\iff M,e\_0\models B$$
for every formula $B$ of degree $\le1$, in particular $M,e\_0\nvDash A$.


It remains to verify that $\langle W,R\rangle$ is an $S$-frame. Since every subset $X\subseteq W$ is definable by a Boolean formula in $M$ (namely, $\LOR\_{e\in X}p^e$), it suffices to show that $M$ satisfies all Boolean substitution instances of $S$-axioms. Every such instance $B$ is an axiom of the type (3), hence $(\*\*)$ gives immediately that $M,e\_0\models B$. In order to verify $M,e\models B$ for $e\ne e\_0$, let $\theta$ be the Boolean substitution
$$\theta(p\_i)=\begin{cases}\top&\text{if $e(p\_i)=1$,}\\\bot&\text{otherwise.}\end{cases}$$
Then
$$\tag{$\*{\*}{\*}$}M,e'\models\theta(C)\iff M,e\models C$$
for every $e'\in W$ and every formula $C$ by induction on the complexity of $C$. (The induction step for $\Box$ needs that $e\_0$ has a successor, i.e., $E$ is nonempty. This follows from the assumption $e\ne e\_0$.) Since we already know that $M,e\_0\models\theta(B)$, we obtain $M,e\models B$ by taking $C=B$ and $e'=e\_0$ in $(\*{\*}\*)$.


