Una tupla especificada con precisión que consiste en un lenguaje formal (símbolos y reglas de formación), un conjunto de axiomas o esquemas de axiomas y reglas de inferencia que determinan cómo se pueden derivar las fórmulas; se usa para generar y manipular expresiones formales de manera independiente de cualquier interpretación pretendida.

Principio

Separación de sintaxis y semántica: especificar reglas de formación y derivación finitas y verificables de modo que las nociones de prueba y derivabilidad sean puramente sintácticas, posibilitando la verificación mecánica y el estudio metateórico de consistencia, completitud y decidibilidad.

Demostración

La aritmética de Peano presentada como sistema formal: un lenguaje con la constante 0 y el sucesor S, axiomas (cero no es sucesor, esquema de inducción como esquema de axiomas) y reglas como modus ponens y generalización que generan los teoremas de la teoría únicamente por derivación sintáctica.

Aplicación incorrecta

Confundir el sistema formal con sus interpretaciones semánticas (tratar la derivabilidad como idéntica a la verdad en todos los modelos), o introducir reglas semánticas informales en las reglas de prueba formales, socava la claridad sobre lo que se demuestra dentro del sistema frente a lo que vale en las estructuras pretendidas.

Consecuencia

Los sistemas formales hacen las pruebas y derivaciones explícitas y verificables, permitiendo el análisis riguroso de la demostrabilidad, la mecanización (asistentes de prueba) y resultados metateóricos como los teoremas de incompletitud de Gödel, que dependen de la forma sintáctica precisa del sistema.

Inversión

La perspectiva inversa enfatiza la práctica matemática informal y el argumento semántico sobre la derivación formal: la argumentación informal o las afirmaciones de verdad modelo-teóricas pueden guiar las matemáticas pero carecen de la certificabilidad mecánica de un sistema formal hasta que se formalizan.

Límite

Un sistema formal es puramente sintáctico y no proporciona significado por sí mismo; la semántica (modelos, interpretaciones) está fuera del sistema. Excluye el razonamiento matemático informal, la justificación empírica y cualquier contenido semántico implícito a menos que se añada explícitamente como axiomas o reglas.

Tensión semántica

Existe tensión entre la demostrabilidad sintáctica (lo que el sistema formal puede derivar) y la verdad semántica (lo que se cumple en los modelos pretendidos o en todos los modelos): los teoremas de completitud, corrección y decidibilidad articulan esta tensión y muestran límites de la formalización.

Síntesis

Un Sistema Formal es una máquina sintáctica deliberadamente restringida: un lenguaje, axiomas y reglas de inferencia que producen pruebas formales; esta separación permite la verificación mecánica, el análisis metamatemático y enunciados precisos sobre lo que es demostrable frente a lo que es verdadero en determinadas interpretaciones.