Propositional Calculus: An algorithm to determine whether a finite sequence belongs to $\mathcal{L_0}$

Question

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}

Problem: Give an algorithm (pseudocode) to determine whether a given finite sequence belongs to $\mathcal{L_0}$.

I was thinking something involving opening vs. closing parenthesis first, if they don't match in count. Or perhaps you could check if the sequence begins with a negation or an implication - that would automatically rule them out. This would be sort of a filter prior to the meat of the algorithm.

Answer 1

If you consult the book Introduction to Metamathematics by S. C. Kleene, you can find an algorithm for a distinct infix language which might give you some ideas here.

In Polish notation there exist several known algorithms. One of them is the following...

1. Assign -1 to each propositional symbol.
2. Assign 0 to $\lnot$ or "N".
3. Assign 1 to $\rightarrow$ or "C". (I'm using C and N for the example)

Then we sum those numbers left to right. For example

C  N  a1 C C C a2 C a3 a4 a5 a1
|  |  |  | | | |  |  |  | |  |
1  1  0  1 2 3 2  3  2  1 0  -1

C  C N  a1 C C a2 a3
|  | |  |  | | |  |
1  2 2  1  2 3 2  1

A string will end up as a formula in Polish notation if the numbers assigned to the symbols start and end with -1, or if those numbers start with 0 or 1, has -1 correspond to the last symbol, and only has -1 corresponding to the last symbol.