SAT y pruebas en lógica proposicional

Question

Una vista ingenua preguntaría por qué debería molestarse con pruebas en lógica proposicional, ya que se pueden usar simplemente tablas de verdad. Uno se vuelve un poco más sofisticado cuando se da cuenta de que los tamaños de las tablas de verdad crecen exponencialmente con el número de variables. De hecho, aquí tenemos un problema NP-duro. ¿Existe algún ejemplo particular de una fórmula de lógica proposicional cuya validez universal es demostrablemente costosa de establecer, pero que tiene una prueba corta y elegante?

Answer 1

Dado un número indefinidamente grande de variables proposicionales, muchas fórmulas de este tipo pueden formularse en lógica proposicional a través de la meta-teoría. Utilizo notación polaca a continuación.

Como señaló Gerry Myerson, un ejemplo consistiría en:

C KaKb...Kyz KaKb...Kyz calificaría. Pero dado el abreviación clara, esto consiste simplemente en una instancia de la ley débil de la identidad Cxx. En otras palabras, la prueba sería la siguiente:

axioma 1 Cxx
1 x / KaKbKcKdKeKfKgKhKiKjKkKlKmKnKoKpKqKrKsKtKuKvKwKxKyz * 2
2 C KaKbKcKdKeKfKgKhKiKjKkKlKmKnKoKpKqKrKsKtKuKvKwKxKyz
 KaKbKcKdKeKfKgKhKiKjKkKlKmKnKoKpKqKrKsKtKuKvKwKxKyz

Supongamos que CxCyx es una tesis (axioma o teorema) de una lógica proposicional con suficientes variables. Entonces,

3) CaCbCcCdCeCfCgChCiCjCkClCmCnCoCpCqCrCsCtCuCvCxCyx es un teorema en dicho sistema. Meta-lógicamente, la prueba es simple. Notamos que a partir de cualquier teorema podemos poner un signo condicional 'C' y cualquier expresión significativa antes de él. Dado que CxCyx es un teorema, mediante aplicaciones repetidas de esos principios, 3) es un teorema.

Supongamos que CxCyz es lógicamente equivalente a CyCxz y que podemos reemplazar cualquier instancia de CxCyz en cualquier fórmula con CyCxz en cualquier fórmula. La meta-teoría aquí implica que cualquier fórmula que tenga exactamente dos instancias de 'x', siga un patrón similar también será un teorema. Como ejemplo fácil:

4) CaCbCcCdCeCfCgChCiCjCkClCmCnCoCpCqCrCsCtCuCxCvCyx es una fórmula.

Pero también lo es,

5) CxCbCcCfCgChCiCjCkCdCeCoCpCqCsCtCrClCmCaCnCvCuCwx

Como otro ejemplo, consideremos lo siguiente:

6) CCabCCbcCCcdCCdeCCefCCfgCChiCCijCCjkCCklCClmCCmnCCnoCCopCCpqCCqrCCrsCCstCCtuCCuvCCvwCCwxCCxyCCyzCaz

Digamos que podemos usar la resolución para determinar la validez de la fórmula. Esto significa que para verificar lo anterior, solo necesitamos considerar cada antecedente como una cláusula. O en otras palabras, Cab se traduce en la cláusula ANab, Cbc a la cláusula ANbc y así sucesivamente. Luego, lo siguiente demostrará lo anterior:

1 ANab
2 ANbc
3 ANcd
4 ANde
5 ANef
6 ANfg
7 ANgh
8 ANhi
9 ANij
10 ANjk
11 ANkl
12 ANlm
13 ANmn
14 ANno
15 ANop
16 ANpq
17 ANqr
18 ANrs
19 ANst
20 ANtu
21 ANuv
22 ANvw
23 ANwx
24 ANxy
25 ANyz
26 a
27 Nz
28 b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, 
t, u, v, w, x, y, z por resolución de 26 y 1, luego de el paso anterior 
y 2, luego del paso anterior y 3, y así sucesivamente.
29 {} del último paso anterior y 27.

Creo que estarás de acuerdo en que incluso si tuviéramos que expandir cada paso en 28, aún así sería más corto que las tablas de verdad.

También podríamos permutar 6) de muchas maneras y obtener fácilmente teoremas con veintiséis variables. Ni siquiera nos molestamos en subíndicar variables con símbolos numéricos. Tampoco tuvimos que invocar grandes números naturales.

Como quizás otro ejemplo, supongamos que tenemos una definición para expresiones significativas:

Una expresión significativa es una de las siguientes:

1. Una letra minúscula del alfabeto inglés.
2. Una expresión de dos unidades con 'N' como primera unidad y alguna expresión significativa $\alpha$ como segunda unidad.
3. Una expresión de tres unidades con 'A' o 'C' o 'K' como primera unidad, alguna expresión significativa $\alpha$ como segunda unidad, y alguna expresión significativa $\beta$ como tercera unidad.

Nada más es una expresión significativa. Supongamos que tenemos las siguientes reglas de inferencia con $\alpha$ y $\beta$ nuevamente representando cualquier expresión significativa.

1. Desprendimiento condensado con CxCyx como siempre el premisa mayor.
2. Podemos reemplazar cualquier instancia de C en cualquier fórmula con AN en cualquier expresión significativa (ya que C$\alpha$$\beta$ es lógicamente equivalente a AN$\alpha$$\beta$).
3. Podemos reemplazar cualquier instancia de C$\alpha$$\beta$ en cualquier expresión significativa con NK$\alpha$N$\beta$ en cualquier expresión significativa.
4. Podemos reemplazar cualquier instancia de $\alpha$ en cualquier fórmula con CC$\alpha$$\beta$$\alpha$ en cualquier expresión significativa.

Observa que en 4. $\beta$ podría consistir en cualquier expresión significativa.

Supongamos que nuestro único axioma es CxCyx. Entonces lo siguiente da como resultado una prueba de 17 pasos con una cantidad modesta de símbolos:

axioma   1 CxCyx
1, 1.   2 CaCbCcb
2, 1.   3 CaCbCcCdc
3, 1.   4 CaCbCcCdCed
4, 1.   5 CaCbCcCdCeCfe
5, 1.   6 CaCbCcCdCeCfCgf
6, 1.   7 CaCbCcCdCeCfCgChg
7, 1.   8 CaCbCcCdCeCfCgChCih
8, 1.   9 CaCbCcCdCeCfCgChCiCji
9, 2.  10 ANaCbCcCdCeCfCgChCiCji
10, 3. 11 ANaCbCcCdCeCfCgNKhNCiCji
11, 2. 12 ANaCbCcCdCeCfCgNKhNCiANji
13, 4. 13 ANaCCCbybCcCdCeCfCgNKhNCiANji
13, 2. 14 ANaCCCbybCcCdANeCfCgNKhNCiANji
14, 4. 15 ANaCCCbybCcCdANeCfCCCgugNKhNCiANji
15, 4. 16 ANaCCCCCbkbybCcCdANeCfCCCgugNKhNCiANji
16, 4. 17 ANCCaCzCoCpCCrstaCCCCCbkbybCcCdANeCfCCCgugNKhNCiANji

El último paso implica que 'a' se reemplace por 'CCaCzCoCpCCrsta'. Aquí, CzCoCpCCrst es una expresión significativa ya que tiene tres unidades 'C', 'z' y 'CoCpCCrst' que son expresiones significativas, 'CoCpCCrst' es una expresión significativa ya que tiene unidades 'C', 'o', y 'CpCCrst', con 'CpCCrst' teniendo unidades 'C', 'p' y 'CCrst', con 'CCrst' teniendo unidades 'C', 'Crs', y 't', con 'Crs' teniendo unidades 'C', 'r', y 's'.

La regla 4 es válida como regla de reemplazo ya que para todo x, para todo y, para todo z, en el dominio proposicional de dos valores de verdad, CxCCxyx es un teorema (ya que CxCzx es un teorema), y también lo es CCCxyxx.

Creo que también estarás de acuerdo en que la prueba de la expresión significativa 17 aquí es mucho más elegante y corta que probarla mediante tablas de verdad.

Answer 2

Las reglas de formación para lo siguiente serán las siguientes:

1. Todas las letras minúsculas del abecedario califican como expresiones significativas.
2. Si $\alpha$ tiene la forma de una expresión significativa y $\beta$ también tiene la forma de una expresión significativa, entonces C$\alpha$$\beta$ también la tiene.
3. Nada más en lo que sigue califica como una expresión significativa.

