Sea x una fórmula, ¿probar si x es válido que ~ x no debe ser satisfactoria?

No estoy seguro de qué tipo de teoría de modelos está utilizando en su ejemplo anterior, pero la prueba es algo como esto:

De derecha a izquierda:
1. Suponga que A es válido en M
2. Si A es válido en M, entonces para todos los modelos m de M, A es satisfactoria en m [definición de validez]
3. Si A es satisfactoria en todos los modelos m de M, entonces ~ A es insatisfactorio en todos los modelos m de M [de 2 y bivalencia]
4. Por lo tanto, ~ A es insatisfactorio en M [de 1, 2, 3 por MP]

De izquierda a derecha:
5. Suponga que ~ A es insatisfactorio en M
6. Si ~ A es insatisfactorio en M, para todos los modelos m de M, ~ A es insatisfactorio en M [definición de satisfacción]
7. Si ~ A es insatisfactorio en M, entonces para todos los m de M, A es satisfactoria en M [de 6 y bivalencia]
8. Si A es satisfactoria para todos los m de M, entonces A es válido [de 5,6,7 por MP y la definición de validez]

La pregunta depende de reconocer que la validez es solo satisfacción en todos los modelos de L.