Hispanopedia Wiki
Articulo de referencia

Prueba formal

En lógica y matemáticas , una demostración o derivación formal es una secuencia finita de enunciados (conocidos como fórmulas bien formadas en el lenguaje formal ), cada uno de ...

Hispanopedia WikiContenido en espanolLectura gratuita

En lógica y matemáticas , una demostración o derivación formal es una secuencia finita de enunciados (conocidos como fórmulas bien formadas en el lenguaje formal ), cada uno de los cuales es un axioma , una suposición o se deduce de los enunciados precedentes en la secuencia, según la regla de inferencia . Se diferencia de un argumento en lenguaje natural en que es riguroso, inequívoco y mecánicamente verificable. [ 1 ] Si el conjunto de suposiciones está vacío, el último enunciado de una demostración formal se denomina teorema del sistema formal . La noción de teorema es generalmente efectiva , pero puede que no exista un método que nos permita encontrar de forma fiable una demostración de un enunciado dado o determinar que no existe ninguna. Los conceptos de demostración al estilo Fitch , cálculo de secuentes y deducción natural son generalizaciones del concepto de demostración. [ 2 ] [ 3 ]

El teorema es una consecuencia sintáctica de todas las fórmulas bien formadas que lo preceden en la demostración. Para que una fórmula bien formada se considere parte de una demostración, debe ser el resultado de aplicar una regla del aparato deductivo (de algún sistema formal) a las fórmulas bien formadas anteriores en la secuencia de la demostración.

Las demostraciones formales a menudo se construyen con la ayuda de computadoras en la demostración interactiva de teoremas (por ejemplo, mediante el uso de verificadores de pruebas y demostradores automáticos de teoremas ). [ 4 ] Es importante destacar que estas demostraciones pueden verificarse automáticamente, también por computadora. La verificación de demostraciones formales suele ser sencilla, mientras que el problema de encontrar demostraciones (demostración automática de teoremas) suele ser computacionalmente intratable y/o solo semidecidible , dependiendo del sistema formal utilizado.

Fondo

Lenguaje formal

Un lenguaje formal es un conjunto de secuencias finitas de símbolos . Dicho lenguaje puede definirse sin referencia a ningún significado de sus expresiones; puede existir antes de que se le asigne cualquier interpretación , es decir, antes de que tenga significado alguno. Las demostraciones formales se expresan en algunos lenguajes formales.

Gramática formal

Una gramática formal (también llamada reglas de formación ) es una descripción precisa de las fórmulas bien formadas de un lenguaje formal. Es sinónimo del conjunto de cadenas sobre el alfabeto del lenguaje formal que constituyen fórmulas bien formadas. Sin embargo, no describe su semántica (es decir, su significado).

Sistemas formales

Un sistema formal (también llamado cálculo lógico o sistema lógico ) consta de un lenguaje formal junto con un aparato deductivo (también llamado sistema deductivo ). El aparato deductivo puede consistir en un conjunto de reglas de transformación (también llamadas reglas de inferencia ) o un conjunto de axiomas , o bien ambos. Un sistema formal se utiliza para derivar una expresión a partir de una o más expresiones.

Interpretaciones

La interpretación de un sistema formal consiste en asignar significados a los símbolos y valores de verdad a las oraciones de dicho sistema. El estudio de las interpretaciones se denomina semántica formal . Dar una interpretación es sinónimo de construir un modelo .

Véase también

Referencias

  1. ↑ Kassios, Yannis (20 de febrero de 2009). "Prueba formal" (PDF) . cs.utoronto.ca . Consultado el 12 de diciembre de 2019 .
  2. ↑ Diccionario de Filosofía de Cambridge, deducción
  3. ↑ Barwise, Jon; Etchemendy, John Etchemendy (1999). Lenguaje, demostración y lógica (1.ª ed.). Seven Bridges Press y CSLI. 
  4. ↑ Harrison, John (diciembre de 2008). "Prueba formal: teoría y práctica" (PDF) . ams.org . Consultado el 12 de diciembre de 2019 .
  • "Número especial sobre demostración formal" . Notices of the American Mathematical Society . Diciembre de 2008.
  • 2πix.com: Lógica. Parte de una serie de artículos que abarcan matemáticas y lógica.
  • Archivo de Pruebas Formales
  • Página principal de Mizar
  • Pr∞fWiki, Definición: Sistema de prueba/Prueba formal
Lecturas relacionadas
6 articulos
Cartel de 1901LógicaLa lógica estudia formas válidas de inferencia como el modus ponens . La lógica es el estudio del razonamiento correcto . Incluye tanto la lógica f...MatemáticasMatemáticasLas matemáticas son un campo de estudio que descubre y organiza métodos, teorías y teoremas que se desarrollan y prueban para las necesidades de la...SecuenciaUna secuencia infinita de números reales (en azul). Esta secuencia no es ni creciente ni decreciente, ni convergente ni de Cauchy . Sin embargo, es...ProposiciónProposiciónUna proposición es un concepto central en la filosofía del lenguaje , la semántica , la lógica y campos relacionados, a menudo caracterizado como e...{\displaystyle (A\land (B\lor C))}Fórmula bien formadaEn lógica matemática , lógica proposicional y lógica de predicados , una fórmula bien formada , abreviada WFF o wff , a menudo simplemente fórmula ...Lenguaje formalEstructura de la oración inglesa, sintácticamente bien formada, aunque completamente absurda, "Las ideas verdes e incoloras duermen furiosamente" (...