RICERCA ITALIANA     

'Mathesis Universalis', oggetti astratti e processi formali.

Scuola Normale Superiore di Pisa

Abstract

‘Mathesis universalis’ è il termine impiegato da Leibniz per designare la sua arte combinatoria o ‘characteristica universalis’, e successivamente adottato da Husserl per designare la logica pura, intesa come “la scienza eidetica dell’oggetto in generale”. Con questa denominazione si vuole alludere a una tradizione nella storia della logica che procede da Leibniz passando per Bolzano, Frege e Husserl fino a Goedel e coinvolge tematiche attuali della filosofia della logica. La ricerca proposta ha una duplice natura, storica e teoretica, e si articola sostanzialmente secondo due linee di ricerca interconnesse:

1) linea di ricerca 1: storia e filosofia della logica, con particolare riferimento alla tradizione dell’oggettivismo logico (quattro sono gli autori che occupano un ruolo preminente in questa direzione: Leibniz, Bolzano, Frege, Husserl);

2) linea di ricerca 2: filosofia della logica e ricerche logiche in senso proprio (la contrapposizione fra momento intensionale e momento estensionale nella logica e nei fondamenti della matematica: le nozioni di ‘tipo’, ‘regola’ , ‘insieme’ e le teorie ad esse pertinenti).

Il passaggio dalle indagini storiche alla riflessione teoretica e alle ricerche logico-formali è innescato dall’osservazione che la coppia concettuale fregeana ‘senso/riferimento’ induce naturalmente - nell’ambito della logica contemporanea – una parallela indagine del nesso fra oggetti astratti e processi formali.


I principali temi e obiettivi della ricerca si lasciano così riassumere:

Linea di ricerca 1:

a) ricostruzione delle idee logiche di Leibniz con particolare attenzione agli aspetti intensionali ed estensionali dei suoi calcoli logici;
b) individuazione degli assunti basilari dell’oggettivismo logico in Bolzano, Frege, Husserl e altri autori della scuola di Brentano, con particolare riferimento ai fondamenti della semantica e dell’ontologia;
c) analisi dei contributi del primo Husserl (1891-1903) alla logica e ai suoi fondamenti;
d) giustificazione del ruolo della fenomenologia nelle riflessioni contemporanee sulla filosofia della matematica (con particolare riferimento all’intuizionismo e al platonismo goedeliano).


Linea di ricerca 2:

a) indagini su (frammenti interessanti de) la teoria dei tipi costruttiva alla Martin-Loef e la teoria costruttiva degli insiemi, mediante tecniche semantiche e di teoria della dimostrazione;
b) studio di cornici logiche di varia forza adeguate a integrare entità estensionali (insiemi) ed entità intensionali (regole, proprietà);
c) indagini sulle teorie delle operazioni e calcoli equazionali corrispondenti, mediante nuovi sistemi analitici di prova;
d) studio dei fondamenti concettuali delle logiche sottostrutturali e della loro applicabilità a specifiche teorie degli insiemi e delle operazioni. <<<

Coordinatore Scientifico del Programma di Ricerca

Massimo Mugnai Scuola Normale Superiore di PISA

Obiettivo del Programma di Ricerca

‘Mathesis universalis’ è il termine impiegato da Leibniz per designare la sua arte combinatoria o ‘characteristica universalis’, e successivamente da Husserl per designare la logica pura, intesa come “la scienza eidetica dell’oggetto in generale”. Abbiamo fatto ricorso a questa denominazione intendendo con ciò alludere a una tradizione nella storia della logica che procede da Leibniz passando per Bolzano, Frege e Husserl fino a Goedel e coinvolge tematiche attuali della filosofia della logica. Il titolo prescelto intende appunto evidenziare la natura duplice, storica e teoretica, della ricerca proposta.

Il progetto si articola sostanzialmente secondo due linee di ricerca interconnesse, che toccano un una serie di specifiche questioni storiche, filosofiche e logiche:

