Bizonyíthatóság

Bizonyíthatóság (provability) az elméleti logikában annak a tulajdonsága, hogy egy mondat véges bizonyítással előállítható egy adott axiomatikus rendszerben. A leggyakoribb példák közé tartozik a Peano-aritmetika (PA) vagy a ZFC. Egy mondat akkor bizonyítható, ha létezik egy formális bizonyítási sor, amely az axiómákból és az inferenciákból levezeti φ-t. A bizonyíthatóságot gyakran jelöljük Pr_T(⌜φ⌝)-val: φ bizonyítható T-ben.

A bizonyíthatóság formalizálása aritmetizálható: a Gödel-féle számkódolás révén belülről beszélhetünk a bizonyításokról. Ennek köszönhetően a rendszer belseje megfogalmazhatja: ha T bizonyítja φ-t, akkor T bizonyíthatja Pr_T(⌜φ⌝). Ezt a Hilbert–Bernays derivability feltételeknek nevezik. A bizonyíthatóság fogalma tehát a rendszertől függ, és különböző rendszerekhez különböző Pr_T-k tartoznak.

Gödel-féle eredmények megvilágítják a bizonyíthatóság korlátait: ha T konszisztens és elegendően kifejező, léteznek olyan φ-k, amelyek a szemantikailag igazak, de T-ben nincsenek bizonyítva (Gödel első incompleteness-tétel). Emellett a második incompleteness-tétel kimondja, hogy T nem állíthatja saját konzisztenciáját, ha az konszisztens. Löb-tétel összefüggéseket ad a belső provability és a mondatok igazságtartalma között.

A bizonyíthatóság megkülönböztethető az igazságtól: bizonyíthatónak lenni nem feltétlenül jelenti a szemantikailag igaz állítást, és fordítva. A tudományos gyakorlatban a bizonyíthatóság alapvető szerepet játszik a formális verifikációban, az automatikus tételbizonyításban, valamint az alapvető matematikai és számítástudományi kérdések logikai vizsgálatában.