Abstract

A logic |$\mathcal{L}$| is said to satisfy the descending chain condition, DCC, if any descending chain of formulas in |$\mathcal{L}$| with ordering induced by |$\vdash _{\mathcal{L}};$| eventually stops. In this short note, we first establish a general theorem, which states that if a propositional logic |$\mathcal{L}$| satisfies both DCC and has the Craig Interpolation Property, CIP, then it satisfies the Uniform Interpolation Property, UIP, as well. As a result, by using the Nishimura lattice, we give a new simply proof of uniform interpolation for |$\textbf{IPL}_2$|⁠, the two-variable fragment of Intuitionistic Propositional Logic; and one-variable uniform interpolation for |$\textbf{IPL}$|⁠. Also, we will see that the modal logics |$\textbf{S}_4$| and |$\textbf{K}_4$| do not satisfy atomic DCC.