Witness Theory: Notes on λ-calculus and Logic
Táto kniha sa zaoberá matematickou analýzou koncepcie formálneho dôkazu v klasickej logike a je v podstate dlhším cvičením z aplikovaného λ-kalkulu.
Podľa hovorových výrazov siahajúcich až k L. E. J. Brouwerovi sa objekty skúmania v tomto podniku nazývajú svedectvá. Svedok má predstavovať logický dôkaz klasicky platnej formuly v danom dôkazovom kontexte. Formalizmy používané na vyjadrenie svedkov a ich rovnostného správania sú rozšíreniami čisto typizovaného λ-kalkulu, ktoré sa považujú za rovnostné teórie.
Formálne je svedok generovaný z dekorovaných - alebo typovaných - svedeckých premenných, ktoré reprezentujú predpoklady, a svedeckých operátorov, ktoré reprezentujú logické pravidlá odvodzovania.
Rovnicové špecifikácie slúžia na definovanie operátorov svedkov.
Vo všeobecnosti sa to dá urobiť ignorovaním typizácie', t. j. samotných logických formúl.
Modelovo-teoreticky sú svedkovia objektmi extenzionálneho Scottovho λ-modelu.
Tento prístup - nazývaný všeobecne "teória svedkov" - je inšpirovaný prácou N. G. de Bruijna o matematickej teórii dokazovania, ktorá sa uskutočnila na prelome 60. a 70. rokov 20. storočia na univerzite v Eindhovene (Holandsko), a je podobný prístupu, ktorý stojí za Curryho-Howardovou korešpondenciou, známou z intuicionistickej logiky.
V klasickom prípade sú dekorácie - často nazývané typy' - formulkami klasickej logiky.
Na úrovni bez kvantifikátorov je teóriou rovníc λ-kalkulus so surjektívnym párovaním' a niektoré jeho podsystémy, vhodne dekorované.
Rozšírenie na výrokové kvantifikátory prvého a druhého rádu je jednoduché.
Kniha pozostáva zo súboru poznámok a príspevkov napísaných a rozoslaných v priebehu posledných desiatich rokov ako pokračovanie predchádzajúceho výskumu, ktorý autor uskutočnil v osemdesiatych rokoch.
Okrem iného obsahuje prehľad počiatkov modernej teórie dôkazu - od Fregeho po Gentzena - zo svedecko-teoretického hľadiska, ako aj charakteristickú aplikáciu teórie svedkov na praktický logický problém týkajúci sa axiomatickosti.
