Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms

We show some applications of the formulas-as-polynomials correspondence: 1) a method for (dis)proving formula isomorphism and equivalence based on showing (in)equality; 2) a constructive analogue of the arithmetical hierarchy, based on the exp-log normal form. The results are valid intuitionistically, as well as classically.