bizonyíthatóságát

Bizonyíthatóság (bizonyíthatóságát) a formális logikában annak a tulajdonsága, hogy egy állítás levezethető-e az adott axiómákból és következtetési szabályokból. Ha létezik olyan formális bizonyítás, amely az állítást a rendszer nyelvén megfogalmazott axiómákból levezeti, akkor az állítást bizonyíthatónak mondjuk. Fontos azonban megkülönböztetni a bizonyíthatóságot az igazságtól: egy állítás lehet igaz egy modellben, de a használt formális rendszerben nem bizonyítható.

Formális rendszerekben az állítások levezetése axiómákból és szabályokból történik. A bizonyítás véges lépésekből álló szekvenciát jelent. A bizonyítható állítások halmazát gyakran rekurzívan felsorolhatónak írják le: van egy algoritmus, amely megadja az összes bizonyítást, és ezek közül kiválogatható a vizsgált tétel.

Gödel 1931-es tételei szerint egy konzisztens, hatékonyan axiomatizált elmélet, amely elég számelméletet ír le, olyan igaz állításokat tartalmaz, amelyeket nem lehet bebizonyítani benne. A második tétel pedig kimondja, hogy az ilyen elmélet nem tudja bebizonyítani saját konzisztenciáját, feltéve hogy az konzisztens.

Az úgynevezett provability logika a □ operátort használja, amely kifejezi, hogy egy állítás bizonyítható-e a rendszerben. Ez a terület a modal logikából fejlődött ki, és összefügg a Löb-tétellel és a formális verifikációval. A bizonyíthatóság elvei fontosak a számítástechnikában is, például automatikus bizonyításban, bizonyítási rendszerekben és a szoftver- és hardver-verifikációban.