Las matemáticas tienen muchos símbolos. Algunos pueden decir demasiados símbolos. Así que hagamos un poco de matemáticas con imágenes
Vamos a tener un papel, en el que nos basaremos. Para comenzar el papel está vacío, diremos que es equivalente a o .
Si escribimos otras cosas en el papel, también serán ciertas.
Por ejemplo
Indica que las afirmaciones y son verdaderas.
Ahora digamos que si dibujamos un círculo alrededor de alguna declaración, esa declaración es falsa. Esto representa lógico no.
Por ejemplo:
Indica que es falso y Q es verdadero.
Incluso podemos colocar el círculo alrededor de múltiples subdeclaraciones:
Dado que la parte dentro del círculo normalmente se lee como al poner un círculo a su alrededor, significa que no ( P y Q ) . Incluso podemos anidar círculos
Esto se lee como .
Si dibujamos un círculo sin nada dentro, eso representa o falso .
Como el espacio vacío era verdadero, entonces la negación de lo verdadero es falsa.
Ahora, usando este método visual simple, podemos representar cualquier declaración en lógica proposicional.
Pruebas
El siguiente paso después de poder representar declaraciones es poder probarlas. Para las pruebas tenemos 4 reglas diferentes que se pueden usar para transformar un gráfico. Siempre comenzamos con una hoja vacía que, como sabemos, es una verdad vacía y luego usamos estas diferentes reglas para transformar nuestra hoja de papel vacía en un teorema.
Nuestra primera regla de inferencia es la inserción .
Inserción
Llamaremos al número de negaciones entre un sub-gráfico y el nivel superior es "profundidad". Inserción nos permite introducir cualquier declaración que deseamos a una profundidad extraña.
Aquí hay un ejemplo de nosotros realizando la inserción:
Borradura
La siguiente regla de inferencia es Erasure . Erasure nos dice que si tenemos una declaración que está a una profundidad uniforme, podemos eliminarla por completo.
Aquí hay un ejemplo de borrado aplicado:
Corte doble
Double Cut es una equivalencia. Lo que significa que, a diferencia de las inferencias anteriores, también se puede revertir. Doble corte nos dice que podemos dibujar dos círculos alrededor de cualquier gráfico secundario, y si hay dos círculos alrededor de un gráfico secundario, podemos eliminarlos a ambos.
Aquí está un ejemplo de la doble corte que se utiliza
Iteración
La iteración también es una equivalencia. 1 Su reverso se llama Deiteración. Si tenemos una declaración y un corte en el mismo nivel, podemos copiar esa declaración dentro de un corte.
Por ejemplo:
La deiteración nos permite revertir una iteración . Una declaración puede eliminarse mediante Deiteración si existe una copia de la misma en el siguiente nivel.
Este formato de representación y prueba no es de mi propia invención. Son una modificación menor de una lógica esquemática que se denominan Gráficos existenciales alfa . Si desea leer más sobre esto, no hay mucha literatura, pero el artículo vinculado es un buen comienzo.
Tarea
Su tarea será probar el siguiente teorema:
Esto, cuando se traduce a la simbolización lógica tradicional es
.
También conocido como el Axioma Łukasiewicz-Tarski .
Puede parecer complicado, pero los gráficos existenciales son muy eficientes cuando se trata de la longitud de la prueba. Seleccioné este teorema porque creo que es una longitud apropiada para un rompecabezas divertido y desafiante. Si tiene problemas con este, le recomendaría probar algunos teoremas más básicos primero para familiarizarse con el sistema. Puede encontrar una lista de estos en la parte inferior de la publicación.
Esto es prueba de golf, por lo que su puntaje será el número total de pasos en su prueba de principio a fin. El objetivo es minimizar tu puntaje.
Formato
El formato para este desafío es flexible; puede enviar respuestas en cualquier formato que sea claramente legible, incluidos los formatos dibujados a mano o renderizados. Sin embargo, para mayor claridad, sugiero el siguiente formato simple:
Representamos un corte con paréntesis, todo lo que estamos cortando se coloca dentro de los parentescos. El corte vacío sería solo,
()
por ejemplo.Representamos átomos con solo sus letras.
Como ejemplo, aquí está la declaración de objetivos en este formato:
(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))
Este formato es bueno porque es legible tanto para humanos como para máquinas, por lo que incluirlo en tu publicación sería bueno.
En cuanto a su trabajo real, le recomiendo lápiz y papel cuando haga ejercicio. Me parece que el texto no es tan intuitivo como el papel cuando se trata de gráficos existenciales.
Prueba de ejemplo
En este ejemplo, demostraremos el siguiente teorema:
Prueba:
Teoremas de práctica
Aquí hay algunos teoremas simples que puede usar para practicar el sistema:
Segundo axioma de Łukasiewicz
El axioma de Meredith
1: La mayoría de las fuentes usan una versión más sofisticada y poderosa de Iteration , pero para mantener este desafío simple, estoy usando esta versión. Son funcionalmente equivalentes.
fuente
Respuestas:
19 pasos
(())
[doble corte](AB()(((G))))
[inserción](AB(A)(((G))))
[iteración](((AB(A)))(((G))))
[doble corte](((AB(A))(((G))))(((G))))
[iteración](((AB(A))(((G))))((H(G))))
[inserción](((AB(A))(((G)(()))))((H(G))))
[doble corte](((AB(A))(((DE()(C)(F))(G))))((H(G))))
[inserción](((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G))))
[iteración](((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G))))
[iteración](((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G))))
[doble corte](((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G))))
[iteración](((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G))))
[doble corte](((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[doble corte](((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[doble corte](((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[doble corte](((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[doble corte](((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[doble corte](((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[doble corte]Practica teoremas
Segundo axioma de Łukasiewicz: 7 pasos
(())
[doble corte](A()(B)(C))
[inserción](A(A(B))(B)(C))
[iteración](A(AB(C))(A(B))(C))
[iteración]((AB(C))(A(B))((A(C))))
[doble corte]((AB(C))(((A(B))((A(C))))))
[doble corte]((A((B(C))))(((A(B))((A(C))))))
[doble corte]El axioma de Meredith: 11 pasos
(())
[doble corte](()(D(A)(E)))
[inserción]((D(A)(E))((D(A)(E))))
[iteración]((D(A)(E))((D(A)(E(A)))))
[iteración]((D(A)(E))(((E(A))((D(A))))))
[doble corte](((E)((D(A))))(((E(A))((D(A))))))
[doble corte](((E)((C)(D(A))))(((E(A))((D(A))))))
[inserción](((E)((C)(D(A)(C))))(((E(A))((D(A))))))
[iteración](((E)((C)((A)(C)((D)))))(((E(A))((D(A))))))
[doble corte](((E)((C)((A)(((C)((D)))))))(((E(A))((D(A))))))
[doble corte](((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A))))))
[inserción]Haskell buscador de pruebas
(¿Qué, pensaste que iba a hacer eso a mano? :-P)
Esto solo intenta la inserción, la introducción de doble corte y la iteración. Por lo tanto, aún es posible que estas soluciones se superen mediante el borrado, la eliminación de doble corte o la deiteración.
fuente
22 pasos
(((())(())))
(((AB())(CDE(F)()))H(G))
(((AB(A))(CDE(F)(CD(F)))(G))H(G))
(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G))))
(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G))))
[Iteración](((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(C((D(F)))))))(G))))((H(G))))
[Doble corte x5](((A((B(A))))(((((C)((D((E)))))((((((D)E)E(F)))(C((D(F)))))))(G))))((H(G))))
[Iteración](((A((B(A))))(((((C)((D((E)))))((((((D)E)((E(F)))))(C((D(F)))))(G))))))((H(G))))
[Doble corte]Algunas cosas que aprendí al completar este rompecabezas:
Reducir la representación provista. Esto implica invertir dobles cortes e iteraciones. Por ejemplo, este axioma se reduce
(((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))
después de revertir los cortes dobles y(((AB(A))(()CDE(F)))H(G)))
después de revertir las iteraciones.Busca átomos perdidos. Por ejemplo, H se usa como una variable ficticia y, por lo tanto, se puede insertar en cualquier punto.
Soluciones de teorema de práctica:
Solución para el segundo axioma de Łukasiewicz: [8 pasos]
(())
[Doble corte](()AB(C))
[Inserción]((AB(C))AB(C))
[Iteración]((A((B(C))))A((B))(C))
[Doble corte x2]((A((B(C))))A(A(B))(C))
[Iteración]((A((B(C))))(((A(B))((A(C))))))
[Doble corte x2]Solución para el Axioma de Meredith: [12 pasos]
(())
[Doble corte](()(A)D(E))
[Inserción](((A)D(E))(A)D(E(A)))
[Iteración x2](((((A)D))(E))(A)D(E(A)))
[Doble corte](((((A(B))D)(C))(E))(A)D(E(A)))
[Inserción x2](((((A(B))(C)D)(C))(E))(A)D(E(A)))
(((((A(B))(((C)((D)))))(C))(E))(((((A)D))(E(A)))))
fuente
\$
como principio / fin, lo que creo que haría que su solución sea mucho más fácil de leer. Espero que