Fondazioni Insiemistiche della Matematica Costruttiva

La teoria costruttiva degli insiemi (Myhill 1975, Aczel 1978) sorge comefondazione per la matematica costruttiva alla Bishop (Bishop 1967, Bishop e Bridges 1985). Motivazione principale e' il pervenire ad un sistema di teoria degli insiemi basato sulla logica intuizionistica che consenta la formalizzazione della matematica costruttiva in modo del tutto analogo e altrettanto semplice della fondazione della matematica classica sulla teoria Zermelo Fraenkel. Chiaramente il passaggio dalla logica classica a quella intuizionistica apre un vastissimo raggio di scelta tra possibili varianti degli assiomi classici, producendo teorie di forza distinta. Presenteremo la teoria CZF (Constructive Zermelo Fraenkel) introdotta da Aczel, che si caratterizza per il suo affiancare ad una limitata forza proof teoretica una notevole capacita' espressiva, cosi' soddisfacendo un criterio di minimalita' senza per questo rinunciare ad essere una fondazione efficace per la matematica costruttiva. Ad esemplificazione del potere espressivo di CZF mostreremo il caso dell'insieme dei numeri reali alla Dedekind. Qualora ve ne sia il tempo presenteremo inoltre alcuni nuovi risultati ottenuti in cooperazione con Hajime Ishihara e Peter Schuster relativi a varianti dell'assioma di fullness, forse uno dei meno noti principi della teoria.