Propositional Calculus: Stating and proving the unique readability theorem in Polish notation

Question

The Language $\mathcal{L_0}$: Let $\mathcal{L_0}$ be the smallest set $L$ of finite sequences of $\textit{logical symbols}= \{(\enspace)\enspace\neg\}$ and $\textit{propositional symbols}=\{A_n|n\in\mathbb{N}\}$ for $n \in \mathbb{N}$ satisfying the following properties:

(1) For each propositional symbol $A_n$ with $n\in\mathbb{N}$, \begin{multline} A_n \in L. \end{multline}

(2) For each pair of finite sequences $s$ and $t$, if $s$ and $t$ belong to $L$, then \begin{multline} (\neg s) \in L \end{multline} and \begin{multline} (s \to t) \in L. \end{multline}

Readability for $\mathcal{L_0}$: Suppose that $\phi$ is a formula in $\mathcal{L_0}$. Then exactly one of the following conditions applies.
(1) There is an $n$ such that $\phi = A_n.$
(2) There is a $\psi \in \mathcal{L_0}$ such that $\phi = (\neg\psi)$.
(3) There are $\psi_1$ and $\psi_2$ in $\mathcal{L_0}$ such that $\phi = (\psi_1 \to \psi_2)$

Unique Readability for $\mathcal{L_0}$: Same conditions as Readability, but in (2) and (3), the formulas $\psi$, $\psi_1$, and $\psi_2$ are unique, respectively.

Problem (Polish Notation): Let $\mathcal{P_0}$ be the smallest set of sequences $P$ such that the following conditions hold.
a) For each $n$, $A_n \in P$.
b) If $\psi_1$ and $\psi_2$ belong to $P$, then so do $\neg\psi_1$ and $\to\psi_1\psi_2 = \langle \to \rangle + \psi_1 + \psi_2$.

State and prove the unique readability theorem for $\mathcal{P_0}$

Answer 1

Suppose $\phi$ is a formula in $\mathcal{P_0}$. Then $\phi$ is one and only one of these forms:
(1) There is an $n$ such that $\phi =A_n$.
(2) There is a $\psi$ in $\mathcal{P_0}$ such that $\phi = \neg\psi$.
(3) There are $\psi_1$ and $\psi_2$ in $\mathcal{P_0}$ such that $\phi = \to\psi_1\psi_2$.
Further, the $\psi_i$ in (2) and (3) are uniquely determined.

It is absolutely clear these are mutually exclusive in polish notation. All that remains is to show that in (2) and (3), these $\psi_i$ are unique:

For (2), suppose $\neg\psi_a$ = $\neg\psi_b \implies \psi_a=\psi_b \implies$ uniqueness.
For (3), suppose $\to\psi_1\psi_2=\to\psi_3\psi_4 \implies \psi_1\psi_2=\psi_3\psi_4 \implies$ one of $\psi_1,\psi_3$ is an initial segment of one another, which we know is not possible:

Let $w$ be the weight of the symbols:
$w(A_n) = 1, w(\neg)=0, w(\to) = -1$.

Then for any polish-formula $\psi = s_1\dots s_n$ of length $n$, The sum of the weights of its symbols, $\sum_{i=1}^{n}w(s_i) =1$ by induction.

Any terminal segment of a polish-formula is a concatenation of polish-formulas. So suppose $\psi'$ is a proper initial segment polish-formula of the polish-formula $\psi$, and $\psi''$ is the terminal segment of $\psi$ that makes $\psi=\psi'\psi''$.

If $\psi=\psi'\psi''$ then $w(\psi) = w(\psi')+w(\psi'')$. But $\psi''$ is a terminating segment of a polish-formula so its weight is greater than or equal to $1$. Contradiction.