"Dado un conjunto de conocidos declaraciones se podría definir la dificultad de un teorema como la longitud mínima de entre todas sus pruebas deducidas a partir de la conocida declaraciones. También se podría definir la importancia de un teorema de T en un conjunto de declaraciones como la inversa de la suma de la dificultad de todo el resto de los teoremas conocidos T."
Incluso axiomática del cálculo proposicional es conocido que el conjunto de todos los restantes teorema es infinito. Dado que la dificultad de todos los teoremas es positivo para cada teorema, esto implica que cada teorema decir 2 valores o cualquier otro axiomática propuesta de cálculo tiene una importancia infinita.
Usted puede ser que desee pensar que todos los restantes teoremas no son conocidos. Y, en cierto sentido, que viene como correcta. Sin embargo, existen infinitos patrones de teoremas que son conocibles en algún sentido. Por ejemplo, bajo condensada desapego como una regla de inferencia, si CpCqp es un axioma o teorema ("tesis" de aquí en adelante), entonces tenemos este infinito patrón de tesis:
{CpCqp, Cp$_1$CpCqp, Cp$_2$Cp$_1$CpCqp ... }
Y usted puede prefijo de una secuencia infinita de tesis en una manera similar.
Otro patrón es la secuencia de las tesis que se pueden derivar mediante condensada desprendimiento de donde CCpqCCqrCpr siempre es la premisa más importante en cualquier sistema donde "C" es el principal conectivo para cada axioma. Desde "Cpq" unifica con todo axioma, y mediante el uso de condensados desprendimiento de generar un condicional de la forma de CC$\alpha$$\beta$C$\gamma$$\beta$, Cpq unifica con cada tesis en esta secuencia. Utilizando la notación D va
(1, D1.1 = 2, D1.2 = 3, D1.3 = 4...) Otro conocible patrón de la tesis se inicia con CCpqCCrpCrq y se comporta de manera similar al modelo anterior.
Robert Veroff hizo algunos trabajos en la búsqueda de más corta pruebas proposicional de los cálculos de forma sistemática (Larry Wos ha pasado años buscando corto pruebas del teorema de provers, pero existen muy pocas pruebas que tienen parecen haber entendido que resultó ser la más corta). Es posible que desee ver su trabajo, que se puede obtener de lectura en formato Postscript como su página web:
Encontrar más corta Pruebas: Una Aplicación de los enlaces a las Reglas de Inferencia
