Sistema formal

La versión actual de la página aún no ha sido revisada por colaboradores experimentados y puede diferir significativamente de la versión revisada el 31 de agosto de 2021; las comprobaciones requieren 3 ediciones .

Un sistema formal ( teoría formal , teoría axiomática , axiomática , sistema deductivo ) es el resultado de una estricta formalización de la teoría , que supone una completa abstracción del significado de las palabras del lenguaje utilizado, y de todas las condiciones que rigen el uso de estas palabras en la teoría se expresan explícitamente a través de axiomas y reglas que permiten derivar una frase de otras [1] .

Un sistema formal es una colección de objetos abstractos que no están relacionados con el mundo exterior, en el que las reglas para operar con un conjunto de símbolos se presentan en una interpretación estrictamente sintáctica sin tener en cuenta el contenido semántico, es decir, la semántica. Los sistemas formales estrictamente descritos aparecieron después de que se planteó el problema de Hilbert . El primer FS apareció después de la publicación de los libros de Russell y Whitehead "Formal Systems".[ especificar ] . Estos FS se presentaron con ciertos requisitos.

Fundamentos

Una teoría formal se considera definida si [2] :

1. Se da un conjunto finito o numerable de símbolos arbitrarios. Las secuencias finitas de símbolos se denominan expresiones teóricas .
2. Hay un subconjunto de expresiones llamadas fórmulas .
3. Se ha destacado un subconjunto de fórmulas, llamado axiomas .
4. Hay un conjunto finito de relaciones entre fórmulas, llamadas reglas de inferencia .

Por lo general, existe un procedimiento eficiente que permite que una expresión dada determine si es una fórmula. A menudo, un conjunto de fórmulas viene dado por una definición inductiva . Por regla general, este conjunto es infinito. El conjunto de símbolos y el conjunto de fórmulas definen colectivamente el lenguaje o firma de una teoría formal.

Muy a menudo, es posible averiguar con eficacia si una fórmula dada es un axioma; en tal caso, se dice que la teoría está efectivamente axiomatizada o axiomática . El conjunto de axiomas puede ser finito o infinito. Si el número de axiomas es finito, se dice que la teoría es finitamente axiomatizable . Si el conjunto de axiomas es infinito, entonces, como regla, se especifica utilizando un número finito de esquemas de axiomas y las reglas para generar axiomas específicos a partir del esquema de axiomas. Por lo general, los axiomas se dividen en dos tipos: axiomas lógicos (comunes para toda una clase de teorías formales) y axiomas no lógicos o propios (que determinan los detalles y el contenido de una teoría en particular).

Para cada regla de inferencia R y para cada fórmula A , la cuestión de si el conjunto de fórmulas elegido está en relación con R con la fórmula A está efectivamente resuelta , y si es así, entonces A se llama una consecuencia directa de estas fórmulas de acuerdo con el gobernante.

Una derivación es cualquier secuencia de fórmulas tal que cualquier fórmula de la secuencia sea un axioma o una consecuencia directa de algunas fórmulas previas de acuerdo con una de las reglas de derivación.

Una fórmula se llama teorema si hay una derivación en la que esta fórmula es la última.

Una teoría para la cual existe un algoritmo eficiente que permite averiguar a partir de una fórmula dada si existe su derivación se denomina decidible ; de lo contrario, se dice que la teoría es indecidible .

Se dice que una teoría en la que no todas las fórmulas son teoremas es absolutamente consistente .

Definición y variedades

Una teoría deductiva se considera dada si:

1. Se dan un alfabeto ( conjunto ) y reglas para la formación de expresiones ( palabras ) en este alfabeto.
2. Se dan las reglas para la formación de fórmulas (expresiones bien formadas y correctas).
3. Del conjunto de fórmulas, se selecciona de alguna forma un subconjunto T de teoremas ( fórmulas demostrables ).

Variedades de teorías deductivas

Dependiendo del método de construcción de un conjunto de teoremas:

Especificación de axiomas y reglas de inferencia

En el conjunto de fórmulas, se destaca un subconjunto de axiomas y se especifica un número finito de reglas de inferencia, reglas con la ayuda de las cuales (y solo con la ayuda de ellas) se pueden formar nuevos teoremas a partir de axiomas y derivados previamente. teoremas Todos los axiomas también están incluidos en el número de teoremas. A veces (por ejemplo, en la axiomática de Peano ), una teoría contiene un número infinito de axiomas que se especifican utilizando uno o más esquemas de axiomas . Los axiomas a veces se denominan "definiciones ocultas". De esta manera, se especifica una teoría formal ( teoría axiomática formal , cálculo (lógico) formal ).

Preguntando solo axiomas

Solo se dan axiomas, las reglas de inferencia se consideran bien conocidas.

Con tal especificación de teoremas, se dice que se da una teoría axiomática semiformal . Ejemplos

Geometría

Especificando reglas de inferencia solamente

No hay axiomas (el conjunto de axiomas está vacío), solo se dan reglas de inferencia.

De hecho, la teoría así definida es un caso especial de la formal, pero tiene su propio nombre: la teoría de la inferencia natural .

Propiedades de las teorías deductivas

Consistencia

