24 found
Sort by:
  1. Thierry Coquand & Giovanni Sambin (forthcoming). Preface of Special Issue on Formal Topology. Annals of Pure and Applied Logic.
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Thierry Coquand (2013). About Goodmanʼs Theorem. 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)  
     
    My bibliography  
     
    Export citation  
  3. Andrej Bauer, Thierry Coquand, Giovanni Sambin & Peter M. Schuster (2012). Preface. Annals of Pure and Applied Logic 163 (2):85-86.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  4. Thierry Coquand, Erik Palmgren & Bas Spitters (2011). Metric Complements of Overt Closed Sets. 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 (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Stefano Berardi, Thierry Coquand & Susumu Hayashi (2010). Games with 1-Backtracking. 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)  
     
    My bibliography  
     
    Export citation  
  6. Thierry Coquand (2009). Space of Valuations. Annals of Pure and Applied Logic 157 (2):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)  
     
    My bibliography  
     
    Export citation  
  7. Thierry Coquand, Type Theory. Stanford Encyclopedia of Philosophy.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  8. Thierry Coquand & Henri Lombardi (2008). A Note on the Axiomatisation of Real Numbers. Mathematical Logic Quarterly 54 (3):224-228.
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. Thierry Coquand & L. Henri Lombardi (2008). A Note on the Axiomatisation of Real Numbers. 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 (3 more)  
     
    My bibliography  
     
    Export citation  
  10. Bernhard Banaschewski, Thierry Coquand & Giovanni Sambin (2006). Preface. Annals of Pure and Applied Logic 137 (1-3):1-2.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  11. Thierry Coquand & Bas Spitters (2005). A Constructive Proof of the Peter‐Weyl Theorem. 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)  
     
    My bibliography  
     
    Export citation  
  12. Thierry Coquand (2004). About Brouwer's Fan Theorem. Revue Internationale de Philosophie 230:483-489.
  13. Sara Negri, Jan von Plato & Thierry Coquand (2004). Proof-Theoretical Analysis of Order Relations. 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)  
     
    My bibliography  
     
    Export citation  
  14. 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  
  15. Thierry Coquand & Erik Palmgren (2002). Metric Boolean Algebras and Constructive Measure Theory. 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)  
     
    My bibliography  
     
    Export citation  
  16. Thierry Coquand & Erik Palmgren (2000). Intuitionistic Choice and Classical Logic. 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)  
     
    My bibliography  
     
    Export citation  
  17. Thierry Coquand, Sara Sadocco, Giovanni Sambin & Jan M. Smith (2000). Formal Topologies on the Set of First-Order Formulae. Journal of Symbolic Logic 65 (3):1183-1192.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  18. Thierry Coquand (1999). A Boolean Model of Ultrafilters. 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)  
     
    My bibliography  
     
    Export citation  
  19. Stefano Berardi, Marc Bezem & Thierry Coquand (1998). On the Computational Content of the Axiom of Choice. 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 (6 more)  
     
    My bibliography  
     
    Export citation  
  20. Thierry Coquand (1998). Two Applications of Boolean Models. 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)  
     
    My bibliography  
     
    Export citation  
  21. Thierry Coquand (1997). Minimal Invariant Spaces in Formal Topology. Journal of Symbolic Logic 62 (3):689-698.
  22. Thierry Coquand (1995). A Semantics of Evidence for Classical Arithmetic. Journal of Symbolic Logic 60 (1):325-337.
  23. Thierry Coquand (1992). An Intuitionistic Proof of Tychonoff's Theorem. Journal of Symbolic Logic 57 (1):28-32.