Cálculo proposicional: Un algoritmo para determinar si una secuencia finita pertenece a $\mathcal{L_0}$

Question

Dejemos que $\mathcal{L_0}$ sea el conjunto más pequeño $L$ de secuencias finitas de $\textit{logical symbols}= \{(\enspace)\enspace\neg\}$ et $\textit{propositional symbols}=\{A_n|n\in\mathbb{N}\}$ para $n \in \mathbb{N}$ que satisface las siguientes propiedades:

(1) Para cada símbolo proposicional $A_n$ con $n\in\mathbb{N}$ , $$\begin{multline} A_n \in L. \end{multline}$$

(2) Para cada par de secuencias finitas $s$ et $t$ , si $s$ et $t$ pertenecen a $L$ entonces $$\begin{multline} (\neg s) \in L \end{multline}$$ y $$\begin{multline} (s \to t) \in L. \end{multline}$$

El problema: Dar un algoritmo (pseudocódigo) para determinar si una secuencia finita dada pertenece a $\mathcal{L_0}$ .

Estaba pensando en algo relacionado con los paréntesis de apertura frente a los de cierre primero, si no coinciden en el recuento. O tal vez podría comprobar si la secuencia comienza con una negación o una implicación, lo que los descartaría automáticamente. Esto sería una especie de filtro antes de la carne del algoritmo.

Answer 1

Si consultas el libro Introduction to Metamathematics de S. C. Kleene, puedes encontrar un algoritmo para un lenguaje infijo distinto que podría darte algunas ideas aquí.

En notación polaca existen varios algoritmos conocidos. Uno de ellos es el siguiente...

1. Asigna -1 a cada símbolo proposicional.
2. Asignar 0 a $\lnot$ o "N".
3. Asignar 1 a $\rightarrow$ o "C". (Estoy usando C y N para el ejemplo)

Luego sumamos esos números de izquierda a derecha. Por ejemplo

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

Una cadena terminará como una fórmula en notación polaca si los números asignados a los símbolos comienzan y terminan con -1, o si esos números comienzan con 0 o 1, tiene -1 corresponde al último símbolo, y sólo tiene -1 correspondiente al último símbolo.