Un sistema formal o axiomàtic és un artifici matemàtic compost de símbols que s'uneixen entre si formant cadenes que, al seu torn, poden ser manipulades segons regles per produir altres cadenes. D'aquesta manera, el sistema formal és capaç de representar cert aspecte de la realitat. El terme «formalisme» s'utilitza, de vegades, com a sinònim de sistema formal, per a un determinat propòsit. Un sistema formal matemàtic consisteix en el següent:

1. Un conjunt finit de símbols que poden ser usats per a la construcció de fórmules.
2. Una gramàtica, és a dir, un mecanisme per a la construcció de fórmules ben formades (WFF). També s'ha de proporcionar un algorisme de decisió per conèixer si una determinada fórmula és ben formada o no.
3. Un conjunt d'axiomes que han de ser fórmules WFF.
4. Un conjunt de regles d'inferència.
5. Un conjunt de teoremes. Aquest conjunt inclou tots els axiomes, més totes les WFF que poden ser derivades dels axiomes o d'altres teoremes per mitjà de les regles d'inferència. La gramàtica no necessàriament garanteix la decidibilitat de si una fórmula és teorema o no.

En les ciències formals de la lògica i les matemàtiques, així com en altres disciplines relacionades, com són la informàtica, la teoria de la informació, i l'estadística, un sistema formal és una gramàtica formal usada per a la modelització de diferents propòsits. S'anomena formalització l'acte de crear un sistema formal, i es tracta d'una acció amb la qual pretenem capturar i abstreure l'essència de determinades característiques del món real, en un model conceptual expressat en un determinat llenguatge formal.

En matemàtiques, les proves formals són el resultat de sistemes formals, consistents en axiomes i regles de deducció. Els teoremes poden ser obtinguts per mitjà de proves formals. Aquest punt de vista de les matemàtiques ha estat anomenat formalista, encara que moltes vegades aquest terme comporta una accepció pejorativa. En aquest sentit, David Hilbert va crear la disciplina anomenada metamatemàtica, dedicada a l'estudi dels sistemes formals, entenent que el llenguatge utilitzat per a això, anomenat metallenguatge, era diferent del llenguatge del sistema formal que es pretenia estudiar. Amb una altra denominació, el metallenguatge o llenguatge obtingut mitjançant la gramàtica formal es diu també, a vegades, llenguatge objecte.

Un sistema així és la reducció d'un llenguatge formalitzat a mers símbols, llenguatge formalitzat i simbolitzat sense cap contingut material; un llenguatge reduït a mera forma que s'expressa mitjançant fórmules que reflecteixen les relacions sintàctiques entre els símbols i les regles de formació i transformació que permeten construir les fórmules del sistema i passar d'una fórmula a una altra.

L'objectiu d'un sistema formal és assenyalar com a vàlides determinades cadenes. Aquestes cadenes vàlides es denominen teoremes. Per a obtenir els teoremes, es fan servir les regles de producció que converteixen una cadena en una altra. Hi ha certs teoremes inicials que no s'obtenen de cap regla, aquests són els axiomes que se suposen vàlids per definició i es converteixen en el germen de producció de teoremes.

El problema de la decisió consisteix a saber si una cadena qualsevol és un teorema. L'algorisme que proporciona una resposta a la pregunta de si la cadena és o no un teorema es denomina procediment de decisió. En alemany, Entscheidungsproblem.

• Coherència: el sistema formal és coherent si cada teorema, en ser interpretat, no correspon a una decisió veritable.
• Completesa: el sistema formal és complet si cada proposició vertadera pot ser representada mitjançant un teorema. És incomplet si alguna veritat no pot expressar-se.
• Decidibilitat: un sistema formal és decidible si existeix un algorisme que digui en temps finit si una cadena qualsevol és un teorema o no ho és.

La matemàtica va ser considerada per David Hilbert un sistema formal, ja que tota la matemàtica es pot interpretar a base de símbols, axiomes i regles de producció. Però, el 1931, Kurt Gödel va demostrar que la coherència i la completesa no podien ser certs a la vegada en les matemàtiques, o almenys en els nombres enters. És el que s'anomena el teorema d'incompletesa de Gödel. D'altra banda, Alonzo Church va demostrar que la matemàtica tampoc podia ser decidible, de manera que la idea de les matemàtiques com a sistema formal, tal com Hilbert pretenia, resulta enderrocada.

El sistema de Peano és un sistema d'axiomes a partir del qual es pot deduir tota l'aritmètica dels nombres naturals. Els primitius d'aquest sistema són els termes "0" (zero), "nombre" i "successor", dels quals, per ser primitius, no es dona cap definició. No obstant això, s'entén per "0" aquest nombre, el terme "nombre" designa els nombres naturals 0, 1, 2, 3... exclusivament, i amb "successor" d'un nombre natural n el nombre natural immediat següent de n en l'ordre natural. El sistema de Peano conté els 5 axiomes que segueixen:

• P1: 0 és un nombre.
• P2: el successor d'un nombre és sempre un nombre.
• P3: dos nombres distints mai tenen el mateix successor.
• P4: 0 no és el successor de cap nombre.
• P5: si P és una propietat tal que (a) zero té la propietat P, i (b) sempre que un nombre n tingui la propietat P, el successor de n també tindrà la propietat P, llavors tots els nombres tindran la propietat P.

L'últim axioma comporta el principi d'inducció matemàtica i il·lustra clarament l'abast d'una "veritat" matemàtica per convenció. Es construeix l'aritmètica fonamental sobre aquesta base, definint els diversos nombres naturals com el successor de zero (0 '), el successor del successor de zero (0 ), i així fins a l'infinit.

Després, s'estableix la definició de suma, que expressa que l'addició d'un nombre natural a un altre donat pot considerar-se com la suma repetida d'1; aquesta última operació és fàcilment expressable per mitjà de la relació de successor:

(a) n + 0 = n ; (b) n + k '= ( n + k)'

Passant ara a la multiplicació dels nombres naturals, se la pot definir per mitjà de la següent definició per recurrència, que expressa de manera rigorosa que el producte nk de dos nombres naturals pot ser considerat com la suma de k termes, cada un dels quals és igual a n, en altres termes:

(a) n . 0 = 0; (b) n . k '= n . k+ n

• Lògica matemàtica.