26 found
Order:
  1.  41
    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 (5 more)  
     
    Export citation  
     
    Bookmark   44 citations  
  2.  73
    The modal logic of provability. The sequential approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.
  3.  44
    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 (2 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  4.  33
    The problem of the formalization of constructive topology.Silvio Valentini - 2005 - Archive for Mathematical Logic 44 (1):115-129.
    Abstract.Formal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in [CSSV]. However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  5.  81
    A structural investigation on formal topology: coreflection of formal covers and exponentiability.Maria 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 (6 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  6.  72
    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 (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  7.  49
    (1 other version)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 (6 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  8.  38
    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 (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  9.  83
    Tychonoff's theorem in the framework of formal topologies.Sara Negri & Silvio Valentini - 1997 - Journal of Symbolic Logic 62 (4):1315-1332.
  10.  14
    Constructive characterizations of bar subsets.Silvio Valentini - 2007 - Annals of Pure and Applied Logic 145 (3):368-378.
  11.  37
    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 (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  12.  17
    (1 other version)The judgement calculus for intuitionistic linear logic: Proof theory and semantics.Silvio Valentini - 1992 - Mathematical Logic Quarterly 38 (1):39-58.
  13.  21
    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 (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  14. 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 (5 more)  
     
    Export citation  
     
    Bookmark  
  15.  39
    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 (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  16.  33
    Topological characterization of Scott domains.Giovanni Sambin & Silvio Valentini - forthcoming - Archive for Mathematical Logic.
    Direct download  
     
    Export citation  
     
    Bookmark  
  17.  24
    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  
     
    Export citation  
     
    Bookmark  
  18.  22
    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  
     
    Export citation  
     
    Bookmark  
  19.  33
    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 (2 more)  
     
    Export citation  
     
    Bookmark  
  20.  47
    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 (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  21.  30
    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  
     
    Export citation  
     
    Bookmark   1 citation  
  22.  10
    Generalising the fan theorem.Silvio Valentini - 2017 - Mathematical Logic Quarterly 63 (1-2):85-93.
    We characterise the collections of infinite binary sequences that, when barred by a set of finite binary sequences, are also barred by a finite subset of such a set.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  23.  22
    Independence results in formal topology.Silvio Valentini - 2012 - Annals of Pure and Applied Logic 163 (2):151-156.
  24.  23
    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 (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  25.  17
    The modal logic of consistency assertions of peano arithmetic.Silvio Valentini - 1983 - Mathematical Logic Quarterly 29 (1):25-32.
  26.  58
    The modal logic of provability: Cut-elimination. [REVIEW]Silvio Valentini - 1983 - Journal of Philosophical Logic 12 (4):471 - 476.