Craig's interpolation theorem in computation theory

Si espongono alcuni risultati, provati dall’Autore negli articoli citati nella bibliografia, a proposito della complessità del teorema d’interpolazione di Craig: con ciò si intende la relazione tra la lunghezza (cioè il numero di simboli) della formula $\chi$ e la lunghezza di $\varphi$ e $\psi$, ove $\varphi \to \psi$ è un’implicazione valida, e $\chi$ è un interpolante, come esibito dal teorema di interpolazione stesso. Si intende altresì sottolineare la rilevanza dello studio della complessità dell’interpolazione per far luce su alcuni importanti problemi della teoria degli algoritmi, con particolare riferimento al problema della complessità dei sistemi naturali di deduzione nella logica delle proposizioni (essenzialmente, problema PNP), oppure il problema di correlare tra loro diverse misure della complessità di una funzione, ad esempio, il tempo occorrente ad una macchina di Turing per calcolare la funzione, rispetto al tempo occorrente ad un circuito «logico».