Formula trees

Ever had to translate a long and complicated propositional logic formula from Polish notation into standard bracket notation or the other way around? Yeah, didn't think so. Well, I'm going to offer you some advice anyway. For whatever reason it just occurred to me that the task becomes much easier if instead of trying to translate directly you first translate your formula from whichever notation you have it in into Smullyan's tree notation, and then from that into the desired final notation. So if you have a formula in Polish notation, you do the following: Put the leftmost operator at the top of the tree (that's your highest-level node); put the second-leftmost operator (if it's there) at the level-two node starting the leftmost branch of your tree; continue that branch until you hit an atomic sentence(s); put the next operator at the level-two node starting the second-to-the-left branch of the tree; continue going down then right like than until you're done.

For example, say you have ENKpqANpNq. Your leftmost operator is E (equivalence); so that's what you'll be putting at the very top of the tree:

1.

<->

Then you've got negation at a level-two node on the left:

2.

<->

~

Then conjunction one node below:

3.

<->

~

&

And then the left node hits bottom with atoms p:

4.

<->

~

&

p

...and q:

5.

<->

~

&

pq

So you move to the right and continue:

6.

<->

~ |

&

pq

7.

<->

~ |

& ~

pq

8.

<->

~ |

& ~

pq p

9.

<->

~ |

& ~~

pq p

10.

<->

~ |

& ~~

pq pq

And that's the tree, which gives ~(p & q) <-> (~p) | (~q) (one of De Morgan's laws), which is the desired translation. The reverse procedure is equally easy.