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+q$ to infer that $\square p \rightarrow \square p + \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.)

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.)

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?

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+q$ to infer that $\square p \rightarrow \square p + \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.)