¿Argumento deductivo en el que todos los pasos y premisas se establecen explícitamente?

No estoy seguro de hasta qué punto los conceptos con los que estoy familiarizado pueden coincidir con lo que busca, pero estoy algo familiarizado con el desarrollo de la Teoría de la prueba , y su búsqueda de términos parece alinearse con algunas ideas que he explorado en ese campo.

En la teoría de la prueba, particularmente en las discusiones sobre la deducción natural , a veces hablamos de una prueba o argumento que está en forma normal. Un argumento de forma normal es uno que ha sido escrito en "la forma más básica", lo que significa que hemos analizado formalmente todas y solo las premisas necesarias del argumento, las hemos dividido en partes sintácticas componentes (a través de "reglas de eliminación"). "), luego los volvió a ensamblar para estructurar las conclusiones deseadas (a través de "reglas de introducción").

No todos los argumentos formales, o incluso todas las pruebas de deducción natural formal válidamente construidas, están en forma normal. Sin embargo, muchos sistemas formales pretenden mostrar algo así como un Teorema de Normalización, en el sentido de que cuando se invoque cualquier uso no mínimo de nuestras reglas lógicas, podríamos, sin pérdida de generalidad, reescribir el argumento para eliminarlo. Uno de los principales defensores de este tipo de trabajo fue Dag Prawitz, cuya tesis sobre el análisis de la teoría de la prueba de la deducción natural ayudó a informar mucho de la escritura filosófica sobre la prueba, la inferencia y el cálculo que seguiría.

Un concepto valioso que Prawitz introduce en su trabajo es la noción de un "esqueleto de argumento". (ver su Sobre la idea de una teoría de prueba general para una descripción más accesible). Esta es una generalización de las estructuras de árbol involucradas en los argumentos o pruebas de deducción natural formal, en la que admitimos no solo que estamos trabajando desde axiomas lógicos como premisas a conclusiones (lo que llamamos un argumento cerrado), sino también que podemos permitir argumentos no probados. antecedentes que conducen a consecuentes a través del mismo tipo de reglas lógicas de inferencia: estas estructuras de "argumento abierto" también son esqueletos de argumento.

(La deducción natural a menudo trata de prescindir por completo de los axiomas en sus estructuras, más bien difiere todo lo que es "puramente lógico" a la aplicación de reglas de inferencia estructural).

Entonces, quizás algunos giros útiles de la frase podrían ser estos: sus argumentos formales "más débiles" son argumentos abiertos, y sus "pruebas" son esqueletos de argumentos, ya que insinúan una estructura de prueba que podría desarrollarse aún más. Sus argumentos "más fuertes" son Argumentos Cerrados, en el sentido de que sus esqueletos no dejan colgando suposiciones extralógicas, y la versión más mínima sintácticamente de dicho argumento (idealmente adecuada para el procesamiento de máquinas) sería su Forma Normal.

Hay interpretaciones alternativas de este tipo de trabajo en otras formas de teoría de la prueba. Donde Prawitz hace uso de Argument Skeletons para respaldar su sistema de Deducción Natural, la tecnología Sequent Calculus más común desarrollada a partir del sistema de Hilbert por Gerhard Gentzen nos permite capturar reglas de transformación para inferencias, colapsando la distinción entre argumentos abiertos y cerrados. Sin embargo, comprender esa distinción puede ayudar a obtener una idea de lo que el cálculo secuencial está haciendo de manera diferente, y cómo podemos aplicar los principios de transformaciones de argumentos que conservan la consistencia y la solidez para usar en la manipulación mecánica de cadenas de prueba.

Ver este post sobre el espectro de formalidad de un argumento matemático . Lo que describió como "cada paso y las premisas se establecen explícitamente" se clasificaría como "absolutamente formal" (y "prueba formal" sin ninguna calificación a menudo significa esto). La mayoría de los argumentos matemáticos no se expresan como pruebas absolutamente formales, sino que se clasifican como "razonablemente formales". Usted solicitó un término para las pruebas en un sistema deductivo que no establezca explícitamente las reglas utilizadas, pero no existe tal término porque los sistemas formales generalmente están diseñados para que se pueda verificar mecánicamente si se siguen las reglas o no, y por lo tanto no hay No es necesario especificar qué regla se usa en cada paso, excepto para mejorar la eficiencia del proceso de verificación.

Sin embargo, parece tener una idea errónea sobre la naturaleza de la prueba de una tautología proposicional a través de tablas de verdad. Si bien es razonable considerarlo informal en el sentido de que dibuja una tabla y dice "mire, estos son todos los casos y la declaración es verdadera en todos los casos", en realidad se puede expresar no menos formalmente que un estilo Hilbert o Fitch . -estilo o estilo secuenteprueba. Todo lo que necesita hacer es escribir la tabla una fila a la vez en un orden sistemático (por ejemplo, orden lexicográfico; para 3 variables A,B,C tendría las filas 000,001,010,011,100,101,110,111 que denotan los valores de verdad de A,B,C ), y el valor de verdad del enunciado para cada fila (que se puede calcular mecánicamente). Esto a veces se denomina prueba semántica, porque procede verificando el valor de verdad del enunciado (de acuerdo con la semántica de la lógica proposicional) en cada situación (asignación de verdad de variables). Por el contrario, una prueba en algún sistema deductivo es una prueba sintáctica, porque es 'solo' una cuestión de empujar símbolos sin tener en cuenta el 'significado'. Sin embargo, las pruebas semánticas pueden ser claramente tan formales como las pruebas sintácticas, ya que aún necesita algún proceso mecánico para verificar una prueba sintáctica,

Pero como siempre, vale la pena enfatizar que aunque podemos tener pruebas semánticas para la lógica proposicional, es imposible tener pruebas semánticas para la lógica de primer orden completa (porque los teoremas de incompletitud aplicados a PA− muestran que no puede haber un programa que pueda decidir en un número finito de pasos si una oración de entrada de la forma "X ⇒ Y" en el lenguaje de PA es una tautología o no, donde "X" es la conjunción de los axiomas de PA−). Entonces, las pruebas sintácticas siguen siendo el único método de prueba completamente adecuado para la lógica de primer orden.