26 found
Sort by:
  1. Giovanni Sambin & Silvio Valentini (forthcoming). Topological Characterization of Scott Domains. Archive for Mathematical Logic.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Silvio Valentini (2013). Cantor Theorem and Friends, in Logical Form. Annals of Pure and Applied Logic 164 (4):502-508.
    We prove a generalization of the hyper-game theorem by using an abstract version of inductively generated formal topology. As applications we show proofs for Cantor theorem, uncountability of the set of functions from N to N and Gödel theorem which use no diagonal argument.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Giovanni Boniolo & Silvio Valentini (2012). Objects: A Study in Kantian Formal Epistemology. Notre Dame Journal of Formal Logic 53 (4):457-478.
    We propose a formal representation of objects , those being mathematical or empirical objects. The powerful framework inside which we represent them in a unique and coherent way is grounded, on the formal side, in a logical approach with a direct mathematical semantics in the well-established field of constructive topology, and, on the philosophical side, in a neo-Kantian perspective emphasizing the knowing subject’s role, which is constructive for the mathematical objects and constitutive for the empirical ones.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  4. Silvio Valentini (2012). Independence Results in Formal Topology. Annals of Pure and Applied Logic 163 (2):151-156.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. Milena Stefanova & Silvio Valentini (2011). Spatiality and Classical Logic. Mathematical Logic Quarterly 57 (4):432-440.
    In this short note we show that any proof of a general spatiality theorem for inductively generated formal topologies requires full classical logic. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Giovanni Boniolo & Silvio Valentini (2008). Vagueness, Kant and Topology: A Study of Formal Epistemology. Journal of Philosophical Logic 37 (2):141 - 168.
    In this paper we propose an approach to vagueness characterised by two features. The first one is philosophical: we move along a Kantian path emphasizing the knowing subject’s conceptual apparatus. The second one is formal: to face vagueness, and our philosophical view on it, we propose to use topology and formal topology. We show that the Kantian and the topological features joined together allow us an atypical, but promising, way of considering vagueness.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  7. Silvio Valentini (2007). Constructive Characterizations of Bar Subsets. Annals of Pure and Applied Logic 145 (3):368-378.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  8. Silvio Valentini (2006). Every Countably Presented Formal Topology is Spatial, Classically. Journal of Symbolic Logic 71 (2):491-500.
    By using some classical reasoning we show that any countably presented formal topology, namely, a formal topology with a countable axiom set, is spatial.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  9. Silvio Valentini (2005). The Problem of the Formalization of Constructive Topology. Archive for Mathematical Logic 44 (1):115-129.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  10. Stefano Berardi & Silvio Valentini (2004). Krivine's Intuitionistic Proof of Classical Completeness (for Countable Languages). Annals of Pure and Applied Logic 129 (1-3):93-106.
    In 1996, Krivine applied Friedman's A-translation in order to get an intuitionistic version of Gödel completeness result for first-order classical logic and countable languages and models. Such a result is known to be intuitionistically underivable 559), but Krivine was able to derive intuitionistically a weak form of it, namely, he proved that every consistent classical theory has a model. In this paper, we want to analyze the ideas Krivine's remarkable result relies on, ideas which where somehow hidden by the heavy (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  11. Maria Emilia Maietti & Silvio Valentini (2004). A Structural Investigation on Formal Topology: Coreflection of Formal Covers and Exponentiability. Journal of Symbolic Logic 69 (4):967-1005.
    We present and study the category of formal topologies and some of its variants. Two main results are proven. The first is that, for any inductively generated formal cover, there exists a formal topology whose cover extends in the minimal way the given one. This result is obtained by enhancing the method for the inductive generation of the cover relation by adding a coinductive generation of the positivity predicate. Categorically, this result can be rephrased by saying that inductively generated formal (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  12. Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini (2003). Inductively Generated Formal Topologies. Annals of Pure and Applied Logic 124 (1-3):71-106.
    Formal topology aims at developing general topology in 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 expressible 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 (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  13. Silvio Valentini (2002). Extensionality Versus Constructivity. Mathematical Logic Quarterly 48 (2):179-187.
    We analyze some extensions of Martin-Löf 's constructive type theory by means of extensional set constructors and we show that often the most natural requirements over them lead to classical logic or even to inconsistency.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  14. Silvio Valentini (2002). On the Formal Points of the Formal Topology of the Binary Tree. Archive for Mathematical Logic 41 (7):603-618.
    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 (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  15. Silvio Valentini (2001). An Elementary Proof of Strong Normalization for Intersection Types. Archive for Mathematical Logic 40 (7):475-488.
    We provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set of strongly normalizing terms (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  16. Maria Emilia Maietti & Silvio Valentini (1999). Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory? Mathematical Logic Quarterly 45 (4):521-532.
    In this paper we analyze an extension of Martin-Löf s intensional set theory by means of a set contructor P such that the elements of P are the subsets of the set S. Since it seems natural to require some kind of extensionality on the equality among subsets, it turns out that such an extension cannot be constructive. In fact we will prove that this extension is classic, that is “ true holds for any proposition A.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  17. Sara Negri & Silvio Valentini (1997). Tychonoff's Theorem in the Framework of Formal Topologies. Journal of Symbolic Logic 62 (4):1315-1332.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  18. Dario Maguolo & Silvio Valentini (1996). An Intuitionistic Version of Cantor's Theorem. Mathematical Logic Quarterly 42 (1):446-448.
    An intuitionistic version of Cantor's theorem, which shows that there is no surjective function from the type of the natural numbers N into the type N → N of the functions from N into N, is proved within Martin-Löf's Intuitionistic Type Theory with the universe of the small types.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  19. Silvio Valentini (1996). Decidability in Intuitionistic Type Theory is Functionally Decidable. Mathematical Logic Quarterly 42 (1):300-304.
    In this paper we show that the usual intuitionistic characterization of the decidability of the propositional function B prop [x : A], i. e. to require that the predicate ∨ ¬ B) is provable, is equivalent, when working within the framework of Martin-Löf's Intuitionistic Type Theory, to require that there exists a decision function ψ: A → Boole such that = Booletrue) ↔ B). Since we will also show that the proposition x = Booletrue [x: Boole] is decidable, we can (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  20. Silvio Valentini (1994). Representation Theorems for Quantales. Mathematical Logic Quarterly 40 (2):182-190.
    In this paper we prove that any quantale Q is 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 Linear Logic using relations.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  21. Ugo Solitro & Silvio Valentini (1993). Local Computation in Linear Logic. Mathematical Logic Quarterly 39 (1):201-212.
    This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic . A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  22. Silvio Valentini (1993). A Proof of the Normal Form Theorem for the Closed Terms of Girard's System F by Means of Computability. Mathematical Logic Quarterly 39 (1):539-544.
    In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be well founded. (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  23. Silvio Valentini (1992). The Judgement Calculus for Intuitionistic Linear Logic: Proof Theory and Semantics. Mathematical Logic Quarterly 38 (1):39-58.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  24. Silvio Valentini (1983). The Modal Logic of Provability: Cut-Elimination. [REVIEW] Journal of Philosophical Logic 12 (4):471 - 476.
  25. Silvio Valentini (1983). The Modal Logic of Consistency Assertions of Peano Arithmetic. Mathematical Logic Quarterly 29 (1):25-32.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  26. Giovanni Sambin & Silvio Valentini (1982). The Modal Logic of Provability. The Sequential Approach. Journal of Philosophical Logic 11 (3):311 - 342.