Los autores de forall x dan esta definición de validez (página 8):
Un argumento es válido si y sólo si es imposible que todas las premisas sean verdaderas y la conclusión falsa.
También se refieren a esto como «validez en virtud de la forma» (página 21):
La validez de los argumentos que acabamos de considerar no tiene mucho que ver con los significados de expresiones inglesas como «Jenny is miserable», «Dipan es un ávido lector de Tolstoi» o «Jim actuó en muchas obras de teatro». Si tiene que ver con los significados, es con los significados de frases como ‘y’, ‘o’, ‘no’, y ‘si…, entonces…’.
Esta validez puede ser validada automáticamente usando comprobadores de pruebas. Suponiendo que el comprobador de pruebas no esté mal construido si el argumento que introducimos en el comprobador de pruebas pasa, entonces es válido en virtud de la forma.
Considere la frase, «Está lloviendo». La negación de esta frase podría escribirse como «No es el caso que esté lloviendo». Simbolicemos «Está lloviendo» con «P». Entonces su negación sería «¬P». Una oración autocontradictoria construida a partir de estas dos sería «P ∧ ¬P», es decir, tanto «P» como «¬P».
Usando esto como premisa ¿podemos construir un argumento válido en virtud de la forma? Sí, se puede. He aquí un ejemplo en el que intento demostrar que «P ∧ ¬P» implica «P».
La primera línea es la premisa. La segunda línea la obtengo utilizando la regla de eliminación de la conjunción (∧E) que me permite utilizar cualquiera de los dos lados de la conjunción (∧) en mi argumento. Resulta que lo que utilicé, «P», era lo que quería demostrar y así el comprobador de pruebas verificó que había alcanzado mi objetivo.
Puede parecer extraño que dada una premisa autocontradictoria, haya sido capaz de construir un argumento válido mostrando que uno de los conjuntos de la premisa autocontradictoria se sigue. Puede ser aún más extraño.
Con un poco más de trabajo, puedo mostrar que cualquier cosa se sigue de una premisa autocontradictoria. Sea «Q» la simbolización de cualquier cosa. Este ejemplo muestra que puedo construir un argumento válido en virtud de la forma para «Q»:
La primera línea contenía la premisa autocontradictoria como en el ejemplo anterior.
En las líneas 2 y 3 utilicé la eliminación de la conjunción (∧E) a ambos lados de la premisa (línea 1) para colocarlas en líneas separadas.
Una vez que las tengo en líneas separadas, puedo usar la regla de introducción de la contradicción (⊥I) para anotar en la línea 4 que tengo una contradicción (⊥).
En la línea 5, como tengo una contradicción, puedo escribir lo que quiera. Eso se llama la regla de la explosión (X). Como mi objetivo es «Q» y según las reglas puedo escribir lo que quiera, escribo «Q». El comprobador de pruebas verifica que he alcanzado mi meta.
Para más detalles sobre estas reglas, véase el capítulo 15 «Reglas básicas para TFL» en forall x.