Sistema formal

Este artículo se basa excesivamente en referencias a fuentes terciarias . Por favor, mejora este artículo añadiendo fuentes primarias o secundarias . Buscar fuentes:  «Sistema formal» – noticias  · periódicos  · libros  · académico  · JSTOR ( diciembre de 2024 ) ( Aprende cómo y cuándo eliminar este mensaje )

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] [ se necesita una fuente no terciaria ] [2]}

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

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 .

Un sistema formal tiene lo siguiente: ^{[4] [5] [6]}

• Lenguaje formal , que es un conjunto de fórmulas bien formadas , que son cadenas de símbolos de un alfabeto , formadas por una gramática formal (formada por 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.

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.

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:

• La sintaxis es el aspecto que tiene el lenguaje (más formalmente: el conjunto de expresiones posibles que son enunciados válidos en el lenguaje).
• La semántica es lo que significan los enunciados 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 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 ^{[7] [¿ fuente poco confiable? ] [8]} ), que son conjuntos de reglas sobre cómo se puede analizar una cadena para determinar si es un miembro del lenguaje.

Es posible que sea necesario limpiar esta sección para cumplir con los estándares de calidad de Wikipedia . El problema específico es: Esta sección necesita una mejor organización y más citas. Por favor, ayude a mejorar esta sección si puede. ( Octubre de 2023 ) ( Aprenda cómo y cuándo eliminar este mensaje )

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

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. ^{[9] [10]}

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 .

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:

• Sonido , si cada fórmula bien formada que puede inferirse de los axiomas es satisfecha por cada modelo del sistema lógico.
• Semánticamente 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 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. ^[11] También existen modelos no estándar de la aritmética .

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 . ^[3] El manifiesto QED representó un esfuerzo posterior, aún infructuoso, de formalización de las matemáticas conocidas.

• Lista de sistemas formales
• Método formal  – Especificaciones de programas matemáticosPáginas que muestran descripciones breves de los objetivos de redireccionamiento
• 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érminoPáginas que muestran descripciones breves de los objetivos de redireccionamiento
• Instancia de sustitución  – Concepto en lógicaPáginas que muestran descripciones breves de los objetivos de redireccionamiento
• Teoría (lógica matemática)  – Conjunto de oraciones en un lenguaje formal

• Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic [Metalógica: Introducción a la metateoría de la lógica estándar de primer orden ]. University of California Press (publicado en 1973). ISBN 9780520023567.OCLC 36312727  .(accesible para usuarios con discapacidades de lectura)

• Hofstadter, Douglas , 1979. Gödel, Escher, Bach: Una eterna trenza dorada ISBN 978-0-465-02656-2 . 777 páginas. 
• Kleene, Stephen C. , 1967. Lógica matemática Reimpreso por Dover, 2002. ISBN 0-486-42533-9 
• Smullyan, Raymond M. , 1961. Theory of Formal Systems: Annals of Mathematics Studies , Princeton University Press (1 de abril de 1961) 156 páginas ISBN 0-691-08047-X 

Busque formalización en Wikcionario, el diccionario libre.

• Medios relacionados con Sistemas formales en Wikimedia Commons
• Enciclopedia Británica, Definición del 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 formales y máquinas: un isomorfismo Archivado el 24 de mayo de 2011 en Wayback Machine , 1997.
• Ray Taol, Sistemas Formales
• ¿Qué es un sistema formal?: Algunas citas de 'Inteligencia artificial: la idea misma' (1985), de John Haugeland, págs. 48-64.