Abstract: Looking for a suitable logic for the subtype relation between the types of the intersection types lambda calculus we developed a modal logic with a two-places modality. We present here its main syntactical and semantical properties, that is, the completeness theorem, the finite model property, the cut-elimination theorem and a decision procedure for theoremhood.

Abstract: First we introduce the notion of super-coherent topology which does not depend on any ordering. Then we show that a topology is super-coherent if and only if it is the Scott topology over a suitable algebraic dcpo. The main ideas of the paper are a by-product of the constructive approach to domain theory through information bases which we have proposed in a previous work, but the presentation here does not rely on that foundational framework.

S. Valentini, Fixed-points of continuos functions between formal spaces,

Abstract: Formal topology is today an established topic in the development of constructive mathematics and constructive proofs for many classical results of general topology has been obtained by using this approach. In this work, after an introduction to the formal approach to constructive topology and its morphisms, we will show sufficient conditions for a continuous function between formal points to admit a fixed-point and we will illustrate an example to the problem of finding the fixed-point of a monotone operator which maps recursive subsets of the natural numbers into recursive subsets.

T. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies,

Abstract: Formal topology is today an established topic in the development of constructive, that is intuitionistic and predicative, mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not sensible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in a predicative way by an inductive generation and thus their properties can be proved inductively.

S. Valentini, Formal topology and search engine,

Abstract: Formal topology can be the key tool to create a new kind of search engine for finding information in the web.

S. Valentini, The problem of completeness of formal topologies with a binary positivity predicate and their inductive generation,

Abstract: Formal topologies are today an established topic in the development of constructive mathematics and many classical results of general topology have been already brought into the realm of constructive mathematics by using this approach. One of the main tools in formal topology is inductive generation and it has been completely solved the problem of inductively generating formal topologies with a cover relation and a unary positivity predicate, namely, the mathematical structures where the properties of the open subsets of a topological space can be expressed. Anyhow, in order to deal both with open and closed subsets, a binary positivity predicate has to be considered and a suitable axiomatization must be provided. In this paper we will show how to adapt to this framework the method used for the inductive generation of formal topologies with a unary positivity predicate since we have now to take into account both the cover relation and the positivity predicate in a general setting where both of them have proper axioms. Indeed, we will show that it is necessary to work in such a generality because the lack of a complete axiomatization of the topological spaces in the present definition of formal topology does not allow to determine the open and the closed subsets by using only the basic opens as it can be done in the classical case.

S. Valentini, A complete formalization of constructive topology,

Abstract: Looking for a complete formalization of constructive topology we analyzed the structure of the subsets of a Heyting algebra which correspond to the concrete closed and open sets of a topological space over its formal points. After this has been done, the rules for a formalization of constructive topology, which is both predicative and complete, are unveiled.

M. Maietti, S. Valentini, Exponentiation of unary topologies over inductively generated formal topologies,

Abstract: We prove that unary formal topologies are exponentiable in the category of inductively generated formal topologies. From an impredicative point of view, this means that algebraic dcpos with a bottom element are exponentiable in the category of open locales.

Abstract: In this paper a simple proof of the completeness theorem of the intuitionistic predicate calculus with respect to the topological semantics is shown. From a technical point of view the proof of the completeness theorem is based on a Rasiowa-Sikirski-like theorem for the countable Heyting algebras which allows to embadd any countable Heyting algebra into a suitable topology in a such way that a countable quantity of the existing suprema are respected.

M. Stefanova, S. Valentini, A note on the Identity Criteria

Abstract: In [Guarino] the notion of identity criteria is introduced in order to distinguish between predicates which carry an identity criteria and predicates which do not. We will show here that, under some very usual assumptions, every predicate carries an identity criteria and we will characterize its general shape.

S. Berardi, S. Valentini, Krivine Intuitionistic Proof of Classical Completeness for countable languages,

Abstract: In 1996, Krivine applied Friedman's A-translation in order to get a constructive version of Gödel Completeness result for first order classical logic. Such result is known to be intuitionistically underivable, but Krivine managed to constructively derive a weak form of it. In this paper, we want to analyze the ideas Krivine's remarkable result relies on, ideas which where somehow hidden by the heavy formal machinery used in the original proof. We show that the ideas in Krivine's proof can be used to intuitionistically derive crucial mathematical results, which were supposed to be purely classical up to now: the Ultrafilter Theorem in Boolean Algebra Theory, and the Maximal Ideal Theorem in Ring Theory.