A long-standing question to which I never found a concise answer is:
Is there something like an unambiguous deep structure of a formula of propositional logic, opposed to its comparingly arbitrary surface structure?
Here, I consider propositional logic with the connectives $\neg,\vee,\wedge,\rightarrow$.
At the surface level it is clear what a negation or a disjunction is: a negation is of the form $\neg (\phi)$, a disjunction is of the form $(\phi)\vee(\varphi)$, and so on.
But there are equivalent formulas that are not of the same type (the "deep structure" being a tree of types):
$\neg(\neg p) \equiv p $
$(p \wedge q )\vee(p \wedge \neg q) \equiv p$
$p \rightarrow q \equiv \neg p \vee q$
So you cannot define "is a formula of type X" bluntly by "has an equivalent formula of the form Y".
Is there eventually a simple rule to single out a distinguished representative among all equivalent formulas that represents the type of a formula $\phi$? Might this rule be as simple as "the formula with minimal numbers of variables, connectives and occurrences thereof"?
Or can there be several formulas with the same minimal numbers, but of different type?