stringtranslate.com

Sistema formal

Un sistema formal es una estructura abstracta y formalización de un sistema axiomático utilizado para deducir , mediante reglas de inferencia , teoremas a partir de axiomas mediante un conjunto de reglas de inferencia . [1]

En 1921, David Hilbert propuso utilizar sistemas formales como base del conocimiento en matemáticas . [2]

El término formalismo es a veces un sinónimo aproximado de sistema formal , pero también se refiere a un estilo determinado de notación , por ejemplo, la notación bra-ket de Paul Dirac .

Conceptos

Este diagrama muestra las entidades sintácticas que se pueden construir a partir de lenguajes formales . Los símbolos y las cadenas de símbolos se pueden dividir en general en fórmulas sin sentido y fórmulas bien formadas . Se puede pensar que un lenguaje formal es idéntico al conjunto de sus fórmulas bien formadas, que se pueden dividir en general en teoremas y no teoremas.

Un sistema formal tiene lo siguiente: [3] [4] [5]

Se dice que un sistema formal es recursivo (es decir, efectivo) o recursivamente enumerable si el conjunto de axiomas y el conjunto de reglas de inferencia son conjuntos decidibles o conjuntos semidecidibles , respectivamente.

Lenguaje formal

Un lenguaje formal es un lenguaje que se define mediante un sistema formal. Al igual que los lenguajes en lingüística , los lenguajes formales generalmente tienen dos aspectos:

Por lo general, solo se considera la sintaxis de un lenguaje formal a través de la noción de gramática formal . Las dos categorías principales de gramática formal son las gramáticas generativas , que son conjuntos de reglas sobre cómo se pueden escribir las cadenas en un lenguaje, y las gramáticas analíticas (o gramática reductiva [6] [7] ), que son conjuntos de reglas sobre cómo se puede analizar una cadena para determinar si es un miembro del lenguaje.

Sistema deductivo

Un sistema deductivo , también llamado aparato deductivo , [8] consiste en los axiomas (o esquemas axiomáticos ) y reglas de inferencia que pueden usarse para derivar teoremas del sistema. [9]

Estos sistemas deductivos conservan cualidades deductivas en las fórmulas que se expresan en el sistema. Por lo general, la cualidad que nos interesa es la verdad en oposición a la falsedad. Sin embargo, otras modalidades , como la justificación o la creencia, pueden conservarse en su lugar.

Para mantener su integridad deductiva, un aparato deductivo debe ser definible sin referencia a ninguna interpretación intencionada del lenguaje. El objetivo es asegurar que cada línea de una derivación sea meramente una consecuencia lógica de las líneas que la preceden. No debe haber ningún elemento de interpretación del lenguaje que interfiera con la naturaleza deductiva del sistema.

La consecuencia lógica (o implicación) del sistema por su fundamento lógico es lo que distingue a un sistema formal de otros que pueden tener alguna base en un modelo abstracto. A menudo, el sistema formal será la base o incluso se identificará con una teoría o campo más amplio (por ejemplo, la geometría euclidiana ) coherente con el uso en las matemáticas modernas, como la teoría de modelos . [ Aclaración necesaria ]

Un ejemplo de un sistema deductivo serían las reglas de inferencia y los axiomas sobre la igualdad utilizados en la lógica de primer orden .

Los dos tipos principales de sistemas deductivos son los sistemas de prueba y la semántica formal. [8]

Sistema de prueba

Las demostraciones formales son secuencias de fórmulas bien formadas (o WFF, por sus siglas en inglés) que pueden ser un axioma o ser el producto de aplicar una regla de inferencia sobre las WFF anteriores en la secuencia de demostraciones. La última WFF en la secuencia se reconoce como un teorema .

Una vez que se da un sistema formal, se puede definir el conjunto de teoremas que se pueden demostrar dentro del sistema formal. Este conjunto consta de todas las FBF para las que existe una demostración. Por lo tanto, todos los axiomas se consideran teoremas. A diferencia de la gramática para las FBF, no hay garantía de que exista un procedimiento de decisión para decidir si una FBF dada es un teorema o no.

El punto de vista de que la generación de pruebas formales es todo lo que hay en matemáticas se suele llamar formalismo . David Hilbert fundó la metamatemática como disciplina para discutir sistemas formales. Cualquier lenguaje que se utilice para hablar sobre un sistema formal se llama metalenguaje . El metalenguaje puede ser un lenguaje natural, o puede estar parcialmente formalizado en sí mismo, pero generalmente está menos formalizado por completo que el componente de lenguaje formal del sistema formal en examen, que entonces se llama lenguaje objeto , es decir, el objeto de la discusión en cuestión. La noción de teorema que se acaba de definir no debe confundirse con los teoremas sobre el sistema formal , que, para evitar confusiones, suelen llamarse metateoremas .

