¿Qué es?
No se ha añadido ninguna twiki todavía.
En lógica, un lenguaje formal que, además de símbolos y fórmulas, consta de procedimientos deductivos, convirtiéndose, por lo mismo, en un cálculo lógico. Como lenguaje deductivo ha de definir los símbolos básicos o primitivos de que dispone, las reglas (sintácticas) de formación de fórmulas y las de transformación de fórmulas, o reglas de inferencia. Los métodos de deducción pueden basarse en axiomas, en axiomas y reglas de inferencia (sistemas axiomáticos) o sólo en reglas de inferencia (sistemas de deducción natural, por ejemplo).
Los sistemas formales deben gozar de determinadas propiedades, o atributos, para ser adecuados: han de ser capaces de expresar todo aquello que les importa expresar (sus teoremas) y, como deductivos, han de ser capaces de demostrar cuáles de sus expresiones son fórmulas válidas y si sólo éstas lo son. Por tanto, han de gozar de consistencia, compatibilidad o no-contradicción, de modo que toda fórmula que pueda demostrarse sea también verdadera (y si es deducible sin premisas, ha de ser una verdad universalmente verdadera), lo que implica, a su vez, que del sistema formal no pueda derivarse una fórmula A y su contraria ¬A. Ha de gozar también de completud, de modo que toda fórmula verdadera en el sistema pueda ser también demostrada (y si es universalmente válida ha de ser un teorema del sistema).
La lógica elemental, según demostró Gödel en 1930, es un sistema formal deductivo que goza de ambas propiedades.
Además de estas dos características formales necesarias, un sistema formal axiomático, ha de mostrar independencia de axiomas, esto es, el conjunto de axiomas o principios del sistema no ha de ser redundante, y, además, todo sistema formal puede gozar, o no, de decidibilidad.
Relaciones geográficas