Modalinės teiginių logikos įrodymų teorija

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. Plačiau apie modalinę teiginių logiką su semantiniais medžiais žr. Fitting & Mendelsohn (1998: 47–65), Priest (2008: 20–63); aksiomatinės sistemos naudojamos Sider (2010); apie sekvencijų skaičiavimą modalinėje teiginių logikoje žr. Fitting (2007: 113–116). Pateikiame aksiomatinę sistemą, kurioje specifikuojame aksiomų schemas ir išvedimo taisykles. Logikos K įrodymų teorija DK yra: Aksiomos (teiginių logika): jei φ yra tautologija teiginių logikoje, tai φ yra aksioma; (aksiomos schema K): □(φ → ψ) → (□φ → □ψ). Išvedimo taisyklės (modus ponens): jei φ ir φ → ψ, tai ψ; (būtinumo įvesties taisyklė): jei ⊢φ, tai ⊢□φ. Svarbu pabrėžti, kad būtinumo įvesties taisyklė nesako, jog jei kažkokia formulė yra teisinga, tai ji būtinai teisinga. Ši išvedimo taisyklė leidžia iš jau išvestos teoremos išvesti tai, kad ji yra būtina. Čia notacija φ1, …, φn ⊢D ψ suprantama kaip ⊢D (φ1 & … & φn) → ψ. Galima įrodyti, kad DK yra adekvati semantiškai apibrėžtai logikai K, t. y. visos DK teoremos yra K-tapačiai teisingos formulės bei visos K-tapačiai teisingos formulės yra DK teoremos. Prie DK galime prijungti papildomas aksiomų schemas ir tada turėsime adekvačias dedukcines sistemas atžvilgiu kitų semantiškai apibrėžtų logikų, kurias įvardinome anksčiau pateiktoje lentelėje (žr. schema nr. 1.). Pavyzdžiui, prie DK prijungę aksiomų schemą □φ→φ gautume aksiomatinę sistemą adekvačią semantiškai apibrėžtai logikai T. Pateikiame lentelę, kurioje nurodome logikos pavadinimą, atitinkamą sąlygą rėmams bei aksiomų schemą, kurią prijungę prie DK gautume aksiomatinę sistemą, adekvačią semantiškai apibrėžtai logikai. Plačiau apie pilnumo ir neprieštaringumo įrodymus šioms logikoms žr. Hughes & Cresswell (1996: 111–121), Fitting (2007: 87–91).