Entonces, según la cláusula 1, a, b y c califican como expresiones significativas. Dado que tenemos esas, Cac también constituye una expresión significativa según la cláusula 2, al igual que Cbc. Según la cláusula 2, CbCac es una expresión significativa. Nuevamente según la cláusula 2, CCbCacCbc califica como una expresión significativa. Nuevamente según la cláusula 2, CaCCbCacCbc califica como una expresión significativa.

Ahora, como ejemplo particular, en lugar de solo unos pocos como en mi respuesta anterior, y para disipar cualquier noción de que CpCqp sea la razón por la que pude hacer lo anterior, escogeré

CaCCbCacCbc

como nuestra tesis lógica para estudiar. Las reglas de inferencia son simplemente sustitución uniforme en la tesis lógica primitiva anterior y desprendimiento de C:

"A partir de una tesis de la forma C$\alpha$$\beta$ y una tesis de la forma $\alpha$ podemos aceptar una de la forma $\beta$".

La notación $\alpha$/$\beta$ indica que $\alpha$ se sustituye con $\beta$. La notación C$\alpha$-$\beta$ indica que tenemos una expresión significativa $\alpha$ en el antecedente, y vamos a desprender $\beta.

axioma 
1 CaCCbCacCbc
1 b/d, c/e, a/CaCCbCacCbc * 2
2 CCaCCbCacCbcCCdCCaCCbCacCbceCde
2 * C1-3
3 CCdCCaCCbCacCbceCde
1 b/f, c/g, a/CCdCCaCCbCacCbceCde * 4
4 CCCdCCaCCbCacCbceCdeCCfCCCdCCaCCbCacCbceCdegCfg
4 * C3-5
5 CCfCCCdCCaCCbCacCbceCdegCfg
1 b/h, c/i, a/CCfCCCdCCaCCbCacCbceCdegCfg * 6
6 CCCfCCCdCCaCCbCacCbceCdegCfgCChCCCfCCCdCCaCCbCacCbceCdegCfgiChi
6 * C5-7
7 CChCCCfCCCdCCaCCbCacCbceCdegCfgiChi
1 b/j, c/k, a/CChCCCfCCCdCCaCCbCacCbceCdegCfgiChi * 8
8 CCChCCCfCCCdCCaCCbCacCbceCdegCfgiChiCCjCCChCCCfCCCdCCaCCbCacCbceCdegCfgiChikCjk
8 * C7-9
9 CCjCCChCCCfCCCdCCaCCbCacCbceCdegCfgiChikCjk

Ahora, la tesis 9 tiene once variables, por lo que su tabla de verdad tiene solo 2048 filas. Pero, nos llevó nueve pasos probar la tesis 9. El paso más largo en esta prueba tiene menos de 100 símbolos. Por lo tanto, esta prueba tiene menos de 900 símbolos en total, y así, si llamamos al tamaño de una prueba al número de símbolos que tiene, el tamaño de esta prueba termina siendo fácilmente menos de la mitad del número de filas para el cálculo de la tabla de verdad. Si seguimos el patrón que he delineado con la prueba, la tesis 11 tendría 13 variables, por lo que su tabla de verdad tendría 8192 filas. Pero, la relación entre el tamaño de una prueba (número total de símbolos) y el número de filas para la tesis 11 ha disminuido de lo que hubiera sido para la tesis 9. Y si tuviéramos una secuencia interminable de pruebas de esta manera y tantas variables como números naturales, resultaría que la relación entre el tamaño de una prueba después de cierto número de pasos y el número de filas en una tabla de verdad convergería a 0.

Para una discrepancia aún mayor aquí, simplemente encontramos alguna tesis del cálculo proposicional completo que tenga una sola letra solo en el antecedente, que esa letra también pertenezca al consecuente y aún más letras en el consecuente que la tesis 1 anterior. Pero, como ejemplo particular, espero que lo anterior sea suficiente.

Editar: Como otros ejemplos donde las tablas de verdad rápidamente se vuelven aún más costosas que las pruebas formales, podríamos escoger: CpCCpCqrCCsqCsr como nuestra tesis para convertirla en nuestro axioma, o CpCCpqCCqrCCrss, o CpCCrqCCqsCCstCCprt o incluso

CaCCabCCbcCCcdCCdeCCefCCfgCCghCChiCCijCCjkCCklCClmCCmnCCnoCCopCCpqCCqrr.

Por lo tanto, aunque esta respuesta no proporciona suficiente ejemplo, quizás el método detrás de la respuesta sí lo hace.