Witness Theory: Notes on λ-calculus and Logic
Książka ta zajmuje się matematyczną analizą pojęcia dowodu formalnego w logice klasycznej i stanowi - w istocie - dłuższe ćwiczenie z zakresu λ-kalkulusa stosowanego.
Zgodnie z kolokwializmami sięgającymi L.E.J. Brouwera, obiekty badań w tym przedsięwzięciu nazywane są świadkami. Świadek ma reprezentować logiczny dowód klasycznie poprawnej formuły w danym kontekście dowodowym. Formalizmy używane do wyrażania świadków i ich zachowań równościowych są rozszerzeniami czystego typowanego λ-kalkulusa, traktowanego jako teorie równościowe.
Formalnie rzecz biorąc, świadek jest generowany z dekorowanych - lub typowanych - zmiennych świadka, reprezentujących założenia, oraz operatorów świadka, reprezentujących logiczne reguły wnioskowania.
Specyfikacje równościowe służą do definiowania operatorów świadków.
Ogólnie rzecz biorąc, można to zrobić, ignorując typowanie, tj. same formuły logiczne.
Teoretycznie, świadkowie są obiektami ekstensjonalnego modelu Scotta λ.
Podejście to - zwane ogólnie teorią świadków - jest inspirowane pracą N. G. de Bruijna nad matematyczną teorią dowodzenia, wykonaną na przełomie lat 60. i 70. na Uniwersytecie w Eindhoven (Holandia), i jest podobne do podejścia stojącego za korespondencją Curry-Howard, znaną z logiki intuicjonistycznej.
W przypadku klasycznym, dekoracje - często nazywane typami - są klasycznymi formułami logicznymi.
Na poziomie bezkwantyfikatorowym, teorią równań jest λ-kalkulus z parowaniem suriektywnym' i niektóre jego podsystemy, odpowiednio udekorowane.
Rozszerzenie na kwantyfikatory propozycjonalne pierwszego i drugiego rzędu jest proste.
Książka składa się ze zbioru notatek i artykułów napisanych i rozpowszechnionych w ciągu ostatnich dziesięciu lat, jako kontynuacja wcześniejszych badań prowadzonych przez autora w latach osiemdziesiątych.
Zawiera między innymi przegląd początków współczesnej teorii dowodu - od Fregego do Gentzena - z punktu widzenia teorii świadków, a także charakterystyczne zastosowanie teorii świadków do praktycznego problemu logicznego dotyczącego aksjomatyzowalności.