1) linea di ricerca 1: storia e filosofia della logica, con particolare riferimento alla tradizione dell’oggettivismo logico (Leibniz, Bolzano, Frege, Husserl);

2) linea di ricerca 2: filosofia della logica e ricerche logiche in senso proprio (la contrapposizione fra momento intensionale e momento estensionale nella logica e nei fondamenti della matematica: nozioni di ‘tipo’, ‘regola’ , ‘insieme’ e teorie ad esse pertinenti).

Gli obbiettivi particolari da raggiungere nel contesto del progetto saranno di conseguenza presentati e ripartiti secondo due distinte liste tematiche:

Linea di ricerca 1:

a) ricostruzione delle principali caratteristiche delle idee logiche leibniziane (con speciale attenzione al nesso intensione/estensione nei calcoli di Leibniz);
b) analisi del concetto di fondazione (Begründung) in rapporto alla distinzione bolzaniana ben nota a Husserl fra derivabilità (Ableitbarkeit) e consecutività (Abfolge);
c) valutazione del grado di congruenza fra la semantica di Frege e quella di Bolzano;
d) analisi comparativa del lavoro di Frege con quello di autori riconducibili alla scuola di Brentano; individuazione nella semantica fregeana di elementi affini alla tradizione semantica classica;
e) spiegazione delle nozioni di ‘nesso di cose’ e di ‘nesso di verità’, in particolare con riferimento al cap. XI dei Prolegomeni di Husserl;
f) interpretazione dell’affermazione husserliana secondo la quale un concetto fonda o determina un dominio concettuale (Begriffsgebiet);
g ) caratterizzazione esaustiva del concetto husserliano di calcolo (Rechnen);
h) valutazione delle riflessioni husserliane sul tempo per spiegare gli oggetti matematici;
i) chiarificazione del nesso fra la nozione husserliana di grado di evidenza e io trascendentale e loro comparazione con i gradi di evidenza alla Heyting;
j) analisi della nozione di ‘soggetto creativo’ e del problema dell’accettabilità fenomenologica delle successioni di libera scelta;
k) giustificazione dell’uso della fenomenologia a fondamento sia dell’intuizionismo sia del platonismo goedeliano; il problema della conciliazione fra intuizionismo e fedeltà husserliana alle leggi logiche classiche.

Il passaggio dalle indagini storiche alla riflessione teoretica e alle ricerche logico-formali è innescato dall’osservazione che la coppia concettuale fregeana ‘senso/riferimento’ induce naturalmente – nell’ambito della logica contemporanea – una parallela indagine del nesso dialettico fra oggetti astratti e processi formali, fra semantica operazionale e semantica denotazionale. Questa contrapposizione si lascia specificamente rintracciare nella relazione di base che soggiace alla teoria dei tipi, alla stessa corrispondenza di Curry-Howard, e in ultima analisi alla forma fondamentale di giudizio della teoria dei tipi, ‘a è di tipo B’ (essendo ‘a’ una costruzione e B il tipo della costruzione, nesso che ricorda ovviamente e fonda la relazione standard fra soggetto e predicato).
Gran parte delle ricerche raccolte sotto la seconda linea tematica costituiscono un tentativo di fornire un'interpretazione alternativa di cosa significhi essere una costruzione (un elemento, una dimostrazione, una operazione) e di cosa voglia dire essere un tipo (o una classificazione).

Linea di ricerca 2. Obiettivi pertinenti alla filosofia della logica e alla ricerca logica in senso stretto.

