Sistema formal

En lògica, un llenguatge formal que, a més de símbols i fórmules, consta de procediments deductius, convertint-se, per aquesta raó, en un càlcul lògic. Com a llenguatge deductiu ha de definir els símbols bàsics o primitius de què disposa, les regles (sintàctiques) de formació de fórmules i les de transformació de fórmules, o regles d'inferència. Els mètodes de deducció poden basar-se en axiomes, en axiomes i regles d'inferència (sistemes axiomàtics) o només en regles d'inferència (sistemes de deducció natural, per exemple).

Els sistemes formals han de gaudir de determinades propietats, o atributs, per a ser adequats: han de ser capaços d'expressar tot allò que els importa expressar (els seus teoremes) i, com a deductius, han de ser capaços de demostrar quins de les seves expressions són fórmules vàlides i si només aquestes ho són. Per tant, han de gaudir de consistència, compatibilitat o no-contradicció, de manera que tota fórmula que pugui demostrar-se sigui també veritable (i si és deduïble sense premisses, ha de ser una veritat universalment veritable), la qual cosa implica, al seu torn, que del sistema formal no pugui derivar-se una fórmula A i la seva contrària ¬A. Ha de gaudir també de completesa, de manera que tota fórmula veritable en el sistema pugui ser també demostrada (i si és universalment vàlida ha de ser un teorema del sistema).

La lògica elemental, segons va demostrar Gödel en 1930, és un sistema formal deductiu que gaudeix d'ambdues propietats.

A més d'aquestes dues característiques formals necessàries, un sistema formal axiomàtic, ha de mostrar independència d'axiomes, això és, el conjunt d'axiomes o principis del sistema no ha de ser redundant, i, a més, tot sistema formal pot gaudir, o no, de decidibilitat.