S. Valentini, Points and Co-Points in Formal Topology

Bollettino dell'Unione Matematica Italiana, 7--A, 1993, pp. 7--19.

Abstract: After a short introduction on formal topology the definition of point and co-point are given. Then some methods to construct points and co-points are shown together with some applications to logic.

S. Valentini, Le relazioni ordinate: definizioni di base ed applicazioni,

in "Atti del XV^o incontro di Logica Matematica", vol. VIII, Gerla, Toffalori, Tulipani (eds), 1993.

Abstract: Nel lavoro vengono introdotte le relazioni ordinate come relazioni binarie sugli elementi di una struttura algebrica ordinata che permettono di darne una rappresentazione di carattere insiemistico. Si studiano in particolare il caso dei monoidi ordinati, dei quantales e delle algebre lineari non commutative, vale a dire le strutture algebriche per la logica lineare non commutativa.

Paulus Venetus (alias G. Sambin, S. Valentini), Propositum Cameriniense sive etiam itinera certaminis inter rationem insiemes aedificandi analisym situs intuitionisticamque et mathematicae artium reliquas res,

in "Atti del XV^o incontro di Logica Matematica", vol. VIII, Gerla, Toffalori, Tulipani (eds), 1993, pp. 115-143.

Abstract: In questo articolo viene illustrato il lavoro che l'autore ha portato avanti soprattuto a Padova. Esso si propone, un po' ambiziosamente, di ricostruire algebra e topologia all'interno della teoria intuizionistica dei tipi di Martin-Löf o di qualche sua opportuna estensione. Il vantaggio di sviluppare una teoria matematica all'interno di una teoria costruttiva degli insiemi, a patto di non farsi prendere da manie fondamentaliste troppo rigide, consiste principalmente nel poter controllare il grado di costruttività dei risultati ottenuti o meglio, come vedremo, di controllare il grado di "distruttività", cioè di astrazione e di idealizzazione, che si è disposti ad accettare. I principali risultati ottenuti fino ad ora comprendono, oltre alle necessarie definizioni, alcuni teoremi di rappresentazione per reticoli completi, quantale e locale, e quindi teoremi di completezza per la logica lineare ed intuizionista sia proposizionale che predicativa, e la definizione degli spazi topologici e dei loro punti, con particolare attenzione agli spazi di Scott e di Stone.

S. Valentini, Representation Theorems for Quantales,

Mathematical Logic Quarterly, 40 (1993), pp. 182-190.

Abstract: In this paper we prove that any quantale Q is (isomorphic to) a quantale of suitable relations on Q. As a consequence two isomorphism theorems are also shown with suitable sets of functions of Q into Q. These theorems are the mathematical background one needs in order to give natural and complete semantics for (non-commutative) Linear Logic using relations.

G. Sambin, S. Valentini, P. Virgili, Constructive Domain Theory as a branch of Intuitionistic Pointfree Topology,

Theoretical Computer Science 159 (1996), pp. 319-341

Abstract: In this paper, the notions of information base and of translation between information bases are introduced; they have a very simple intuitive interpretation and can be taken as an alternative approach to domain theory. Technically, they form a category which is equivalent to the category of Scott domains and approximable mappings. All the definitions and most of the results are inspired by the intuitionistic approach to pointfree topology as developed mainly by Martin-Löf and the first author. As in intuitionistic pointfree topology, constructivity is guaranteed by adopting the framework of Martin-Löf's intuitionistic type theory, equipped with a few abbreviations which allow to use a standard set theoretic notation.

S. Valentini, A completeness theorem for formal topologies,

in "Logic and Algebra" (ed. Ursini, Aglianò), Dekker, New York, 1996, pp. 689-702.

Abstract: The main mathematical result of this work is a quite simple formulation and proof of a Rasiowa-Sikorski-like theorem for countable lattices. Then the paper suggests an interpretation of this mathematical result as a completeness theorem for the formal topologies introduced by G. Sambin in order to provide a constructive approach to topology which is expressible within Martin Löf's intuitionistic theory of types. This completeness theorem shows that, as long as one is interested in dealing only with the coverage relation between two open sets of a topology, within a constructive framework, a very simple mathematical structure is needed. It is necessary to stress that the completeness theorem holds because of the "weak" intuitionistic set and subset theory that we use when dealing with formal topologies.

S. Negri, S. Valentini, Tychonoff's theorem in the framework of formal topologies,

Journal of Symbolic Logic, 1997.

Abstract: In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology.

S. Valentini, A cartesian closed category in Martin-Löf's intuitionistic type theory,

Theoretical Computer Science, 2001.

Abstract: First, we briefly recall the main definitions of the theory of Information Bases and Translations. These mathematical structures are the basis to construct the cartesian closed category InfBas, which is equivalent to the category ScDom of Scott Domains. Then, we will show that all the definitions and the proof of all the properties that one needs in order to show that InfBas is indeed a cartesian closed category can be formalized within Martin-Löf's Intuitionistic Type Theory.

S. Valentini, On the formal points of the formal topology of the binary tree,

Archive for Mathematical Logic, 2001.

Abstract: Formal topology is today an established topic in the development of constructive mathematics and constructive proofs for many classical results of general topology have been obtained by using this approach. Here we analyze one of the main concepts in formal topology, namely, the notion of formal point. We will contrast two classically equivalent definitions of formal points and we will see that from a constructive point of view they are completely different. Indeed, according to the first definition the formal points of the formal topology of the real numbers can be indexed by a set whereas this is not possible according to the second one.