¿Qué significa "probar"?

Question

¿Qué significa "probar"?

Estoy usando los siguientes ejemplos para comprender los casos generales. No sé cómo articular mis preguntas en el caso general. Me preguntaba a qué niveles se enuncian los siguientes, cómo se formulan los siguientes y qué diferencias y relaciones hay entre ellos:

1. Demuestra una fórmula $p$. ¿Significa probar$ \vdash p$ (o $\models p$?), y por lo tanto convertir la tarea a 3 a continuación? (Es posible que haya preguntado esto en algún comentario, y alguien puede haber respondido que probar$p$ medios para probar $\vdash p$, pero no puedo encontrar los comentarios).

2. Demuestra si $\phi$, luego $\psi$. ¿Qué significa probar:$\phi \to \psi$, $\phi \vdash \psi$o $\phi \models \psi$y, por lo tanto, convertir la tarea en 1 arriba o 3 debajo?

3. Probar $\phi \vdash \psi$.

   • ¿Significa derivar $\phi \vdash \psi$, utilizando las reglas de inferencia y axiomas en un sistema de prueba dado (por ejemplo, cálculo secuencial)?

   • O trata $\phi \vdash \psi$ como fórmula en un idioma de un nivel superior al idioma que contiene $\phi$ y $\psi$y probar $\vdash (\phi \vdash \psi)$ aplicando un sistema de prueba dado (por ejemplo, cálculo secuencial) a este lenguaje de nivel superior?

4. Demuestra si $\phi' \vdash \psi'$, luego $\phi \vdash \psi$.

   • ¿Significa derivar $\phi \vdash \psi$, mediante el uso $\phi' \vdash \psi'$, y las reglas de inferencia y axiomas en un sistema de prueba dado (por ejemplo, cálculo secuencial)?

   • O trata $\phi' \vdash \psi'$ y $\phi \vdash \psi$ como fórmulas en un idioma de un nivel superior al idioma que contiene $\phi$, $\psi$, $\phi'$ y $\psi'$y probar $(\phi' \vdash \psi') \vdash (\phi \vdash \psi)$ aplicando un sistema de prueba dado (por ejemplo, cálculo secuencial) a este lenguaje de nivel superior?

5. y 6. Considere reemplazar $\vdash$ con $\models$ en 3 y 4

Algo relacionado: pregunté :

¿Se aplica "demostrable" o "refutable" solo a las fórmulas, no a "una inferencia" o "derivación" como $∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$? Podemos reescribir$∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$ como una fórmula, de modo que sea derivable (casi) si y solo si la fórmula correspondiente es demostrable?

lemontree respondió :

"Demostrable" significa "derivable sin premisas", es decir, la demostrabilidad es una propiedad de las fórmulas mientras que la derivabilidad es una propiedad de las inferencias en general. Lo que está buscando es probablemente el teorema de deducción también conocido como teorema de importación-exportación, que establece que$𝐴_1,…,𝐴_𝑛⊢𝐵$ si y solo si $⊢(𝐴_1∧…∧𝐴_𝑛)→𝐵$. Así, con$∃𝑥𝑅(𝑥)⊬∀𝑦𝑅(𝑦)$ tenemos eso $⊬∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$, es decir, la fórmula $∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$ no es demostrable.

Supongo que mis preguntas anteriores son una cuestión de metalenguaje o teoría de la prueba, y sé poco sobre ellas. Al mismo tiempo, también me preguntaba ¿Cómo se formulan las técnicas de prueba en lógica matemática? , que podría ser parte de la teoría de la prueba?

Gracias.

Answer 1

“Probar” en matemáticas significa escribir una prueba de un enunciado en el contexto de una teoría matemática. Una prueba será un "argumento" a partir de los axiomas de la teoría y resultados probados previos y concluyendo con el enunciado que se va a probar que utiliza pasos deductivos lógicos "correctos" (es decir, un argumento válido ).

En lógica tenemos el concepto de derivación, es decir, el modelo matemático formal de una prueba en el contexto de un cálculo lógico, por ejemplo, deducción natural .

Los pasos lógicos deductivos generalmente se formalizan a través de reglas de inferencia , que son los bloques de construcción básicos del sistema de prueba , también conocido como "cálculo lógico".

Tratando de seguir el libro de texto de Ebbinghaus, el símbolo $\vDash$es una expresión de metalenguaje utilizada en el contexto semántico con diferentes usos: flanqueada a la derecha por una fórmula abrevia “es válido” (página 35); entre el nombre de un conjunto de fórmulas y una fórmula abrevia “es una consecuencia de” (página 33).

Finalmente, flanqueado por el nombre de una interpretación y una fórmula abrevia "es cierto bajo la interpretación".

No forma parte del lenguaje formal del cálculo: se utiliza para expresar propiedades de las fórmulas del cálculo; en el contexto del cálculo proposicional , leemos la expresión "$⊨ A ∨ ¬A$"como" fórmula ... es una tautología ", es decir, es una fórmula válida de cálculo proposicional.

Podemos probar (en la metateoría) que la fórmula $A ∨ ¬A$es una tautología que usa el método de la tabla de verdad (esta "prueba" es una prueba matemática y no una derivación en el cálculo).

Similar para el símbolo $\vdash$ (ver definición en la página 61).

Siguiendo a Ebbinghaus, $\varphi \to \varphi$ es una fórmula, es decir, una expresión del lenguaje formal que leemos: "si $\varphi$, luego $\varphi$”.

Podemos derivarlo fácilmente en el sistema de prueba y simbolizamos la existencia de tal derivación con $\vdash \varphi \to \varphi$ que de nuevo no es una fórmula del lenguaje formal sino una expresión del metalenguaje abreviando la declaración: "hay una derivación de ...." y lo leemos (según la respuesta a su publicación anterior): "fórmula. .. es derivable (en el cálculo) ".

Desafortunadamente, en algunas formulaciones de ND y cálculo secuencial, el símbolo $\vdash$es parte del lenguaje formal, en cuyo caso podemos tener problemas para utilizarlo también en la metateoría .

Finalmente, tenemos que considerar el Teorema de Solidez y Completitud , un meta-teorema que se aplica tanto al cálculo proposicional como al predicado uno (ver página 70 y página 75) que dice en pocas palabras:

"$\vdash \text { iff } \vDash$”.

Este teorema expresa una propiedad del cálculo y su semántica. Lo probamos de una manera matemática "estándar".

Como se dijo anteriormente, podemos usar la tabla de verdad para demostrar que $A ∨ ¬A$ es una tautología$⊨ A ∨ ¬A$) y luego use Integridad para demostrar $⊢ A ∨ ¬A$.

De esta manera, usamos un argumento (tabla de verdad) para probar una propiedad "semántica" de una determinada fórmula y luego usamos un meta-teorema (Completitud) para probar una segunda propiedad de la misma fórmula: la existencia de una derivación en el correspondiente sistema de prueba.

Esta es la esencia de los dos símbolos omnipresentes .