a) individuazione di una fondazione concettuale unificata per distinti metodi di semantica costruttiva (realizzabilità, teoria delle costruzioni e teorie costruttive dei tipi, metodi categoriali);
b) utilizzazione, in vista di a), della teoria costruttiva dei tipi o della teoria costruttiva degli insiemi;
c) combinazione di tecniche semantiche costruttive con i metodi diretti di teoria della dimostrazione, e adeguate al caso speciale della teoria costruttiva degli insiemi;
d) studio dei fondamenti concettuali delle cosiddette resource-logics (un terzo e più recente paradigma accanto alle tradizionali logica classica e logica intuizionistica);
e) raffinamento e generalizzazione dei risultati fin qui ottenuti intorno ai sistemi di prova equazionali analitici per la logica combinatoria e il lambda calcolo (non-tipati);
f) costruzione di modelli della teoria dei tipi di Martin-Loef in teorie forti delle operazioni;
g) sviluppo della teoria della dimostrazione della logica equazionale ed estensione dell’approccio analitico a teorie tipate delle operazioni;
h) studio di sottosistemi della teoria costruttiva degli insiemi, eventualmente estesa con operazioni, che siano significativi per le applicazioni, anche in presenza di principi che garantiscono l’esistenza di oggetti circolari.

Ciascun problema specifico verrà affrontato non solo per il suo intrinseco interesse ma anche con lo scopo di stabilire una interazione fruttuosa fra tematiche non solo tecniche, ma anche concettuali e storiche, al fine di contribuire alla comprensione del problema principale che sta alla base del progetto, ovvero quello del nesso fra oggetti astratti della logica e i processi formali che ad essi si riferiscono.
I nessi e le interazioni previste fra le quattro unità di ricerca sono evidenziati dal seguente diagramma:

1) Un I-Un III (SNS-Milano): Husserl; oggettivismo logico;
2) Un I-Un IV (SNS-Pisa): Bolzano, Frege; oggettivismo logico;
3) Un II-Un IV (Firenze-Pisa): teoria costruttiva dei tipi MLTT, logica combinatoria e lambda calcolo, logiche sottostrutturali;
4) Un II-Un III (Firenze-Milano): fondamenti del costruttivismo ed intuizionismo;
5) Un II-Un I (Firenze-SNS): logica in forma algebrica (logica equazionale di Leibniz); aspetti intensionali ed estensionali della logica ;
6) Un IV-Un III (Pisa-Milano): fondamenti dell’intuizionismo e Husserl.

Risultati attesi (sommario)

(i) Storia della logica: avanzamento della nostra comprensione di aspetti centrali della logica di Leibniz, di Frege e di Husserl
(ii) filosofia della logica: una valutazione critica complessiva dei fondamenti fenomenologici dell’intuizionismo; chiarificazione dei fondamenti filosofici della teoria dei tipi e analisi delle conseguenze sulla ontologia della logica e della matematica;
(iii) logica: contributi tecnici specifici in teoria della dimostrazione per teorie sensibili dei tipi e degli insiemi, per sistemi funzionali ed equazionali; costruzione di sistemi di teoria delle classi(ficazioni) basati su logiche sottostrutturali.

Come concreto risultato della ricerche storicamente orientate, è programmata la pubblicazione di due volumi:
a) una raccolta commentata di saggi logici leibniziani tradotti in Italiano (principalmente le “Generales Inquisitiones de analysi notionum et veritatum”) con una ricca introduzione al testo;
b) una monografia sulle teorie logiche e matematiche del primo Husserl. La monografia verrà scritta in Inglese per una casa editrice internazionale.

Per quel che riguarda i risultati concreti delle ricerche teoriche, è programmata la pubblicazione di:

c) saggi su riviste nazionali e internazionali sui risultati ottenuti nell’ambito della logica e della filosofia della logica;
d) un volume di atti degli incontri dedicati alla discussione dei risultati intermedi delle unità di ricerca. <<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

Illustriamo lo stato dell’arte relativo ai principali snodi tematici (storici, filosofici, logici) del progetto di ricerca seguendo la suddivisione di quest’ultimo nelle sue due linee di ricerca portanti (cf. la descrizione dettagliata degli obiettivi del progetto):
(1) Storia e filosofia della logica (oggettivismo logico; Leibniz, Bolzano, Frege, Husserl; fenomenologia, intuizionismo e platonismo).
(2) Filosofia della logica e indagini logiche (intensionalità / estensionalità in logica e nei fondamenti della matematica; tipi, regole, insiemi e relative teorie).

