26 found
Order:
  1.  5
    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   29 citations  
  2.  22
    A Semantics of Evidence for Classical Arithmetic.Thierry Coquand - 1995 - Journal of Symbolic Logic 60 (1):325-337.
  3.  8
    Games with 1-Backtracking.Stefano Berardi, Thierry Coquand & Susumu Hayashi - 2010 - Annals of Pure and Applied Logic 161 (10):1254-1269.
    We associate with any game G another game, which is a variant of it, and which we call . Winning strategies for have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over , and vice versa. Through we can express in algorithmic form, as a recursive winning strategy, many common proofs of non-constructive Mathematics, namely exactly the theorems of the (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  4.  28
    On the Computational Content of the Axiom of Choice.Stefano Berardi, Marc Bezem & Thierry Coquand - 1998 - Journal of Symbolic Logic 63 (2):600-622.
    We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   7 citations  
  5.  9
    Intuitionistic Choice and Classical Logic.Thierry Coquand & Erik Palmgren - 2000 - Archive for Mathematical Logic 39 (1):53-74.
    . The effort in providing constructive and predicative meaning to non-constructive modes of reasoning has almost without exception been applied to theories with full classical logic [4]. In this paper we show how to combine unrestricted countable choice, induction on infinite well-founded trees and restricted classical logic in constructively given models. These models are sheaf models over a $\sigma$ -complete Boolean algebra, whose topologies are generated by finite or countable covering relations. By a judicious choice of the Boolean algebra we (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  6.  11
    Formal Topologies on the Set of First-Order Formulae.Thierry Coquand, Sara Sadocco, Giovanni Sambin & Jan M. Smith - 2000 - Journal of Symbolic Logic 65 (3):1183-1192.
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  7.  15
    An Intuitionistic Proof of Tychonoff's Theorem.Thierry Coquand - 1992 - Journal of Symbolic Logic 57 (1):28-32.
  8.  21
    Minimal Invariant Spaces in Formal Topology.Thierry Coquand - 1997 - Journal of Symbolic Logic 62 (3):689-698.
  9.  2
    Proof-Theoretical Analysis of Order Relations.Sara Negri, Jan von Plato & Thierry Coquand - 2004 - Archive for Mathematical Logic 43 (3):297-309.
    A proof-theoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contraction-free sequent calculus. Among the results obtained are proof-theoretical formulations of conservativity theorems corresponding to Szpilrajn’s theorem on the extension of a partial order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is shown by giving terminating methods of proof-search.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  10.  23
    Metric Boolean Algebras and Constructive Measure Theory.Thierry Coquand & Erik Palmgren - 2002 - Archive for Mathematical Logic 41 (7):687-704.
    This work concerns constructive aspects of measure theory. By considering metric completions of Boolean algebras – an approach first suggested by Kolmogorov – one can give a very simple construction of e.g. the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such Boolean algebras. We analyse next the notion of Borel subsets. We show that the algebra of such subsets can be characterised in a pointfree and constructive way by (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  11.  2
    Space of Valuations.Thierry Coquand - 2009 - Annals of Pure and Applied Logic 157 (2-3):97-109.
    The general framework of this paper is a reformulation of Hilbert’s program using the theory of locales, also known as formal or point-free topology [P.T. Johnstone, Stone Spaces, in: Cambridge Studies in Advanced Mathematics, vol. 3, 1982; Th. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic 124 71–106; G. Sambin, Intuitionistic formal spaces–a first communication, in: D. Skordev , Mathematical Logic and its Applications, Plenum, New York, 1987, pp. 187–204]. Formal topology presents a (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  12.  11
    Two Applications of Boolean Models.Thierry Coquand - 1998 - Archive for Mathematical Logic 37 (3):143-147.
    Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  13.  16
    A Note on the Axiomatisation of Real Numbers.Coquand Thierry & Lombardi L. Henri - 2008 - Mathematical Logic Quarterly 54 (3):224-228.
    Is it possible to give an abstract characterisation of constructive real numbers? A condition should be that all axioms are valid for Dedekind reals in any topos, or for constructive reals in Bishop mathematics. We present here a possible first-order axiomatisation of real numbers, which becomes complete if one adds the law of excluded middle. As an application of the forcing relation defined in [3, 2], we give a proof that the formula which specifies the maximum function is not provable (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  14. About Brouwer's Fan Theorem.Thierry Coquand - 2004 - Revue Internationale de Philosophie 230:483-489.
  15.  5
    A Boolean Model of Ultrafilters.Thierry Coquand - 1999 - Annals of Pure and Applied Logic 99 (1-3):231-239.
    We introduce the notion of Boolean measure algebra. It can be described shortly using some standard notations and terminology. If B is any Boolean algebra, let BN denote the algebra of sequences , xn B. Let us write pk BN the sequence such that pk = 1 if i K and Pk = 0 if k < i. If x B, denote by x* BN the constant sequence x* = . We define a Boolean measure algebra to be a Boolean (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  16.  4
    Some Remarks About Normal Rings.Henri Lombardi & Thierry Coquand - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter. pp. 141-150.
    Direct download  
     
    Export citation  
     
    My bibliography  
  17.  10
    A Constructive Proof of the Peter‐Weyl Theorem.Thierry Coquand & Bas Spitters - 2005 - Mathematical Logic Quarterly 51 (4):351-359.
    We present a new and constructive proof of the Peter-Weyl theorem on the representations of compact groups. We use the Gelfand representation theorem for commutative C*-algebras to give a proof which may be seen as a direct generalization of Burnside's algorithm [3]. This algorithm computes the characters of a finite group. We use this proof as a basis for a constructive proof in the style of Bishop. In fact, the present theory of compact groups may be seen as a natural (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  18.  8
    About Goodmanʼs Theorem.Thierry Coquand - 2013 - Annals of Pure and Applied Logic 164 (4):437-442.
    We present a proof of Goodmanʼs Theorem, which is a variation of the proof of Renaldel de Lavalette [9]. This proof uses in an essential way possibly divergent computations for proving a result which mentions systems involving only terminating computations. Our proof is carried out in a constructive metalanguage. This involves implicitly a covering relation over arbitrary posets in formal topology, which occurs in forcing in set theory in a classical framework, but can also be defined constructively.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  19. Preface of Special Issue on Formal Topology.Thierry Coquand & Giovanni Sambin - forthcoming - Annals of Pure and Applied Logic.
  20.  4
    Metric Complements of Overt Closed Sets.Thierry Coquand, Erik Palmgren & Bas Spitters - 2011 - Mathematical Logic Quarterly 57 (4):373-378.
    We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop-compact. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  21.  9
    Type Theory.Thierry Coquand - 2008 - Stanford Encyclopedia of Philosophy.
    Direct download  
     
    Export citation  
     
    My bibliography  
  22. A Note on the Axiomatisation of Real Numbers.Thierry Coquand & Henri Lombardi - 2008 - Mathematical Logic Quarterly 54 (3):224-228.
     
    Export citation  
     
    My bibliography  
  23.  2
    Preface.Andrej Bauer, Thierry Coquand, Giovanni Sambin & Peter M. Schuster - 2012 - Annals of Pure and Applied Logic 163 (2):85-86.
  24.  1
    Preface.Bernhard Banaschewski, Thierry Coquand & Giovanni Sambin - 2006 - Annals of Pure and Applied Logic 137 (1-3):1-2.
  25. Formal Topologies on the Set of First-Order Formulae.Thierry Coquand, Sara Sadocco, Giovanni Sambin & Jan Smith - 2000 - Journal of Symbolic Logic 65 (3):1183-1192.
    Direct download  
     
    Export citation  
     
    My bibliography  
  26. Preface.Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin & Peter Schuster - 2016 - Annals of Pure and Applied Logic 167 (9):725.