The deep structure of logical formulas 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? 
 A: Game semantics might be something like what you're looking for. If you have a formula and take all valid game traces for it, and then remove plays that correspond only to the visible connectives of the formula, keeping those that correspond to the atoms, then conceivably the set of partial traces you get could be considered to encode some kind of "deep structure" of the formula.
Ideas like these have been used to reason about "observational equivalence" of formulas, which sound like it's at least related to what you're talking about.
A: There are certainly normal forms of propositional formulae, e.g. CNF, but I don't think that any particular normal form can claim to be the "unique underlying deep structure of the formulae to which it is equivalent." After all, how simple a formula appears depends sensitively on what we plan to do with it.
A: You seem to be talking about a way to choose a particular surface structure to be the canonical representation of the formula.
But... Is it really necessary that the deep structure "look and feel" like a surface structure? If not, every formula in (classical) propositional logic can be reduced to an unambiguous deep structure in the form of a truth table.
p  ¬(¬p)
-  -----
F  F
T  T

p  q  (p∧q)∨(p∧¬q)
-  -  ------------
F  F  F
F  T  F
T  F  T
T  T  T

p  q  p⊃q  ¬p∨q
-  -  ---  -----
F  F  T    T
F  T  T    T
T  F  F    F
T  T  T    T

You can simplify the notation further if you like. For $n$ variables, construct an array of $n^2$ bits or a string of $n$ characters from the set $\{ ``F",`` T" \} -$ e.g., $(\lnot p \vee q)$ could be written as either 1 1 0 1 or 'TTFT'.
Of course, the meaning depends on the order of the rows and columns in the table, so to make it unambiguous, we need a convention: the columns for the input variables should be in alphabetical order from left to right, and the rows arranged so they count in binary from $0$ to $n^2-1$.
For example, in the notation of the J programming language, 2b00 2b01 2b10 2b11 is the base 2 notation for 0 1 2 3, and if you substitute F for 0 and T for 1, you can see that's how I've arranged the values of $p$ and $q$ in the tables above.
A: "Is there eventually a simple rule to single out a distinguished representative among all equivalent formulas that represents the type of a formula ϕ?  Might this rule be as simple as "the formula with minimal numbers of variables, connectives and occurrences thereof"? "
No.  The law of commutation is a logical truth.  That is, [(p→(q→r)→(q→(p→r)] is a tautology.  The upshot here makes such a distinguished representative impossible to find in general, since along with modus ponens it ends up implying that (among endless possible examples) [p→(q→r)] is equivalent to [q→(p→r)].  But, both formulas have the same number of variables, connectives, and occurrences thereof.  And 5 is the smallest possible number of symbols involved here (in Polish notation) for any formula which has three variables... that is you simply can't use fewer symbols than 5 to represent a formula equivalent to [p→(q→r)], but such a formula, in terms of what it represents semantically, is not unique.  (and, of course, both formulas are of the implication type)
Also, even though both $\land$ and $\lor$ associate, they have fixed arity via the formation rules.  Consequently, there is no such distinguished representative which is unique for cases which only involve only conjunctions or only disjunctions.  So, even if you require that the first variable to always get labeled by the same symbol rendering the reasoning of the paragraph above irrelevant, you'll still have [p$\land$(q$\land$r)] as not qualifying as a unique, distinguished representative.
A: If you think to a "canonical representation of a formula", following @Doug Spoonwood refernce to polish notation and @Peter Smith reference to Wittgenstein, we can use the Sheffer stroke.
We have two possibilities :
(i) stay with the standard polish notation : $D\phi\psi$;
in this case, we have minimized the numebr of connectives, and we have a formula like : $DpDpDDqqDpp$.
(ii) Otherwise (see Wiki) :

since the only connective of this logic is $|$, the symbol $|$ could be discarded altogether, leaving only the parentheses to group the letters. A pair of parentheses must always enclose a pair of wffs. Examples of theorems in this simplified notation are $(p(p((qq)(pp))))$.

Are those representation unique ? I think so.
Are them "readable" ? I think not.
