En lógica proposicional, hay tablas de verdad. Entonces puede verificar si la estructura lógica de su argumento no es correcta en sí misma, pero si es lo que pretendía que fuera.
En la lógica de predicados, no he visto ninguna referencia a las tablas de verdad, ni he visto ningún uso (uso literal) de las tablas de verdad al buscar ejemplos en los que se usan tablas de verdad en PL.
Sería bueno verificar la estructura lógica de mis propios argumentos, ya que no siempre tendré a alguien que valide mi propio trabajo. Planeo emplear mis habilidades en lógica, pero quiero una forma segura de asegurarme de que mi forma sea correcta :)
Las tablas de verdad no son suficientes para capturar la lógica de primer orden (con cuantificadores), por lo que usamos reglas de inferencia en su lugar. Cada regla de inferencia se elige para que sea sólida, lo que significa que si comienza con declaraciones verdaderas y usa la regla, deducirá solo declaraciones verdaderas. Decimos que estas reglas preservan la verdad. Si elige con suficiente cuidado, puede hacer que las reglas no solo preserven la verdad, sino que también le permitan deducir cada declaración (bien formada) que sea necesariamente verdadera (en todas las situaciones).
Lo que probablemente esté buscando (es decir, una forma práctica de verificar rigurosamente la validez lógica de sus argumentos) es la deducción natural. Hay muchos estilos diferentes, el tipo más intuitivo es el estilo Fitch , que marca los subcontextos usando sangría o alguna demarcación visual relacionada. El siguiente sistema usa sangría y sigue la intuición más de cerca en mi opinión.
Cada línea es un encabezado o una declaración. Pondremos dos puntos después de cada encabezado y un punto después de cada declaración. Cada encabezado especifica algún subcontexto (contenido por el contexto actual), y las líneas gobernadas por ese encabezado se indican mediante la sangría. El contexto completo de cada línea está especificado por todos los encabezados que la gobiernan (es decir, todos los encabezados más cercanos por encima de ella en cada nivel de sangría inferior).
Por ejemplo, un análisis de caso anidado podría verse así:
Y razonar sobre un miembro arbitrario de una colección. se vería como:
Tenga en cuenta que lo que se afirma en algún contexto puede no ser válido en otros contextos. Una vez que comprenda el principio detrás de los contextos y la sangría, las siguientes reglas son muy naturales. También tenga en cuenta que para la lógica de primer orden, estos dos tipos de encabezados de contexto (para subcontextos condicionales y subcontextos universales, respectivamente) son los únicos tipos necesarios.
Una declaración debe ser una proposición atómica (indivisible) o una declaración compuesta formada de la manera habitual usando operaciones booleanas o cuantificadores, con la restricción de que cada variable que está limitada por un cuantificador no se usa ya para referirse a algún objeto en el contexto actual. , y que no hay cuantificadores anidados que vinculen la misma variable.
Cada regla de inferencia es de la forma:
lo que significa que si las últimas líneas que ha escrito coinciden con "X", puede escribir "Y" inmediatamente después con el mismo nivel de sangría. Cada aplicación de una regla de inferencia también está ligada al contexto actual, a saber, el contexto de "X". No mencionaremos el "contexto actual" todo el tiempo.
Toma cualquier declaración (en el contexto actual).
replantear : Si probamos algo, podemos afirmarlo nuevamente en el mismo contexto.
Tenga en cuenta que " " denota cualquier número de líneas que estén al menos en el nivel de sangría representado. En la regla anterior, esto significa que todas las líneas escritas desde la escritura anterior de " " debe estar en el mismo contexto (o en algún subcontexto).
En la práctica nunca escribimos la misma línea dos veces. Para indicar que podemos omitir una línea en una prueba, la marcaré con corchetes como este:
⇒sub ⇒restate (Podemos crear un subcontexto condicional donde sostiene.)
⇒introducción ⇒eliminación
∧introducción ∧eliminación
∨introducción ∨elim
¬introducción ¬eliminar ¬¬eliminar
Tenga en cuenta que al usar ¬intro y ¬¬elim podemos obtener la siguiente regla de inferencia adicional:
que corresponde a cómo uno intentaría probar por contradicción , es decir, mostrar que suponiendo implica una falsedad.
⇔introducción ⇔eliminar
Las reglas aquí son para cuantificadores restringidos porque generalmente pensamos en términos de ellos. Primero necesitamos algunas definiciones.
Variable utilizada : una variable que se declara en el encabezado de algún contexto contenedor o se declara en algún paso anterior de eliminación ("let") de algún contexto contenedor.
Variable no utilizada : una variable que no se utiliza.
Variable nueva : una variable que no aparece en ninguna declaración anterior en ningún contexto que la contenga.
Expresión de objeto : una expresión que hace referencia a un objeto (por ejemplo, una variable utilizada o un símbolo de función aplicado a expresiones de objeto).
Propiedad con parámetros : una cadena con algunos espacios en blanco donde cada espacio en blanco tiene alguna etiqueta de a , tal que reemplazando cada espacio en blanco en por alguna expresión de objeto produce una declaración. Si , entonces es el resultado de reemplazar cada espacio en blanco etiquetado por y reemplazando cada espacio en blanco etiquetado por . Del mismo modo para otros .
En esta sección, (si está involucrado) puede ser cualquier expresión de objeto (en el contexto actual).
Comenzamos con las siguientes reglas que proporcionan un tipo de todos los objetos.
universo : es un tipo
Ahora toma cualquier tipo y una propiedad de 1 parámetro y una variable no utilizada que no aparece en o .
∀sub ∀restate (Podemos crear un ∀-subcontexto en el que es de tipo .)
( no debe aparecer en )
∀introducción ∀eliminar
( no debe compartir ninguna variable no utilizada con )
∃ introducción ∃ elim
(dónde es una variable fresca)
= introducción = eliminar
( no debe compartir ninguna variable no utilizada con )
Finalmente, las siguientes reglas para renombrar variables son redundantes, pero acortarían las demostraciones.
∀renombrar ∃renombrar
(dónde es una variable no utilizada que no aparece en )
Por conveniencia escribimos " " como abreviatura de " ", y de manera similar para más variables y para " ". También comprimiremos los encabezados de subcontexto ∀ anidados de la siguiente forma:
a:
Además, " " es la forma abreviada de " ".
He aquí un ejemplo, donde son de cualquier tipo y es cualquier propiedad con dos parámetros.
Primero con todas las líneas mostradas:
Si
: [⇒sub]
. [⇒sub]
Deja
tal que
. [∃eliminar]
. [∃eliminar]
. [∃eliminar]
. [∀renombrar]
Dado
: [∀sub]
. [∀sub]
. [∀reiterar]
. [reafirmar]
. [∀eliminar]
. [∀reiterar]
. [∃introducción]
. [∀introducción]
. [⇒introducción]
Finalmente, con todas las líneas entre corchetes eliminadas:
Si
: [⇒sub]
Vamos
tal que
. [∃elim]
Dado
: [∀sub]
. [∀eliminar]
. [∃introducción]
. [∀introducción]
. [⇒introducción]
Esta prueba final está limpia pero aún es fácilmente verificable por computadora.
Para facilitar las definiciones , que pueden acortar significativamente las demostraciones, también tenemos las siguientes reglas de expansión definitoria.
Para cada -propiedad del parámetro y predicado-símbolo fresco :
Para cada -propiedad del parámetro y nuevo símbolo de función :
Estas reglas son redundantes en el sentido de que cualquier declaración que pueda probar que no use ninguno de los nuevos símbolos puede probarse sin usar la expansión definitoria.
Las reglas anteriores evitan el problema habitual que tienen muchos otros sistemas, donde las variables utilizadas para testigos de declaraciones existenciales deben distinguirse de las variables utilizadas para objetos arbitrarios. La razón es que cada variable aquí está especificada por un subcontexto ∀ o por una instrucción "let"; en otras palabras, no hay variables libres. El hecho de que toda variable esté ligada está fuertemente relacionado con el hecho de que este sistema permite un universo vacío, si no hay otros axiomas.
Además, cada variable se especifica mediante un encabezado único o una declaración "let" en el contexto actual; en otras palabras, no hay sombreado variable. Esto es por diseño, y en la práctica matemática real también lo cumplimos, aunque la mayoría de los otros sistemas formales no lo hacen. En consecuencia, oraciones como " ." simplemente no se puede escribir en este sistema. Si desea permitir este tipo de oraciones terribles, tendría que modificar las reglas apropiadamente, pero lo más probable es que le cause un dolor de cabeza.
Finalmente, hubo algunas decisiones técnicas sutiles. Para las reglas del cuantificador, la razón por la que exigí que no aparece en es que, si más adelante incluyéramos reglas para especificar tipos, normalmente tendríamos nombres de variables en su sintaxis, lo que daría problemas. Por ejemplo, si hemos escrito en el contexto actual " " y " ", no será sensato permitir la escritura" ". Del mismo modo, si hemos escrito " " y " ", no queremos permitir la escritura" ".
Además, para permitir que una variable se actualice nuevamente después de dejar el subcontexto en el que fue declarada, requerí que las reglas ⇒intro e ∀intro se puedan aplicar solo inmediatamente después del ⇒-subcontext o ∀-subcontext correspondiente. Sería más sencillo simplemente definir una variable nueva como una que no aparece en ninguna línea anterior, pero luego fácilmente podemos quedarnos sin nombres de variables nuevas en una prueba larga.
~ ~ ~ ~ ~ ~ ~
Para ilustrar la flexibilidad de este sistema, expresaré tanto la Aritmética de Peano como la Teoría de conjuntos como reglas adicionales que pueden agregarse simplemente al sistema.
Agrega el tipo y los símbolos de PA, a saber, los símbolos constantes y el -símbolos de función de entrada y el -input predicado-símbolo .
Añadir los axiomas de PA , adaptado de aquí :
Agregue los axiomas de inducción, es decir, para cada propiedad involucrando solo los símbolos de PA y cuantificadores sobre agregue el siguiente axioma (donde no aparece en ):
Agrega el tipo y la regla de que todo miembro de también es un tipo.
Agregue los símbolos de función unarios , los símbolos de funciones binarias , y el símbolo constante . Reutilizamos el predicado-símbolo binario , ya que no habrá ambigüedad. También agregue las siguientes reglas (en cada contexto) para la otra notación:
Agregue los siguientes axiomas:
Agregue las siguientes reglas:
notación de tipo
Tomar (en el contexto actual) cualquier propiedad y expresión de objetos y variable no utilizada .
Entonces es un tipo y su pertenencia se rige por:
. ( no debe aparecer en o )
comprensión
Tomar cualquier propiedad y variable no utilizada .
. ( no debe aparecer en o )
reemplazo
Tomar cualquiera -propiedad del parámetro y variables no utilizadas .
( no debe aparecer en o )
inducción
Tomar cualquier propiedad con parámetro de .
( no debe aparecer en )
La regla de inducción subsume los axiomas de inducción para PA, y esencialmente la única diferencia es que la propiedad puede involucrar operaciones de conjuntos y cuantificación sobre conjuntos.
notación de función
Esta regla es teóricamente innecesaria pero pragmáticamente muy conveniente (también conocida como expresiones lambda en informática).
Toma cualquier conjunto y cualquier expresión de objeto con parámetro de y variable no utilizada .
Entonces es un objeto y su comportamiento se rige por:
La combinación de la Aritmética de Peano anterior más la Teoría de conjuntos produce un sistema fundamental que es esencialmente tan fuerte como ZFC pero mucho más fácil de usar. También es agnóstico a la existencia de objetos que no son conjuntos, y ni siquiera asume que los miembros de son conjuntos. También trata los productos cartesianos y los pares ordenados como nociones abstractas incorporadas. Así es como los usamos en las matemáticas reales. (Más precisamente, el sistema anterior interpreta directamente ZFC menos la regularidad).
Hagen von Eitzen
Dan Christensen
Stefan Mesken