Eredeti címe:
Formal Logic: Classical Problems and Proofs
Könyv tartalma:
A logika - vitathatatlanul - a bizonyításról szól, de a bizonyítás "költséges" lehet, gyakran lehetetlenül költséges, és manapság a legtöbbet (részben) automatikus bizonyítókra bízzák, nevezetesen az úgynevezett SAT solverekre, a (Boolean) kielégíthetőségi problémán alapuló szoftverekre, vagy SAT-ra. Ez a (Boole-i) érvényességi probléma (VAL) kettőse, amely Hilbert Entscheidungsproblem-jén és az univerzális Turing-gépen keresztül a digitális számítógép koncepciójának középpontjában áll. Míg ezek a problémák - a VAL lényegesen kevésbé, mint a SAT - szerepelnek az informatikus hallgatóknak szóló bevezető logikai tankönyvekben, addig a matematikai vagy filozófiai hallgatóknak szóló tankönyvekből nagyrészt vagy teljesen hiányoznak.
A Formális logika: Klasszikus problémák és bizonyítások ezt a - véleményünk szerint - helytelen állapotot korrigálja azzal, hogy a formális klasszikus logika alapjait egy olyan formális vagy számítógépes nyelv központi nézőpontjából mutatja be, amely az igazság megőrzésének képessége révén különbözik a többi formális vagy számítógépes nyelvtől, és így potenciálisan megoldást kínál a VAL és/vagy SAT formájában megfogalmazott döntési problémákra. A klasszikus logikának ezt az alapvető aspektusát, az igazság megőrzését három fő formális szemantika, a Tarsk-féle, a Herbrand-féle és az algebrai (Boole-féle) szemantika alapján dolgozzuk ki, amelyek viszont a standard elsőrendű logikára vonatkozó adekvátsági eredményeken keresztül a VAL-hoz és a SAT-hoz kapcsolódó közvetlen és közvetett, illetve cáfoló bizonyítási rendszerek fő bizonyítási rendszereit alapozzák meg.
Ez a könyv nem a klasszikus logika történetére összpontosít, mégis tárgyalja és idézi a logika eredetével és fejlődésével kapcsolatos központi részeket, mégpedig filozófiai szempontból. Mivel nem a matematikai logikáról szóló könyv, a formális logikát alapvetően matematikai szempontból veszi szemügyre. A számítási megközelítés felé hajló, a SAT és a VAL gerincét képező megközelítéssel, ez tehát egy olyan bevezetés a logikába, amely a logika három ágának, nevezetesen a filozófiai, a matematikai és a számítási ágnak a lényeges aspektusait tárgyalja.
