formálislogikai

A formális logika a logika egyik fő ága, amely a nyelvek, kifejezések és érvelések formális megadására, a levezetés szabályainak kidolgozására és a helyesség viszonyainak tisztázására törekszik. A hangsúly a szintaktikán és a szemantikán van: szigorúan definiált szimbólumokból felépített formulákat vizsgál, és meghatározza, hogy mely állítások érvényesek vagy levezethetők bizonyos bizonyítási rendszerekben.

Alapvető fogalmai közé tartozik a formálisan leírt nyelv szintaxisa (formulák, kötőjelek, kvantorok), a szemantika (értelmezések, modellek és igazságértékek), valamint a bizonyítási rendszerek (axiomák és szabályok). A formális logikában kiemelkedő a következtetés formális gyakorlata: egy állítást a meglévő axiomákból és szabályokból lehet igazolni vagy cáfolni.

Historikus jellegzetességek szerint a formális logika gyökerei Frege-ra és a klasszikus kalkulusokra vezethetők vissza; a 20. században Hilbert-féle axiomatikus megközelítések, Gentzen-féle szekvencia-kalkulus és Tarski szemantikája alakították ki a modern területet. A teljesességi tétel kimondja, hogy a first-order logikában minden szemantikailag igaz formula levezethető; a hangság pedig azt garantálja, hogy minden levezetés igaz. Gödel 1931-es nem-teljesességi tétele pedig megmutatja, hogy elegendően erős aritmetikában nem létezik teljes, konzisztens formális rendszer.

Alkalmazások közé tartozik a formális verifikáció, az automatikus bizonyítás és a matematikai, számítástechnikai és nyelvészeti kutatások támogatása. A proposicionális logika decidabilis, az elsőrendű logika általánosan nem decidabilis.