Originaltitel:
Witness Theory: Notes on λ-calculus and Logic
Inhalt des Buches:
Dieses Buch befasst sich mit der mathematischen Analyse des Begriffs des formalen Beweises in der klassischen Logik und stellt im Wesentlichen eine längere Übung in angewandtem λ-Kalkül dar.
In Anlehnung an die auf L. E. J. Brouwer zurückgehende Umgangssprache werden die Untersuchungsobjekte in diesem Unternehmen als Zeugen bezeichnet. Ein Zeuge soll den logischen Beweis einer klassisch gültigen Formel in einem bestimmten Beweiskontext darstellen. Die Formalismen, die verwendet werden, um Zeugen und ihr Gleichsetzungsverhalten auszudrücken, sind Erweiterungen des rein typisierten λ-Kalküls, die als Gleichsetzungstheorien betrachtet werden.
Formal wird ein Zeuge aus dekorierten - oder typisierten' - Zeugenvariablen, die Annahmen darstellen, und Zeugenoperatoren, die logische Inferenzregeln darstellen, erzeugt.
Die Gleichungsspezifikationen dienen dazu, die Zeugenoperatoren zu definieren.
Im Allgemeinen kann dies unter Vernachlässigung der Typisierung", d. h. der logischen Formeln selbst, geschehen.
Modelltheoretisch sind die Zeugen Objekte eines extensionalen Scott λ-Modells.
Der Ansatz - allgemein als "Zeugnistheorie" bezeichnet - ist inspiriert von der Arbeit von N. G. de Bruijn an einer mathematischen Theorie des Beweisens, die in den späten 1960er und frühen 1970er Jahren an der Universität Eindhoven (Niederlande) durchgeführt wurde, und ähnelt dem Ansatz hinter der Curry-Howard-Korrespondenz, der aus der intuitionistischen Logik bekannt ist.
Für den klassischen Fall sind die Dekorationen - oft als Typen bezeichnet - Formeln der klassischen Logik.
Auf quantifikatorfreier Ebene ist die betreffende Gleichungstheorie der λ-Kalkül mit surjektiver Paarung" und einige Untersysteme davon, die entsprechend dekoriert sind.
Die Erweiterung auf propositionale Quantoren erster und zweiter Ordnung ist einfach.
Das Buch besteht aus einer Sammlung von Notizen und Papieren, die in den letzten zehn Jahren geschrieben und verbreitet wurden, als Fortsetzung früherer Forschungen des Autors aus den achtziger Jahren.
Es enthält unter anderem einen Überblick über die Ursprünge der modernen Beweistheorie - von Frege bis Gentzen - aus zeugnistheoretischer Sicht sowie eine charakteristische Anwendung der Zeugentheorie auf ein praktisches logisches Problem der Axiomatisierbarkeit.
Weitere Daten des Buches:
| ISBN: | 9781848903265 |
| Autor: | |
| Verlag: | |
| Sprache: | Englisch |
| Einband: | Taschenbuch |
Kauf:
Derzeit verfügbar, auf Lager.
