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.

Corrections to statements of cited results and to proof presentation; no theorem, proof, or conclusion is changed.

(1) Section 6.2: the definition of MIN-DNF is corrected to Umans' formulation (input a DNF formula; measure the number of literal occurrences). The previous version stated a different variant (arbitrary formula, number of terms).

(2) Theorem 4: the statement is reworded to what the proof establishes: condition (i) of Definition 7 is implied by (iii), and the quantification over $G$ collapses. The previous wording ("conditions (i), (iii) are redundant") was too strong if read literally.

(3) Remark after Definition 6: the complexity of equivalence under renaming on truth-table inputs is stated as polynomial time (Luks 1999), previously overstated as NC; the closing clause now reads "unless GI $\in$ P".

(4) Theorem 2, colour gadget: the clique-size condition is simplified to $a, b \geq 3$ with $a \neq b$; the previous bound in terms of vertex degrees was not used by the argument. A guard for the three excluded instances (those with $n + |ON| \leq 1$, all constant functions) is added, and the caption of Figure 2 is aligned.

(5) Figure 3: the canonical-inputs row is relabelled CFI ($=$ DSFI) to match the text, and a fourth row for CNF-FI is added.

(6) Minor: Section 1.4 wording on the provenance of the membership reduction; "deterministic" removed from an $NP^{GI}$ phrase in Proposition 5; explicit edgeless-graph clauses in Theorem 6 and Proposition 3; bibliography corrections for [AGTH96] (full page range) and [GHM08] (journal title); title-page spacing.

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.