The entanglement of logic and set theory, constructively

Le teorie degli insiemi quali la teoria Zermelo Fraenkel (ZF) sono in genere introdotte come se fossero la combinazione di due tipi distinti di principi (ovvero, assiomi, schemi, regole): i principi logici e quelli propriamente insiemistici. I principi insiemistici vengono dunque presentati come se fossero sovrapposti alla base della logica del primo ordine. Questo modo di presentare la teoria degli insiemi ben si concilia con una visione tradizionale della logica come universalmente applicabile e neutrale, ovvero non dipendente dal tipo di soggetto a cui si applica. Tale interpretazione della logica è stata rifiutata dagli intuizionisti, sulla base di una riflessione sulla quantificazione su domini infiniti. L'idea è che la quantificazione su domini infiniti richieda l'utilizzo della logica intuizionista invece che di quella classica. In questo articolo considero teorie degli insiemi costruttive, ovvero teorie che usano la logica intuizionista piuttosto che quella classica e sostengo che esse manifestano una interdipendenza o un 'entanglement' delle nozioni insiemistiche e logiche. In modo più specifico, osservo come la teoria dei tipi di Martin-Löf identifichi nozioni fondamentali della logica e della teoria degli insiemi. Uno dei motivi per questa identificazione è l'idea che la quantificazione classica su domini infiniti sia problematica, mentre quella intuizionista non lo sia. L'approccio alla quantificazione caratteristico della teoria dei tipi di Martin-Löf ha connessioni profonde e complesse con la predicatività di questa teoria. Concludo l'articolo ricordando i tratti principali di un approccio alla predicatività ispirato da Poincaré. Tale approccio è anch'esso incentrato sulla questione della corretta quantificazione su domini infiniti. Concludo con un confronto con teoria dei tipi di Martin-Löf . Theories of sets such as Zermelo Fraenkel set theory are usually presented as the combination of two distinct kinds of principles: logical and set-theoretic principles. The set-theoretic principles are imposed ‘on top’ of first-order logic. This is in agreement with a traditional view of logic as universally applicable and topic neutral. Such a view of logic has been rejected by the intuitionists, on the ground that quantification over infinite domains requires the use of intuitionistic rather than classical logic. In the following, I consider constructive set theories, which use intuitionistic rather than classical logic, and argue that they manifest a distinctive interdependence or an entanglement between sets and logic. In fact, Martin-Löf type theory identifies fundamental logical and set-theoretic notions. Remarkably, one of the motivations for this identification is the thought that classical quantification over infinite domains is problematic, while intuitionistic quantification is not. The approach to quantification adopted in Martin-Löf’s type theory is subtly interconnected with its predicativity. I conclude by recalling key aspects of an approach to predicativity inspired by Poincaré, which focuses on the issue of correct quantification over infinite domains and relate it back to Martin-Löf type theory.