LINEA DI RICERCA 1
a) La logica di Leibniz. Sebbene la letteratura secondaria sulla filosofia di Leibniz abbia conosciuto uno straordinario sviluppo nel secolo scorso, le monografie dedicate a uno studio sistematico delle concezioni logiche leibniziane sono relativamente poche. Un elenco delle più rilevanti non supera le quattro opere: 1) il classico libro di L. Couturat: La logique de Leibniz, Paris, 1901; 2) la monografia di R. Kauppi: Über die Leibnizschen Logik (Helsinki, 1960); il volume di H. Burkhardt: Logik und Semiothik in der Philosophie von Leibniz (München, 1980); 4) la recente raccolta di saggi di W. Lenzen: Calculus Universalis: Studien zur Logik von G. W. Leibniz (Paderborn, 2004). A tali lavori vanno senz'altro aggiunti: a) l'introduzione di G. H. R. Parkinson alla raccolta di scritti logici leibniziani: Leibniz, Logical Papers, Oxford, 1966 (pp. viii - lxv); b) l'ampio commento di Franz Schupp alle Ricerche generali (G. W. Leibniz, Allgemeine Untersuchungen über die Analyse der Begriffe und Wahrheiten, Hamburg, 1982 (pp. 135-242)); c) l'introduzione e commento, sempre a opera di F. Schupp a G. W. Leibniz, Die Grundlagen des logischen Kalküls, Hamburg, 2000, pp. vii-lxxxvi, 157-264. In lingua francese un'utile raccolta di testi logici (e metafisici) di Leibniz è costituita da G.W. Leibniz, Recherches générales sur l'analyse des notions et des vérités, Paris, 1998. La recente pubblicazione di gran parte dei manoscritti logici leibniziani in edizione critica (Akademie Verlag, Münster-Berlin, 1999) ha cambiato notevolmente la nostra conoscenza della logica di Leibniz e ha reso obsoleti molti lavori che sul tema sono stati pubblicati finora. Ciò è vero anche della maggiore raccolta di scritti logici leibniziani tradotti in italiano, curata da F. Barone alla fine degli anni Sessanta del secolo scorso (Bologna, 1968; Bari, 1992, voll. I e II). L'opera di Barone, infatti, non solo contiene testi che ormai, in confronto all'edizione critica, non sono più affidabili, ma è anche accompagnata da un commento e da note esplicative che risultano datati e, per certi aspetti, sono al di sotto degli standard raggiunti, per esempio, dalle analoghe edizioni curate da Schupp in Germania. Rimane dunque l'esigenza, da un lato, di un lavoro di analisi e di interpretazione delle opere logiche di Leibniz che tenga conto dei nuovi testi, e dall'altro di avere disponibile anche in italiano una raccolta di opere logiche leibniziane commentata e annotata, al pari di quelle presenti in Germania e Francia.

