This paper studies the isomorphism problem for Boolean formulas and places it precisely in the polynomial hierarchy. Two of its results are new. The first sharpens the relationship between Boolean and graph isomorphism. Chang's reduction shows only that the unrestricted Boolean isomorphism problem is GI-hard, in one direction; restricting both inputs to canonical form, where equivalence is free, sharpens this to a both-directions many-one equivalence. Encoding each input as a weight-two-minterm canonical DNF rigid enough that every renaming witnessing isomorphism is forced to be a graph isomorphism, we obtain Canonical Formula Isomorphism CFI $\equiv_m$ GI, together with CFNI $\equiv_m$ GNI for the separation problem. This is completeness in both directions, not the one-directional hardness Chang established. The second result is a classification instrument: writing formula isomorphism as FI $= \exists\lambda \cdot$ EQ exhibits the renaming as a single existential quantifier over a polynomial-size witness applied to the equivalence problem of the inputs, so the renaming is the only complexity the isomorphism question adds beyond equivalence, and the equivalence cost caps the level and fixes its semantic component, while the renaming search supplies the residual structural complexity, which on canonical inputs is exactly the graph-isomorphism core above. Applying the instrument to compact representations, where equivalence is coNP-complete, places the mixed case DT-FI (an arbitrary formula matched against a DNF target) and the fully compact case CNF-FI at the second level: both lie in $\Sigma_2^P$, are coNP-hard and GI-hard, and are complete for no level unless the polynomial hierarchy collapses. The structural facts that frame this level (Schöning's lowness $\Sigma_k^P$[GI] $= \Sigma_k^P$ for $k \geq 2$, under which a graph-isomorphism oracle adds nothing at the second level and above; a first-level boundary at which the graph-isomorphism level lies in NP $\cap$ coNP exactly when GI is low for NP; and a conditional non-completeness from GI $\in$ coAM) are not new, and the paper's role for them is to combine them into a four-case analysis of when the graph-isomorphism core can affect the hierarchy: only when it is complete for its level, and then only at the second. In every case the residue that remains once the equivalence test is made free is graph isomorphism itself.