Hola.
Aún no he leído el último mensaje completo, pero como me ha surgido una duda nada más empezar y no tengo justo ahora mucho tiempo, lo pauso de momento aquí y en cuanto pueda continuo leyendo

El significado de estas fórmulas es claro. Fijada una valoración \( v \), tenemos:
- \( \vDash \color{blue}\neg\color{red}\alpha[v] \) si y sólo si \( 1\dot{-} N(t_\alpha)[v] =0 \), si y sólo si \( N(t_\alpha)[v]\neq 0 \), si y sólo si no se cumple \( \vDash \alpha[v] \).
- \( \vDash(\alpha\lor \beta)[v] \) si y sólo si \( N(t_\alpha)[v]\cdot N(t_\beta)[v] =0 \), si y sólo si \( N(t_\alpha)[v] =0 \) o \( N(t_\beta)[v] =0 \), si y sólo si \( \vDash \alpha[v] \) o \( \vDash \beta[v] \).
- \( \vDash(\alpha\land \beta)[v] \) si y sólo si \( N(t_\alpha)[v]+ N(t_\beta)[v] =0 \), si y sólo si \( N(t_\alpha)[v] =0 \) y \( N(t_\beta)[v] =0 \), si y sólo si \( \vDash \alpha[v] \) y \( \vDash \beta[v] \).
- \( \vDash(\alpha\rightarrow \beta)[v] \) si y sólo si \( (1\dot{-} N(t_\alpha)[v])\cdot N(t_\beta)[v]=0 \), lo cual equivale a que \( 1\dot{-} N(t_\alpha)[v]=0 \) o \( N(t_\beta)[v]=0 \), que a su vez equivale a que \( N(t_\alpha)\neq 0 \) o \( N(t_\beta)[v]=0 \), que a su vez equivale a que, o bien no \( \vDash \alpha[v] \), o bien \( \vDash \beta[v] \).
- Claramente \( \vDash (\alpha\leftrightarrow \beta)[v] \) si y sólo \( \alpha \) y \( \beta \) son equivalentes, en el sentido de que se cumple \( \vDash \alpha[v] \) si y sólo si se cumple \( \vDash \beta[v] \).
A parte de la pequeña errata marcada en azul tengo una duda sobre esto. En todos veo claro las equivalencias hasta la última de ellas, que es donde tengo la duda. Se que esto es consecuencia de las dos reglas de inferencia dichas anteriormente y del teorema de corrección, pero el teorema de corrección nos dice que si la premisa es verdadera, entonces la conclusión también lo es. Ahora bien, aquí estamos trabajando con valoraciones particulares, sin partir en ningún momento de que cierta fórmula sea o no verdadera, por tanto, el teorema de corrección no aplica tal cual, ¿no?
Porque, cuando se probó que las reglas de inferencia si parten de fórmulas verdaderas dan conclusiones verdaderas, se utilizó explícitamente que las premisas eran ciertas para cualquier valoración (pues se utilizaba que se satisfacian en valoraciones ligeramente distintas a la fijada), por tanto no parece que se pueda concluir que si tienes cierta regla de inferencia de ARP y la premisa es satisfecha por una valoración fija (sin saber si la fórmula es verdadera), entonces la conclusión también lo sea. De hecho, no es así pues, por ejemplo, para la regla \( S_1 \) si se considera la fórmula \( x+y=2 \) y la valoración \( v \) tal que \( v(x)=1, v(y)=1, v(z)=3 \), entonces es claro que dicha fórmula es satisfecha por \( v \), pero no lo es la fórmula \( z+y=2 \) que se concluye por \( S_1 \).
En resumen, mi pregunta es, ¿no debería enunciarse lo que he citado en términos de fórmulas verdaderas y no de valoraciones concretas?
Por ejemplo, el 1. no debería ser más bien:
\( \vDash \neg\alpha \) si y sólo si \( \vDash 1\dot{-} t_\alpha =0 \), si y solo si, para cualquier valoración \( v \) es \( 1\dot{-} N(t_\alpha)[v] =0 \), si y sólo si, para cualquier valoración \( v \) es \( N(t_\alpha)[v]\neq 0 \), si y sólo si \( t_\alpha=0 \) es falsa, si y sólo si \( \alpha \) es falsa.EDITO: Aunque, pensándolo ahora, tampoco estoy seguro que se pueda asegurar que \( t_\alpha=0 \) es falsa si, y solo si, \( \alpha \) es falsa, pues lo que sabemos es que \( t_\alpha=0 \) es verdadera si, y solo si, \( \alpha \) es verdadera, pero ser falso no es la negación de ser verdadero. Por tanto, ¿no habría que ver de alguna forma que para una valoración cualquiera \( v \) se tiene que \( \vDash \alpha[v] \) si, y solo si, \( \vDash (t_\alpha = 0)[v] \)? Porque, como decía antes, esto no se deduce de las reglas de inferencia dadas al principio de este último mensaje y el teorema de corrección.
Un saludo.