Kalkulusok a konstruktív logikában

Abstract

Ebben a dolgozatban az alapvető célkitűzésem az volt, hogy áttekintéssel szolgáljak az intuicionista logikában használatos kalkulusokról, és egyáltalán az intuicionista logikáról. Közel sem törekedtem a teljességre; inkább azt tartottam szem előtt, hogy a konstruktivizmus egy-egy oldalát felvázolva kiindulópontot nyújtsak egy részletesebb vizsgálódás számára. Alapvetően három különböző kalkulust tárgyalok, amelyek alkalmasak az intuicionista szemléletű következtetések szintaktikai reprezentációjára: Heyting predikátumkalkulusát, az intuicionista szekvent kalkulust, és az intuicionista tábla módszert. Az első kettő ekvivalenciáját részletesen bebizonyítom, az utóbbi esetében pedig azt a szemantikát is ismertetem, melyre nézve a tábla módszer helyességi és teljességi bizonyítását nagyvonalakban prezentálom. Ezenkívül a tábla módszer kapcsán kitérek arra a kérdésre is, hogy miként lehet egy megadott formula intuisztikus érvényességét a gyakorlatban bizonyítani, és a kapott eredményeket a dolgozatomhoz mellékelt programban – igaz, csak nulladrendben – interpretálom is.