Occurrence in Polish Notation has Unique Scope

From ProofWiki
Jump to navigation Jump to search


Let $\FF$ be a formal language in Polish notation.

Let $\mathbf A$ be a well-formed formula of $\FF$.

Let $a$ be an occurrence in $\mathbf A$.

Then $a$ has a unique scope.


From the formal definition of Polish notation, it follows that $a$ must be introduced by the rule of formation:

$a \mathbf A_1 \cdots \mathbf A_n$

for some well-formed formulas $\mathbf A_1, \ldots, \mathbf A_n$.

By Unique Readability for Polish Notation, the $\mathbf A_i$ are uniquely determined.

Then $\mathbf A' = a \mathbf A_1 \cdots \mathbf A_n$ is a well-formed part of $\mathbf A$.

Moreover, any well-formed part of $\mathbf A$ containing $a$ must contain $\mathbf A'$.

Hence $\mathbf A'$ is the scope of $a$.