b) Interrelazioni tra le dottrine logiche di Leibniz, Bolzano e Husserl. Nella Wissenschaftslehre (§ 21), Bolzano menziona Leibniz come ‘precursore' della sua nozione di proposizione in sé (Satz an sich). A. Church e I. Berg hanno sollevato qualche dubbio sulla correttezza di siffatta attribuzione (cfr. A. Church, Propositions and Sentences, in I. M. Bochenski, A. Church, N. Goodman, The Problem of the Universals, Notre Dame, 1956, p. 3; I. Berg, Bolzano's Logic, Stockholm, 1962, pp. 51-52): è assai probabile, tuttavia, che l'indicazione bolzaniana corrisponda a verità (cfr. M. Mugnai, Leibniz and Bolzano on the "Realm of Truths", in Bolzano's Wissenschaftslehre: 1837-1987, Firenze, 1992, pp. 207-20). In ogni caso, Bolzano si richiama numerose volte, sia nella Wissenschaftslehre sia in altre opere, a Leibniz e al suo lascito intellettuale, proponendosi di svilupparne le dottrine in ambito logico, ontologico e metafisico. Ciononostante, sono pur sempre pochi gli studi specificamente dedicati all'approfondimento delle relazioni reciproche tra questi due pensatori; anche in tal caso manca un lavoro sistematico che studi questa questione.
L'apprezzamento estremamente positivo dell'opera di Bolzano da parte di Husserl (alla fine dei Prolegomeni alle Ricerche logiche) sembra avere dato finora soltanto un debole impulso agli studi orientati a stabilire un confronto tra le dottrine logiche di Bolzano e quelle di Husserl. Inoltre, le più recenti opere sulla filosofia husserliana rivelano un diminuito interesse per le idee di Husserl riguardanti la logica e la matematica. E addirittura autori interessati alla filosofia della matematica husserliana sembrano non aver più una sufficiente familiarità con gli sviluppi della logica e della matematica che costituiscono lo sfondo storico contro il quale vengono elaborate le dottrine di Husserl. (Basti un esempio fra molti: il curatore della Logikvorlesung 1896 nella recente edizione critica confonde il filosofo Sir William Hamilton, del quale Husserl discute le dottrine, col matematico William Rowan Hamilton, noto per avere scoperto i cosiddetti ‘quaternioni'!). Al tempo stesso, non viene fatto alcuno sforzo, nella letteratura secondaria, per connettere le idee di Husserl riguardo alla logica e all'ontologia con l'eredità di Leibniz e di Bolzano.

c) Frege e la tradizione filosofica. Sono ormai numerosi i lavori concernenti i rapporti di Frege con la tradizione filosofica (non solo, quindi, strettamente logica). Particolare attenzione è stata dedicata al rapporto tra Frege e Kant, con risultati interpretativi a volte antitetici: alcuni, come Sluga (Gottlob Frege, Boston, 1980) e (in parte) Angelelli (Studies on Gottlob Frege and Traditional Philosophy, Dordrecht 1967), hanno inserito Frege nell'ambito della rinascita kantiana in Germania, altri, come Coffa (The Semantic Tradition from Kant to Carnap, Cambridge 1991), lo hanno visto come una tappa importante nel percorso, iniziato da Bolzano, dell'abbandono dell'intuizione nella pratica della matematica e nella ricerca sui suoi fondamenti. Al contrario, con l'eccezione del libro di Angelelli (che risale però a quasi quaranta anni fa), minore attenzione è stata dedicata alle relazioni dell'opera di Frege con le tematiche tradizionali della ricerca filosofica, se si eccettua ovviamente la ripresa e trasformazione dell'idea di una lingua formale insita nel progetto leibniziano della mathesis universalis.

d) Fenomenologia, intuizionismo, platonismo goedeliano. All'interno dei vari tentativi di ricavare dalle opere di Husserl del periodo successivo a quello della "Filosofia dell'aritmetica" una definizione di numero e, piu' in generale, di oggetto matematico, si è venuto recentemente a formare, a livello internazionale, un filone di ricerca che si è proposto più specificamente di utilizzare metodi e tematiche husserliane per rimediare ad alcune falle che si erano aperte nell'edificio intuizionista e che ne avevano minato la credibilità come scuola fondazionale. In particolare, la nozione di evidenza, che l'intuizionismo aveva proposto come criterio di verità per le proposizioni e di esistenza per gli oggetti matematici, era stata messa in crisi dagli intuizionisti stessi (Griss, Heyting) in quanto non completamente convinti dell'accettabilità della nozione di negazione e della nozione di successione di libera scelta. A. Heyting, negli anni Cinquanta, aveva prima proposto una "scala di evidenze", in cui i numeri naturali piccoli, quelli grandi, le successioni di libera scelta, la negazione, la quantificazione universale venivano a occupare posizioni diverse in un contesto, ancora, di fede comune intuizionista nell'evidenza come fonte assoluta di certezza; poi, negli anni Sessanta, aveva preso atto, stante proprio tale scala, dell'impossibilità di considerare l'evidenza come criterio e quindi, viste le problematiche che avevano già da decenni indebolito il logicismo e il formalismo, aveva dichiarato conclusa l'epoca fondazionale e aveva indicato nuovi compiti per la filosofia della matematica (v. Franchella, Heyting's contribution to the change in research into the foundations of mathematics, History and Philosophy of Logic 15, 1994). A partire dalla definizione di numeri ed insiemi che Richard Tieszen ha offerto (v. per es. Tieszen, Mathematical Intuition: Phenomenology and Mathematical Knowledge, Dordrecht, 1989), Mark van Atten ha suggerito, in una serie di libri ed articoli (1999-2004), la possibilità di usare la specifica nozione fenomenologica di gradi di evidenze per rimediare alle problematiche di cui sopra e la possibilità di utilizzare l'ego trascendentale per rimediare all'accusa di psicologismo relativa alle successioni di libera scelta. Va sottolineato che i medesimi autori citati hanno contemporaneamente proceduto ad uno studio dei rapporti fra Goedel e Husserl, che comprendeva anche l'utilizzo della fenomenologia per rispondere alle critiche epistemologiche di Paul Benacerraf al platonismo goedeliano


