Fixed-Point Elimination in the Intuitionistic Propositional Calculus (Extended Version)

Introduction

\begin{matrix} μx.φ(x) = φ^n(⊥), \\ νx.φ(x) = φ^n(⊤). \end{matrix}