Teoria del testimone: Appunti sul calcolo e la logica di λ

Titolo originale:

Witness Theory: Notes on λ-calculus and Logic

Contenuto del libro:

Questo libro si occupa dell'analisi matematica del concetto di prova formale nella logica classica e registra - in sostanza - un più lungo esercizio di λ-calcolo applicato.

Seguendo i termini colloquiali che risalgono a L. E. J. Brouwer, gli oggetti di studio di questa impresa sono chiamati testimoni. Un testimone è destinato a rappresentare la prova logica di una formula classicamente valida, in un determinato contesto di prova. I formalismi utilizzati per esprimere i testimoni e il loro comportamento equazionale sono estensioni del λ-calcolo puro tipizzato, considerate come teorie equazionali.

Formalmente, un testimone è generato da variabili decorate - o tipizzate' -, che rappresentano le assunzioni, e da operatori di testimonianza, che rappresentano le regole logiche di inferenza.

Le specifiche equazionali servono a definire gli operatori del testimone.

In generale, questo può essere fatto ignorando la tipizzazione', cioè le formule logiche stesse.

Dal punto di vista teorico-modellistico, i testimoni sono oggetti di un modello estensionale Scott λ.

L'approccio - chiamato genericamente "teoria dei testimoni" - si ispira al lavoro di N. G. de Bruijn, su una teoria matematica della dimostrazione, svolto tra la fine degli anni '60 e l'inizio degli anni '70 presso l'Università di Eindhoven (Paesi Bassi), ed è simile all'approccio alla base della Corrispondenza di Curry-Howard, familiare alla logica intuizionistica.

Nel caso classico, le decorazioni - dette anche "tipi" - sono formule logiche classiche.

A livello quantificatorio, la teoria equazionale in questione è il λ-calcolo con accoppiamento surgiettivo' e alcuni suoi sottosistemi, opportunamente decorati.

L'estensione ai quantificatori proposizionali, del primo e del secondo ordine, è semplice.

Il libro consiste in una raccolta di note e documenti scritti e diffusi negli ultimi dieci anni, come continuazione di precedenti ricerche svolte dall'autore negli anni Ottanta.

Include, tra l'altro, una rassegna delle origini della moderna teoria delle prove - da Frege a Gentzen - dal punto di vista della teoria dei testimoni, nonché una caratteristica applicazione della teoria dei testimoni a un problema di logica pratica riguardante l'assiomatizzabilità.