LINEA DI RICERCA 2.
a) Estensionalità / intensionalità.
Per quanto l'indagine storica sia utile a comprendere più a fondo le motivazioni e la struttura della semantica fregeana, l'importanza di quest'ultima risiede soprattutto in ciò che da essa ha avuto origine. E non solo (com’è ovvio) per quel che riguarda la filosofia del linguaggio. Alla distinzione fregeana tra senso e significato si richiama infatti una duplicità di prospettiva nello studio delle operazioni logiche e matematiche: da un lato quella in cui viene privilegiato il risultato ottenuto, dall'altro quella in cui si cerca di mettere a fuoco il processo, la serie di passi e istruzioni che a quel risultato conducono. Se il primo punto di vista ha trovato una soddisfacente sistemazione nella semantica "denotazionale" di tipo algebrico-insiemistico, i primi passi nello studio del secondo punto di vista sono da rintracciare nelle più o meno esplicite indicazioni contenute nelle ricerche sulle diverse formalizzazioni della sintassi sviluppate da G. Gentzen, il cui tratto caratteristico qui pertinente è lo spostamento dal "che cosa" al "come". Il centro dell'interesse non è più costituito da quanto si dimostra entro una data teoria, ma da come si dimostra (e quindi risultati di normalizzazione, sottoformula, interpolazione, linearità, ecc.). Si tratta di caratteristiche "intensionali" che permettono di differenziare argomentazioni estensionalmente coincidenti, nel senso che sorreggono una stessa affermazione. Strettamente connessa, da questo punto di vista, con le ricerche di Gentzen è l'analisi della funzionalità fornita dal lambda-calcolo di A. Church: un suo tratto fondamentale è il fatto che viene recuperata la dimensione intensionale di contro a quella puramente estensionale delle funzioni calcolate (ad esempio procedure diverse che calcolano le stesse funzioni possono essere interessanti oggetti autonomi di studio a causa delle loro diverse definizioni e caratteristiche, di velocità, eleganza, modularità, ecc.). Fondamentale, poi, è anche la visione unificante di queste due prospettive fornita, in un quadro generale fondamentalmente costruttivo, dal cosiddetto “isomorfismo di Curry-Howard”.


