Abstract

In classical propositional calculus for each proposition A(p) the following holds: $\vdash A(p) \leftrightarrow A^3(p)$ . In this paper we consider what remains of this in the intuitionistic case. It turns out that for each proposition A(p) the following holds: there is an n ∈ N such that $\vdash A^n(p) \leftrightarrow A^{n + 2}(p)$ . As a byproduct of the proof we give some theorems which may be useful elsewhere in propositional calculus