{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T07:03:25Z","timestamp":1697439805556},"reference-count":10,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":8046,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1992,3]]},"abstract":"<jats:p>Tychonoff's theorem states that a product of compact spaces is compact. In [3], P. Johnstone presents a proof of Tychonoff's theorem in a \u201clocalic\u201d framework. The surprise is that the point-free formulation of Tychonoff's theorem is provable <jats:italic>without<\/jats:italic> the axiom of choice, whereas in the usual formulation it is equivalent to the axiom of choice (see Kelley [5]).<\/jats:p><jats:p>The proof given in [3], however, is classical and seems to use the replacement axiom of Zermelo-Fraenkel. The aim of this paper is to present what we believe to be a more direct proof, which is intuitionistic and can be proved using as primitive only the notion of inductive definition, as it is for instance presented in Martin-L\u00f6f [6]. One main point of the paper is to show that the theory of locales can be developed rather naturally in the framework of inductive definitions. We think that our arguments can be presented in the constructive set theory of Aczel [2].<\/jats:p><jats:p>The paper is organized as follows. In \u00a71 we show the argument in the case of a product of two spaces. This proof has a direct generalisation to the case of a product over a set with a decidable equality.<\/jats:p><jats:p><jats:bold>\u00a71. Product of two spaces<\/jats:bold>. We first recall a possible definition of a point-free space (see Johnstone [3] or Vickers [10]). It is a poset (<jats:italic>X<\/jats:italic>, \u2264), together with a meet operation <jats:italic>ab<\/jats:italic>, written multiplicatively, and, for each <jats:italic>a<\/jats:italic> \u2208 <jats:italic>X<\/jats:italic>, a set <jats:bold>Cov<\/jats:bold>(<jats:italic>a<\/jats:italic>) of subsets of {<jats:italic>x<\/jats:italic> \u2208 <jats:italic>X<\/jats:italic> \u2223 <jats:italic>x<\/jats:italic> \u2264 <jats:italic>a<\/jats:italic>}. We ask that if <jats:italic>M<\/jats:italic> \u2208 <jats:bold>Cov<\/jats:bold>(<jats:italic>a<\/jats:italic>) and <jats:italic>b<\/jats:italic> \u2264 <jats:italic>a<\/jats:italic>, then {<jats:italic>bs<\/jats:italic> \u2208 <jats:italic>s<\/jats:italic> \u2208 <jats:italic>M<\/jats:italic>} \u2208 <jats:bold>Cov<\/jats:bold>(<jats:italic>b<\/jats:italic>). This property of <jats:bold>Cov<\/jats:bold> will be called the <jats:italic>axiom of covering<\/jats:italic>. The elements of <jats:bold>Cov<\/jats:bold>(<jats:italic>u<\/jats:italic>) are called <jats:italic>basic covers<\/jats:italic> of <jats:italic>u<\/jats:italic> \u2208 <jats:italic>X<\/jats:italic>.<\/jats:p>","DOI":"10.2307\/2275174","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:43:45Z","timestamp":1146955425000},"page":"28-32","source":"Crossref","is-referenced-by-count":12,"title":["An intuitionistic proof of Tychonoff's theorem"],"prefix":"10.1017","volume":"57","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120002315X_ref008","volume-title":"Choice sequences: a chapter of intuitionistic mathematics","author":"Troelstra","year":"1977"},{"key":"S002248120002315X_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"S002248120002315X_ref005","doi-asserted-by":"publisher","DOI":"10.4064\/fm-37-1-75-76"},{"key":"S002248120002315X_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"S002248120002315X_ref010","volume-title":"Topology via logic","volume":"5","author":"Vickers","year":"1989"},{"key":"S002248120002315X_ref004","doi-asserted-by":"crossref","unstructured":"Johnstone P. J. and Vickers S. , Preframe presentations present, preprint, 1990.","DOI":"10.1007\/BFb0084221"},{"key":"S002248120002315X_ref003","volume-title":"Stone spaces","author":"Johnstone","year":"1982"},{"key":"S002248120002315X_ref009","unstructured":"Vermeulen J. J. C. , Tychonoff's theorem in a topos, preprint, 1990."},{"key":"S002248120002315X_ref002","first-page":"17","volume-title":"Logic, methodology and philosophy of science","volume":"VII","author":"Aczel","year":"1986"},{"key":"S002248120002315X_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0897-3_12"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120002315X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T22:32:38Z","timestamp":1558045958000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120002315X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["S002248120002315X"],"URL":"https:\/\/doi.org\/10.2307\/2275174","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}