b) Tipi, regole, insiemi e relative teorie. Riguardo ai sistemi tipati, un primo genere di formalismo da prendere in considerazione è costituito dalle teorie costruttive delle operazioni e delle classi di Feferman (EM, “Matematica esplicita”; S. Feferman, A language and axioms for explicit mathematics, Lectures Notes in Mathematics vol. 450, Berlin 1975, 87-139), dove la stessa nozione di regola-in-intensione e la nozione di predicato sono primitive.
Una via alternativa è basata sulla teoria costruttiva dei tipi MLTT, sviluppata da Per Martin-Loef e la sua scuola nei primi anni '70 del '900 (si veda, p. es., Martin Loef, Intuitionistic type theory, Napoli 1984), i cui assunti basilari sono il predicativismo e la specificazione canonica degli elementi dei tipi. MLTT può essere effettivamente vista come un'implementazione delle idee di Poincaré circa le classi predicative.
Un problema concettuale di base è ovviamente l'esistenza o meno di un modo per rendere sensato il ragionamento insiemistico estensionale (= il ragionamento matematico standard) in MLTT. È un fatto importante che Peter Aczel, verso la fine degli anni '70, abbia dimostrato che una versione predicativa, detta CZF, della teoria degli insiemi - variante di una teoria costruttiva che era stata sviluppata da Myhill del 1975, come una teoria-quadro per l'analisi costruttiva nello stile di Bishop - possa essere interpretata mediante la teoria costruttiva dei tipi MLTT. Ciò dimostra che esiste una nozione genuina di insieme costruttivo che è ottenuta mediante la sola analisi concettuale senza alcuna restrizione artificiosa ad una logica di tipo costruttivo, ma che necessita, occorre sottolinearlo, l'adozione di una teoria che comprenda, in un contesto unitario, operazioni e tipi. Ricordiamo per inciso una mossa provvisoria in questa direzione: il lavoro recente di Cantini e Crosilla (A. Cantini, L. Crosilla, Constructive set theory with rules, Proceedings of the European Logic Colloquium 2004, Torino; in corso di stampa) definisce una teoria unificata di operazioni e insiemi costruttivi, che estende CZF mediante una struttura applicativa e rende possibile esprimere uniformemente ed esplicitamente parecchi costrutti insiemistici. Dal punto di vista della teoria della dimostrazione, il sistema è conservativo e ammette un modello in particolari strutture applicative (varianti delle strutture di Frege).
Ora, MLTT è in effetti una teoria del significato per gli enunciati logici e matematici che implementa rigidamente l'idea alla base della cosiddetta corrispondenza di Curry-Howard: ossia l'idea che una proposizione dovrebbe essere grossolanamente identificata con l'insieme delle sue dimostrazioni, o con un problema le cui soluzioni sono date dalle dimostrazioni di essa (v. sopra, punto (a)). Se si riuscisse a dimostrare che CZF è una teoria matematicamente effettiva, si potrebbe altresì affermare che, rispetto a un esempio rilevante dell'indagine, è possibile sviluppare una teoria degli oggetti matematici nella quale l'aspetto epistemico e intensionale (come giungiamo a conoscere le proprietà di tali entità), non è separato dall'aspetto puramente ontologico e referenziale (ciò di cui si sta parlando).
Un aspetto cruciale che è comune tanto a MLTT quanto alla teorie EM di Feferman è che queste teorie possiedono una soggiacente teoria delle operazioni che sono tipate nel primo caso e non tipate nel secondo. Da un lato, la struttura applicativa ha il compito di ridurre gli elementi di un tipo che non sono in forma canonica, ossia di termini che rappresentino algoritmi, alla forma canonica: le regole di eliminazione di MLTT comprendono certe equazioni alle quali spetta tale riduzione. Dal lato di EM, la struttura applicativa è non tipata ed è la teoria stessa che classifica le operazioni in tipi. In entrambi i casi, la base operazionale ha più che altro il ruolo di guida e non ha ricevuto una grande attenzione. In questo contesto, si dovranno pertanto tenere presente i calcoli equazionali analitici recentemente introdotti (P. Minari, Proof-theoretical methods in combinatory logic and lambda-calculus, CIE 2005: New Computational Paradigms, Amsterdam 2005, 148-157) per la logica combinatoria e il lambda-calcolo (con e senza estensionalità). Tali nuovi sistemi dimostrativi risultano essere analitici grazie al risultato principale che mostra (in modo costruttivo) che la regola di transitività per l'uguaglianza è eliminabile. Ne risultano derivazioni analitiche con buone proprietà strutturali che possono essere applicate per ottenere una non banale semplificazione della teoria della dimostrazione dei calcoli equazionali applicativi corrispondenti. <<<