Įrodymų teorija

Įrodymų teorija – tai matematinės logikos šaka nagrinėjanti įrodymų formalias savybes. Esama įvairių būdų kaip galima pateikti įrodymų teoriją loginei kalbai L – semantinių medžių, aksiomatinės sistemos, sekvencijų skaičiavimas ir t. t.

Deduktyvioje sistemoje D ψ išvedimą iš prielaidų φ1,…, φn žymėsime φ1, …, φn ⊢D ψ. φ1, …, φn ⊢D ψ reiškia, kad esama sakinio ψ įrodymo iš prielaidų φ1, …, φn. Jei sistemoje D galime įrodyti formulę ψ nesiremdami jokiomis prielaidomis, tai sakysime, kad ψ yra teorema ir žymėsime ⊢D ψ. Tam, kad deduktyvi sistema D „būtų adekvati semantiškai apibrėžtai logikai L“, D turi atitikti du kriterijus: ji turi būti neprieštaringa ir pilna atžvilgiu L. (neprieštaringumas): D yra neprieštaringa atžvilgiu L, jei ir tik jei φ1, …, φn ⊢D ψ ⇒ φ1, …, φn ⊨L ψ; (pilnumas): D yra pilna atžvilgiu L, jei ir tik jei φ1, …, φn ⊨L ψ ⇒ φ1, …, φn ⊢D ψ. Kitaip sakant, D adekvati semantiškai apibrėžtai logikai L, jei ir tik jei tai, kas išvedama sistemoje D, sutampa su tuo, kas logiškai seka logikoje L.

Pabrėžiame, kad yra įvairių būdų pateikti įrodymų teoriją semantiškai apibrėžtai logikai L – semantinių medžių, aksiomatinės sistemos, sekvencijų skaičiavimas ir t. t.


Susijusios sąvokos: