Decidibilitat

En metalògica, la decidibilitat és una propietat dels sistemes formals quan, per a qualsevulla fórmula en el llenguatge del sistema, existeix un mètode efectiu per determinar si aquesta fórmula pertany o no al conjunt de les veritats del sistema. Per exemple, la lògica proposicional és decidible, perquè existeix un algoritme (taula de veritat) que en un nombre finit de passos pot decidir si la fórmula és vàlida o no.

Quan una fórmula no pot ser provada vertadera ni falsa, es diu que la fórmula és independent, i que per tant el sistema és no decidible. L'única manera d'incorporar una fórmula independent a les veritats del sistema és postulant-la com a axioma. Dos exemples molt importants de fórmules independents són l'axioma de l'elecció en la teoria de conjunts, i el cinquè postulat d'Euclides.

Decidibilitat sintàctica

Un sistema formal és decidible sintàcticament si el conjunt de totes les fórmules vàlides en el sistema és decidible. És a dir, existeix un algoritme tal que per a cada fórmula del sistema és capaç de decidir en un nombre finit de passos i la fórmula és vàlida o no en el sistema.

La lògica de primer ordre és sintàcticament decidible si es limita a predicats amb un sol argument (monàdica). Si s'inclouen predicats amb dos o més arguments, no és decidible.

Tota teoria completa i recursivament enumerable és decidible sintàcticament. D'altra banda, tota teoria que inclogui aritmètica bàsica no és decidible sintàcticament.