Hispanopedia WikiUn sistema formal (o sistema deductivo ) es una estructura abstracta y una formalización de un sistema axiomático que se utiliza para deducir , mediante reglas de inferencia , teoremas a partir de axiomas . [ 1 ]
En 1921, David Hilbert propuso utilizar sistemas formales como fundamento del conocimiento en matemáticas . [ 2 ] Sin embargo, en 1931 Kurt Gödel demostró que ningún sistema formal consistente , lo suficientemente potente como para expresar la aritmética básica, puede probar su propia completitud . Esto demostró, en efecto, que el programa de Hilbert era imposible tal como se planteaba.
El término formalismo es a veces un sinónimo aproximado de sistema formal , pero también se refiere a un estilo de notación determinado , por ejemplo, la notación bra-ket de Paul Dirac .
Conceptos
Un sistema formal tiene como mínimo los siguientes componentes: [ 3 ] [ 4 ] [ 5 ]
- El lenguaje formal es un conjunto de fórmulas bien formadas , que son cadenas de símbolos de un alfabeto , formadas por una gramática formal (que consta de reglas de producción o reglas de formación ).
- Sistema deductivo, aparato deductivo o sistema de prueba , que tiene reglas de inferencia que toman axiomas e infieren teoremas , ambos parte del lenguaje formal.
- En algunos casos, se utiliza un sistema inductivo para derivar una demostración estableciendo primero un caso simple y luego generalizándolo.
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 utiliza un conjunto de cadenas cuyos símbolos se toman de un alfabeto específico, y operaciones que se utilizan para formar oraciones a partir de ellas. Al igual que los lenguajes en lingüística , los lenguajes formales generalmente tienen dos aspectos:
- La sintaxis es la apariencia del lenguaje (más formalmente: el conjunto de expresiones posibles que son enunciados válidos en el lenguaje).
- La semántica es el significado de las expresiones del lenguaje (que se formaliza de diversas maneras, dependiendo del tipo de lenguaje en cuestión).
Por lo general, solo se considera la sintaxis de un lenguaje formal a través de la noción de una 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 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 ] consta de los axiomas (o esquemas axiomáticos ) y reglas de inferencia que pueden usarse para derivar teoremas del sistema. [ 1 ]
Para mantener su integridad deductiva, un aparato deductivo debe poder definirse sin referencia a ninguna interpretación del lenguaje. El objetivo es asegurar que cada línea de una derivación sea simplemente una consecuencia lógica de las líneas que la preceden. Ningún elemento de interpretación del lenguaje debe interferir con la naturaleza deductiva del sistema.
La consecuencia lógica (o implicación) del sistema, derivada de su fundamento lógico, es lo que distingue un sistema formal de otros que pueden tener alguna base en un modelo abstracto. A menudo, el sistema formal será la base de, o incluso se identificará con, una teoría o campo más amplio (por ejemplo, la geometría euclidiana ), en consonancia con el uso en matemáticas modernas como la teoría de modelos .
Un ejemplo de sistema deductivo serían las reglas de inferencia y los axiomas sobre 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 ] [ 9 ]
Sistema de prueba
Las demostraciones formales son secuencias de fórmulas bien formadas (o FBF, por sus siglas en inglés) que pueden ser un axioma o el resultado de aplicar una regla de inferencia a FBF anteriores en la secuencia de demostración.
Una vez establecido un sistema formal, se puede definir el conjunto de teoremas que pueden demostrarse dentro de dicho sistema. Este conjunto comprende todas las fórmulas bien formadas (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 existe garantía de que haya un procedimiento de decisión para determinar si una FBF dada es un teorema o no.
La perspectiva que considera que generar demostraciones formales es todo lo que hay en matemáticas se suele denominar formalismo . David Hilbert fundó la metamatemática como una disciplina para analizar sistemas formales. Cualquier lenguaje que se utilice para hablar de un sistema formal se denomina metalenguaje . El metalenguaje puede ser un lenguaje natural o estar parcialmente formalizado, pero generalmente está menos formalizado que el componente de lenguaje formal del sistema formal en estudio, que entonces se denomina lenguaje objeto , es decir, el objeto de la discusión en cuestión. La noción de teorema que acabamos de definir no debe confundirse con los teoremas sobre el sistema formal , que, para evitar confusiones, suelen denominarse metateoremas .
Semántica formal de los sistemas lógicos
Un sistema lógico es un sistema deductivo (generalmente lógica de primer orden ) junto con axiomas no lógicos adicionales . Según la teoría de modelos , un sistema lógico puede interpretarse de manera que se describa si una estructura dada —la correspondencia entre fórmulas y 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:
- Sólido , si cada fórmula bien formada que se puede inferir de los axiomas es satisfecha por cada modelo del sistema lógico.
- Semánticamente completo , si cada fórmula bien formada que satisface cada modelo del sistema lógico puede inferirse a partir de los axiomas.
Un ejemplo de sistema lógico es la aritmética de Peano . El modelo estándar de aritmética establece el dominio del discurso como los enteros no negativos y da a los símbolos su significado habitual. [ 10 ] También existen modelos no estándar de aritmética .
Historia
Entre los primeros sistemas lógicos se encuentran 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 épocas más recientes, destacan figuras como George Boole , Augustus De Morgan y Gottlob Frege . La lógica matemática se desarrolló en la Europa del siglo XIX .
David Hilbert impulsó 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, hasta entonces infructuoso, de formalización de las matemáticas conocidas.
Véase también
- Lista de sistemas formales
- Método formal – Especificaciones del programa matemático Páginas que muestran breves descripciones de los destinos de redirección
- Ciencia formal : estudio de estructuras abstractas descritas por sistemas formales.
- Traducción lógica : traducción de un texto a un sistema lógico.
- Sistema de reescritura : Reemplazo de un subtérmino en una fórmula por otro término. Páginas que muestran descripciones breves de los destinos de redireccionamiento.
- Instancia de sustitución : concepto en lógica. Páginas que muestran descripciones breves de los destinos de redirección.
- Teoría (lógica matemática) – Conjunto de enunciados en un lenguaje formal
Referencias
- 1 2 Hunter 1996 , pág. 7.
- 1 2 Zach, Richard (31 de julio de 2003). "El programa de Hilbert" . El programa de Hilbert, Enciclopedia de Filosofía de Stanford . Laboratorio de Investigación en Metafísica, Universidad de Stanford.
- ↑ "Sistema formal" . PlanetMath .
- ↑ Rapaport, William J. (25 de marzo de 2010). "Sintaxis y semántica de los sistemas formales" . Universidad de Buffalo .
- ↑ "Sistema formal" . PrfWiki .
- ↑ "Gramática reductiva" . Diccionario de términos científicos y técnicos (6.ª ed.). McGraw-Hill.
Gramática reductiva: (
informática
) Un conjunto de reglas sintácticas para el análisis de cadenas de caracteres con el fin de determinar si dichas cadenas existen en un lenguaje.
- ↑ Rulifson, Johns F. (abril de 1968). "A Tree Meta for the XDS 940" (PDF) . Augmentation Research Center . Recuperado el 30 de noviembre de 2024.
Hay dos clases de esquemas de escritura de compiladores de definiciones de lenguajes formales. 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.
- 1 2 "Aparato deductivo" . PrfWiki . Consultado el 30 de noviembre de 2024 .
- ↑ van Fraassen, Bas C. (2016) [1971]. Formal Semantics and Logic (PDF) . Nousoul Digital Publishers. p. 12.
La metalógica, a su vez, puede dividirse aproximadamente en dos partes: la teoría de la demostración y la semántica formal... La división no es exacta; muchas cuestiones se han tratado desde ambos puntos de vista, y algunos métodos y resultados de la teoría de la demostración son indispensables en semántica.
- ↑ Kaye, Richard (1991). "1. El modelo estándar". Modelos de aritmética de Peano . Oxford: Clarendon Press. pág. 10. ISBN 9780198532132.
Fuentes
- Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic . University of California Press (publicado en 1973). ISBN 9780520023567OCLC 36312727 ( Accesible para usuarios con discapacidades visuales ).
Lecturas adicionales
- Hofstadter, Douglas , 1979. Gödel, Escher, Bach: Una eterna trenza dorada ISBN 978-0-465-02656-2777 páginas.
- Kleene, Stephen C. , 1967. Lógica matemática. Reimpreso por Dover, 2002. ISBN 0-486-42533-9.
- Smullyan, Raymond M. , 1961. Teoría de los sistemas formales: Anales de estudios matemáticos , Princeton University Press (1 de abril de 1961), 156 páginas ISBN 0-691-08047-X.
Enlaces externos
Contenido multimedia relacionado con sistemas formales en Wikimedia Commons- Encyclopædia Britannica, Definición de sistema formal , 2007
- Daniel Richardson, Sistemas formales, lógica y semántica
- Sistema formal en PlanetMath .
- Enciclopedia de Matemáticas, Sistema formal
- Peter Suber, Sistemas y máquinas formales: un isomorfismo
Archivado el 24/05/2011 en Wayback Machine , 917.
- Ray Taol, Sistemas Formales
- ¿Qué es un sistema formal? Archivado el 7 de junio de 2011 en Wayback Machine : algunas citas de "Inteligencia artificial: la idea misma" de John Haugeland (1985), págs. 48-64.
- Siglo IV a. C. en la India
- Metalogic
- Sintaxis (lógica)
- Sistemas formales
- lógica formal
- Lenguajes formales
- Introducciones del primer milenio a. C.
