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.)

David MakinsonThis 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.

David AuerbachI 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*.

Rowsety MoidA 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.