Una teoría en la que el conjunto de teoremas cubre todo el conjunto de fórmulas (todas las fórmulas son teoremas, "enunciados verdaderos") se denomina inconsistente . De lo contrario, se dice que la teoría es consistente . La elucidación de la inconsistencia de una teoría es una de las tareas más importantes y, a veces, más difíciles de la lógica formal.

Integridad

Una teoría se llama completa si en ella para cualquier oración (fórmula cerrada) ya sea ella misma o su negación es derivable . En caso contrario, la teoría contiene enunciados indemostrables (enunciados que no pueden ser ni probados ni refutados por medio de la propia teoría), y se denomina incompletos .

Independencia de los axiomas

Se dice que un axioma individual de una teoría es independiente si ese axioma no se puede deducir del resto de los axiomas. El axioma dependiente es esencialmente redundante y su eliminación del sistema de axiomas no afectará a la teoría de ninguna manera. Todo el sistema de axiomas de una teoría se llama independiente si cada axioma en él es independiente.

Resolubilidad

Una teoría se llama decidible si en ella es efectivo el concepto de un teorema , es decir, existe un proceso efectivo (algoritmo) que permite que cualquier fórmula determine en un número finito de pasos si es un teorema o no.

Resultados clave

• En los años 30. En el siglo XX, Kurt Gödel demostró que existe toda una clase de teorías de primer orden que están incompletas. Además, la fórmula que establece la consistencia de una teoría tampoco es derivable por medio de la teoría misma (ver los teoremas de incompletitud de Gödel ). Esta conclusión fue de gran importancia para las matemáticas, ya que la aritmética formal (y cualquier teoría que la contenga como una subteoría) es precisamente una teoría de primer orden y, por lo tanto, incompleta.
• A pesar de esto, la teoría de campos cerrados reales con suma, multiplicación y relación de orden es completa ( el teorema de Tarski-Seidenberg ).
• Alonzo Church demostró que el problema de determinar la validez de cualquier fórmula lógica arbitraria de predicados es algorítmicamente irresoluble .
• El cálculo proposicional es una teoría consistente, completa y decidible.

Véase también

• Autoformalización
• teoría de conjuntos
• lógica formal
• Formalismo (matemáticas)
• Sistema de codificación
• Axiomática de la termodinámica

Ejemplos de sistemas formales

• calculo proposicional
• Teorías de primer orden (lógica de primer orden)
  • aritmética formal
  • Teoría axiomática de conjuntos
  • teoría de grupos
• Teorías de orden superior (lógica de orden superior)
• cálculo lambda
  • Cálculo lambda con tipos
  • Cálculo de la construcción
  • Cálculo de construcciones inductivas

Notas

1. ↑ Kleene S.K. Introducción a las Metamatemáticas . - M. : IL, 1957. - S. 59-60. Archivado el 1 de mayo de 2013 en Wayback Machine .
2. ↑ Mendelssohn E. Introducción a la lógica matemática . - M .: "Nauka", 1971. - Pág. 36. Copia de archivo fechada el 1 de mayo de 2013 en la Wayback Machine

Literatura

• Galiev Sh. I. Lógica matemática y teoría de algoritmos. - Kazan: Editorial de KSTU nombrada después. A. N. Tupolev. 2002.
• Kleene S. K. Introducción a las Metamatemáticas . - M. : IL, 1957. - 526 p.
• Kleene S. K. Lógica matemática . - M. : "Mir", 1973. - 480 p.
• Mendelsohn E. Introducción a la Lógica Matemática . - M. : "Nauka", 1971. - 320 p.
• Novikov F. A. Matemáticas discretas para programadores. - San Petersburgo: Peter, 2000. - 304 p.: il. ISBN 5-272-00183-4 .
• Yanovskaya S. A. De la historia de la axiomática // Investigación histórica y matemática . - M. : GITTL, 1958. - Nº 11 . - S. 63-96 .

diccionarios y enciclopedias	gran ruso Britannica (en línea) Britannica (en línea)

Lógicas
Filosofía • Semántica • Sintaxis • Historia
Grupos lógicos	lógica clásica lógica aristotélica Lógica proposicional Lógica de primer orden Lógica de segundo orden lógica de orden superior lógica matemática teoría de conjuntos Teoría del modelo teoría de la computabilidad Teoría de la prueba y matemáticas constructivas lógica lineal sistema formal conclusión natural cálculo de secuencias Álgebra de la lógica Lógica relevante lógica deóntica lógica intuicionista cálculo de Lambek Lógica no clásica intuicionismo lógica difusa Lógica subestructural lógica Descripción lógica Lógica multivaluada Síntesis lógica Lógica vinculante Lógica temporal Lógica modal ( Lógica híbrida ) lógica epistémica lógica filosófica Pensamiento crítico lógica informal razonamiento deductivo
Componentes	Abducción (lógica) Probabilidad declaración Deducción / Inducción / Traducción La realidad razonamiento inductivo inferencia constante booleana Verdadero seguimiento lógico Forma lógica Condiciones necesarias y suficientes Descripción Definición Sustitución Paquete Controversia ( Antinomia ) Juicio sintético / Juicio analítico Enlace
Lista de símbolos booleanos