Semántica formaldel sistema lógico

Un sistema lógico es un sistema deductivo (más comúnmente, lógica de primer orden ) junto con axiomas no lógicos adicionales . Según la teoría de modelos , a un sistema lógico se le pueden dar interpretaciones que describan si una estructura dada (la aplicación de fórmulas a un significado particular) satisface una fórmula bien formada. Una estructura que satisface todos los axiomas del sistema formal se conoce como modelo del sistema lógico.

Un sistema lógico es:

Un ejemplo de un sistema lógico es la aritmética de Peano . El modelo estándar de la aritmética establece que el dominio del discurso sean los números enteros no negativos y otorga a los símbolos su significado habitual. [10] También existen modelos no estándar de la aritmética .

Historia

Los primeros sistemas lógicos incluyen la lógica india de Pāṇini , la lógica silogística de Aristóteles, la lógica proposicional del estoicismo y la lógica china de Gongsun Long (c. 325-250 a. C.). En tiempos más recientes, entre los contribuyentes se incluyen George Boole , Augustus De Morgan y Gottlob Frege . La lógica matemática se desarrolló en la Europa del siglo XIX .

David Hilbert instigó un movimiento formalista llamado el programa de Hilbert como una solución propuesta a la crisis fundacional de las matemáticas , que finalmente fue atenuada por los teoremas de incompletitud de Gödel . [2] El manifiesto QED representó un esfuerzo posterior, aún infructuoso, de formalización de las matemáticas conocidas.

Véase también

Referencias

  1. ^ "Sistema formal | Lógica, símbolos y axiomas | Britannica". www.britannica.com . Consultado el 10 de octubre de 2023 .
  2. ^ ab Zach, Richard (31 de julio de 2003). "El programa de Hilbert". Programa de Hilbert, Stanford Encyclopedia of Philosophy . Metaphysics Research Lab, Universidad de Stanford.
  3. ^ "sistema formal". planetmath.org . Consultado el 10 de octubre de 2023 .
  4. ^ Rapaport, William J. (25 de marzo de 2010). "Sintaxis y semántica de los sistemas formales". Universidad de Buffalo .
  5. ^ "Definición:Sistema formal - ProofWiki". proofwiki.org . Consultado el 16 de octubre de 2023 .
  6. ^ Gramática reductiva: ( ciencia informática ) Un conjunto de reglas sintácticas para el análisis de cadenas para determinar si las cadenas existen en un lenguaje. "Sci-Tech Dictionary McGraw-Hill Dictionary of Scientific and Technical Terms" (6.ª ed.). McGraw-Hill.[ fuente poco confiable? ] Acerca del autor Compilado por los editores de la Enciclopedia McGraw-Hill de Ciencia y Tecnología (Nueva York, NY), un personal interno que representa la vanguardia de las habilidades, el conocimiento y la innovación en la publicación científica. [1]
  7. ^ "Existen dos clases de esquemas de escritura de compiladores de definiciones de lenguaje formal. El enfoque de gramática productiva es el más común. Una gramática productiva consiste principalmente en un conjunto de reglas que describen un método para generar todas las cadenas posibles del lenguaje. La técnica de gramática reductiva o analítica establece un conjunto de reglas que describen un método para analizar cualquier cadena de caracteres y decidir si esa cadena está en el lenguaje". "El sistema compilador-compilador TREE-META: un sistema de compilador meta para Univac 1108 y General Electric 645, Informe técnico RADC-TR-69-83 de la Universidad de Utah. C. Stephen Carr, David A. Luther, Sherian Erdmann" (PDF) . Consultado el 5 de enero de 2015 .
  8. ^ ab «Definición: Aparato deductivo - ProofWiki». proofwiki.org . Consultado el 10 de octubre de 2023 .
  9. ^ Hunter, Geoffrey, Metalogic: Una introducción a la metateoría de la lógica estándar de primer orden, University of California Press, 1971
  10. ^ Kaye, Richard (1991). "1. El modelo estándar". Modelos de aritmética de Peano . Oxford: Clarendon Press. pág. 10. ISBN 9780198532132.

Lectura adicional

Enlaces externos