Skip to main content
1 of 3
Emil Jeřábek
  • 47.1k
  • 4
  • 147
  • 208

$\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.

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$) for every variable in the proof 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 $$M,e'\models\theta(C)\iff M,e_0\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$.

Emil Jeřábek
  • 47.1k
  • 4
  • 147
  • 208