Another end-of-chapter exercise in IFL2 very briefly introduces Polish notation for propositional logic, and invites you to construe a few Polish wffs, and (going in the other direction) to render some standard wffs into prefix Polish. So far, so easy!
Then — at the moment! — I cheerfully add, “Show that Polish notation, although bracket-free, introduces no structural ambiguities (i.e. every Polish wff can be parsed in only one way).”
But now I find, when I come to write up the answers to the exercises, that my first draft attempt at explaining uniqueness isn’t super user-friendly. Before I try to massage it something better, any pointers to a particularly nice explanation already out there which is likely to be immediately grasped by just-beginning philosophy students of why the prefix notation is unambiguous? (I don’t mean so much a full-blown proof as enough arm-waving to get across the idea of a proof.)
A key idea could be that, when parsing a prefix wff top-down — which corresponds to recursive decomposition — there are no choices to be made any any point. The first symbol in the wff always tells you what to do, and if it’s a connective it has a definite, fixed number of arguments in a fixed order. That’s why it’s easy to write a parser or evaluator for expressions in that sort of notation.
If there are no choices, there’s no way for two different parses to be possible.
I can’t answer your actual question, but I have found that students find it easier to follow (in these kinds of example) proof by infinite descent in the form of *there’s a smallest counterexample*.
This is, of course, an instance of the principle of proof (of the existence of a unique function satisfying certain conditions) by structural recursive definition under the unique decomposability (unique readability) condition. It is very difficult, if not impossible, to get a proof of the general principle across to students unless they have already had some practice in working set theory, although it may be possible to give a rough but convincing account of a particular instance such as the one about Polish notation. There is an intuitive explanation (but not a proof) of what is going on in the general principle, designed for students with a a few weeks of set theory behind them, in section 4.6.3 of “Sets Logic and Maths for Computing” 2nd edition 2012, with application to Polish notation in section 7.4.