Tanúelmélet: Jegyzetek a λ-kalkulusról és a logikáról

Eredeti címe:

Witness Theory: Notes on λ-calculus and Logic

Könyv tartalma:

Ez a könyv a klasszikus logikában a formális bizonyítás fogalmának matematikai elemzésével foglalkozik, és - lényegében - az alkalmazott λ-kalkulus egy hosszabb gyakorlatát rögzíti.

A L. E. J. Brouwerig visszanyúló köznyelvi kifejezéseket követve a vizsgálat tárgyait ebben a vállalkozásban tanúknak nevezzük. Egy tanú egy klasszikusan érvényes formula logikai bizonyítását hivatott reprezentálni egy adott bizonyítási kontextusban. A tanúk és egyenletességük kifejezésére használt formalizmusok a tiszta tipizált λ-kalkulus kiterjesztései, amelyeket egyenletességelméleteknek tekintünk.

Formailag egy tanú kitüntetett - vagy tipizált - tanúváltozókból, amelyek feltételezéseket, és tanúoperátorokból, amelyek logikai következtetési szabályokat képviselnek, generálódik.

Az egyenlőségi specifikációk a tanúoperátorok definiálására szolgálnak.

Általában ez a tipizálás', azaz maguknak a logikai formuláknak a figyelmen kívül hagyásával végezhető el.

Modellelméletileg a tanúk egy extenzionális Scott λ-modell objektumai.

A megközelítés - amelyet általánosságban tanúelméletnek neveznek - N. G. de Bruijn munkájából származik, amelyet a bizonyítás matematikai elméletével kapcsolatban végzett az 1960-as évek végén és az 1970-es évek elején az Eindhoveni Egyetemen (Hollandia), és hasonló az intuitív logikából ismert Curry-Howard-korrespondencia mögött álló megközelítéshez.

A klasszikus esetben a kitüntetések - gyakran típusoknak nevezik őket - klasszikus logikai formulák.

Kvantormentes szinten a szóban forgó egyenletelmélet a λ-kalkulus szürjektív párosítással' és néhány alrendszere, megfelelően dekorálva.

A kiterjesztés az állítmányos, első- és másodrendű kvantorokra egyszerű.

A könyv az elmúlt tíz évben írt és terjesztett jegyzetek és dolgozatok gyűjteménye, a szerző által a nyolcvanas években végzett korábbi kutatások folytatásaként.

Többek között tartalmazza a modern bizonyításelmélet eredetének áttekintését - Frege-től Gentzenig - tanúelméleti szempontból, valamint a tanúelmélet egy jellegzetes alkalmazását egy gyakorlati logikai problémára, az axiomatizálhatóságra vonatkozóan.