26 found
Order:
  1.  4
    Inductively Generated Formal Topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - 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)  
     
    Export citation  
     
    My bibliography   25 citations  
  2.  10
    The Problem of the Formalization of Constructive Topology.Silvio Valentini - 2005 - Archive for Mathematical Logic 44 (1):115-129.
  3.  73
    Vagueness, Kant and Topology: A Study of Formal Epistemology.Giovanni Boniolo & Silvio Valentini - 2008 - 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)  
     
    Export citation  
     
    My bibliography  
  4.  30
    The Modal Logic of Provability. The Sequential Approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.
  5.  3
    A Structural Investigation on Formal Topology: Coreflection of Formal Covers and Exponentiability.Maria Emilia Maietti & Silvio Valentini - 2004 - 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 (5 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  6.  23
    The Modal Logic of Provability: Cut-Elimination. [REVIEW]Silvio Valentini - 1983 - Journal of Philosophical Logic 12 (4):471 - 476.
  7.  23
    On the Formal Points of the Formal Topology of the Binary Tree.Silvio Valentini - 2002 - 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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  8. Objects: A Study in Kantian Formal Epistemology.Giovanni Boniolo & Silvio Valentini - 2012 - 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 (4 more)  
     
    Export citation  
     
    My bibliography  
  9.  8
    Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?Maria Emilia Maietti & Silvio Valentini - 1999 - 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.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  10.  13
    Every Countably Presented Formal Topology is Spatial, Classically.Silvio Valentini - 2006 - 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 (5 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  11.  7
    Tychonoff's Theorem in the Framework of Formal Topologies.Sara Negri & Silvio Valentini - 1997 - Journal of Symbolic Logic 62 (4):1315-1332.
  12.  2
    Krivine's Intuitionistic Proof of Classical Completeness.Stefano Berardi & Silvio Valentini - 2004 - 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)  
     
    Export citation  
     
    My bibliography   2 citations  
  13.  14
    The Judgement Calculus for Intuitionistic Linear Logic: Proof Theory and Semantics.Silvio Valentini - 1992 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 38 (1):39-58.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  14.  1
    Constructive Characterizations of Bar Subsets.Silvio Valentini - 2007 - Annals of Pure and Applied Logic 145 (3):368-378.
  15.  13
    An Intuitionistic Version of Cantor's Theorem.Dario Maguolo & Silvio Valentini - 1996 - 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.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  16.  9
    Decidability in Intuitionistic Type Theory is Functionally Decidable.Silvio Valentini - 1996 - 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 (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  17.  15
    Topological Characterization of Scott Domains.Giovanni Sambin & Silvio Valentini - forthcoming - Archive for Mathematical Logic.
    Direct download  
     
    Export citation  
     
    My bibliography  
  18.  3
    Representation Theorems for Quantales.Silvio Valentini - 1994 - 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.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  19.  1
    The Judgement Calculus for Intuitionistic Linear Logic: Proof Theory and Semantics.Silvio Valentini - 1992 - Mathematical Logic Quarterly 38 (1):39-58.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  20.  10
    Cantor Theorem and Friends, in Logical Form.Silvio Valentini - 2013 - 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)  
     
    Export citation  
     
    My bibliography  
  21.  8
    Extensionality Versus Constructivity.Silvio Valentini - 2002 - 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.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  22.  6
    A Proof of the Normal Form Theorem for the Closed Terms of Girard's System F by Means of Computability.Silvio Valentini - 1993 - 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. (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  23.  3
    Independence Results in Formal Topology.Silvio Valentini - 2012 - Annals of Pure and Applied Logic 163 (2):151-156.
  24.  5
    Local Computation in Linear Logic.Ugo Solitro & Silvio Valentini - 1993 - 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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  25.  3
    The Modal Logic of Consistency Assertions of Peano Arithmetic.Silvio Valentini - 1983 - Mathematical Logic Quarterly 29 (1):25-32.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  26.  2
    Spatiality and Classical Logic.Milena Stefanova & Silvio Valentini - 2011 - 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.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography