Se utiliza un sistema formal para inferir teoremas a partir de axiomas de acuerdo con un conjunto de reglas. Estas reglas, que se utilizan para realizar la inferencia de teoremas a partir de axiomas, son el cálculo lógico del sistema formal. Un sistema formal es esencialmente un " sistema axiomático ". [1]
En 1921, David Hilbert propuso utilizar dicho sistema como base para el conocimiento en matemáticas . [2] Un sistema formal puede representar un sistema bien definido de pensamiento abstracto .
El término formalismo a veces es sinónimo aproximado para sistema formal , pero también se refiere a un estilo determinado de la notación , por ejemplo, Paul Dirac 's notación bra-ket .
Fondo
Cada sistema formal usa símbolos primitivos (que colectivamente forman un alfabeto ) para construir finitamente un lenguaje formal a partir de un conjunto de axiomas mediante reglas inferenciales de formación .
Por tanto, el sistema consta de fórmulas válidas construidas a través de combinaciones finitas de los símbolos primitivos, combinaciones que se forman a partir de los axiomas de acuerdo con las reglas establecidas. [3]
Más formalmente, esto se puede expresar de la siguiente manera:
- Un conjunto finito de símbolos, conocido como alfabeto, que concatenan fórmulas, de modo que una fórmula es solo una cadena finita de símbolos tomados del alfabeto.
- Una gramática que consta de reglas para formar fórmulas a partir de fórmulas más simples. Se dice que una fórmula está bien formada si puede formarse utilizando las reglas de la gramática formal. A menudo se requiere que exista un procedimiento de decisión para decidir si una fórmula está bien formada.
- Conjunto de axiomas, o esquemas de axiomas , que consta de fórmulas bien formadas.
- Un conjunto de reglas de inferencia . Una fórmula bien formada que se puede inferir de los axiomas se conoce como teorema del sistema formal.
Recursivo
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.
Inferencia y vinculación
La 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 ) consistente con el uso en matemáticas modernas como la teoría de modelos . [ aclaración necesaria ]
Lenguaje formal
Un lenguaje formal es un lenguaje definido por un sistema formal. Al igual que los idiomas en lingüística , los idiomas formales generalmente tienen dos aspectos:
- la sintaxis de un lenguaje es cómo se ve el lenguaje (más formalmente: el conjunto de posibles expresiones que son enunciados válidos en el lenguaje) estudiados en la teoría formal del lenguaje
- la semántica de una lengua es lo que significan las emisiones de la lengua (que se formaliza de varias formas, dependiendo del tipo de lengua en cuestión)
En informática y lingüística, por lo general, solo se considera la sintaxis de un lenguaje formal a través de la noción de gramática formal . Una gramática formal es una descripción precisa de la sintaxis de un lenguaje formal: un conjunto de cadenas . Las dos categorías principales de gramática formal son la de gramáticas generativas , que son conjuntos de reglas sobre cómo se pueden generar cadenas en un idioma, y la de gramáticas analíticas (o gramática reductiva, [4] [5] ), que son conjuntos de reglas. para saber cómo se puede analizar una cadena para determinar si es miembro del idioma. En resumen, una gramática analítica describe cómo reconocer cuando las cadenas son miembros del conjunto, mientras que una gramática generativa describe cómo escribir solo esas cadenas en el conjunto.
En matemáticas , un lenguaje formal generalmente no se describe mediante una gramática formal sino mediante (a) un lenguaje natural, como el inglés. Los sistemas lógicos se definen tanto por un sistema deductivo como por un lenguaje natural. Los sistemas deductivos, a su vez, solo están definidos por el lenguaje natural (ver más abajo).
Sistema deductivo
Un sistema deductivo , también llamado aparato deductivo o lógica , consta de axiomas (o esquemas de axiomas ) y reglas de inferencia que pueden usarse para derivar teoremas del sistema. [6]
Tales sistemas deductivos conservan cualidades deductivas en las fórmulas que se expresan en el sistema. Por lo general, la cualidad que nos preocupa es la verdad en contraposición a la falsedad. Sin embargo, se pueden conservar otras modalidades , como la justificación o la creencia .
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 simplemente una consecuencia sintáctica de las líneas que la preceden. No debe haber ningún elemento de interpretación del lenguaje que se involucre con la naturaleza deductiva del sistema.
Un ejemplo de sistema deductivo es la lógica de predicados de primer orden .
Sistema lógico
Un sistema lógico o lenguaje (que no debe confundirse con el tipo de "lenguaje formal" discutido anteriormente que se describe mediante una gramática formal), es un sistema deductivo (ver sección anterior; más comúnmente lógica de predicados de primer orden ) junto con adicionales (no- axiomas lógicos) y una semántica [ discutido ] . De acuerdo con la interpretación de la teoría de modelos , la semántica de un sistema lógico describe si una fórmula bien formada es satisfecha por una estructura dada. 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. A la inversa, un sistema lógico está completo si cada fórmula bien formada que es satisfecha por cada modelo del sistema lógico puede inferirse de los axiomas.
Un ejemplo de sistema lógico es la aritmética de Peano .
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, los contribuyentes incluyen a George Boole , Augustus De Morgan y Gottlob Frege . La lógica matemática se desarrolló en la Europa del siglo XIX .
Formalismo
El programa de Hilbert
David Hilbert instigó un movimiento formalista que finalmente se vio atenuado por los teoremas de incompletitud de Gödel .
Manifiesto QED
El manifiesto QED representó un esfuerzo posterior, aún sin éxito, de formalización de las matemáticas conocidas.
Ejemplos de
Los ejemplos de sistemas formales incluyen:
- Cálculo lambda
- Cálculo de predicados
- Cálculo proposicional
Variantes
Los siguientes sistemas son variaciones de sistemas formales [ aclaración necesaria ] .
Sistema de prueba
Las pruebas formales son secuencias de fórmulas bien formadas (o wff para abreviar). Para que una wff califique como parte de una prueba, puede ser un axioma o el producto de aplicar una regla de inferencia sobre wffs anteriores en la secuencia de prueba. La última wff de la secuencia se reconoce como teorema .
El punto de vista de que la generación de pruebas formales es todo lo que hay en las matemáticas a menudo se llama formalismo . David Hilbert fundó la metamatemática como una disciplina para discutir sistemas formales. Cualquier lenguaje que se use para hablar de 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 completamente formalizado que el componente de lenguaje formal del sistema formal bajo examen, que luego se llama lenguaje objeto , es decir, el objeto del lenguaje. discusión en cuestión.
Una vez que se da un sistema formal, se puede definir el conjunto de teoremas que se pueden probar dentro del sistema formal. Este conjunto consta de todas las wffs para las que existe una prueba. Por tanto, todos los axiomas se consideran teoremas. A diferencia de la gramática de las wff, no hay garantía de que haya un procedimiento de decisión para decidir si una wff dada es un teorema o no. 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 .
Ver también
|
|
Referencias
- ^ "Sistema formal, ENCYCLOPÆDIA BRITANNICA" .
- ^ "Programa de Hilbert, enciclopedia de filosofía de Stanford" .
- ^ Encyclopædia Britannica,Definición de sistema formal , 2007.
- ^ Gramática reductiva: ( informática ) Un conjunto de reglas sintácticas para el análisis de cadenas para determinar si las cadenas existen en un idioma. "Diccionario de ciencia y tecnología Diccionario McGraw-Hill de términos científicos y técnicos" (6ª ed.). McGraw-Hill.[ fuente no 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 en habilidades, conocimientos e innovación en la publicación científica. [1]
- ^ "Hay dos clases de esquemas de escritura de compiladores de definiciones de lenguaje formal. Elenfoque de gramática productivaes 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. o la técnica de gramática 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 idioma ". " The TREE-META Compiler-Compiler System: A Meta Compiler System for the Univac 1108 and General Electric 645 , University of Utah Technical Report RADC-TR-69-83. C. Stephen Carr, David A. Luther, Sherian Erdmann" ( PDF) . Consultado el 5 de enero de 2015 .
- ^ Hunter, Geoffrey, Metalogic: Una introducción a la metateoría de la lógica estándar de primer orden, University of California Pres, 1971
Otras lecturas
- Raymond M. Smullyan , 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
- Stephen Cole Kleene , 1967. Lógica matemática Reimpreso por Dover, 2002. ISBN 0-486-42533-9
- Douglas Hofstadter , 1979. Gödel, Escher, Bach: An Eternal Golden BraidISBN 978-0-465-02656-2 . 777 páginas.
enlaces externos
Medios relacionados con sistemas formales en Wikimedia Commons- Encyclopædia Britannica, Definición de sistema formal , 2007.
- ¿Qué es un sistema formal? : Algunas citas de "Artificial Intelligence: The Very Idea" de John Haugeland (1985), págs. 48-64.
- Peter Suber, Sistemas formales y máquinas: un isomorfismo , 1997.
Medios relacionados con sistemas formales en Wikimedia Commons