{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:18Z","timestamp":1761611178755},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":6036,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1997,9]]},"abstract":"A standard result in topological dynamics is the existence of minimal subsystem. It is a direct consequence of Zorn's lemma: given a compact topological space X<\/jats:italic> with a map f<\/jats:italic>: X<\/jats:italic>\u2192X<\/jats:italic>, the set of compact non empty subspaces K<\/jats:italic> of X<\/jats:italic> such that f(K)<\/jats:italic> \u2286 K<\/jats:italic> ordered by inclusion is inductive, and hence has minimal elements. It is natural to ask for a point-free (or formal) formulation of this statement. In a previous work [3], we gave such a formulation for a quite special instance of this statement, which is used in proving a purely combinatorial theorem (van de Waerden's theorem on arithmetical progression).<\/jats:p>In this paper, we extend our analysis to the case where X<\/jats:italic> is a boolean space, that is compact totally disconnected. In such a case, we give a point-free formulation of the existence of a minimal subspace for any continuous map f<\/jats:italic>: X<\/jats:italic>\u2192X<\/jats:italic>. We show that such minimal subspaces can be described as points<\/jats:italic> of a suitable formal topology, and the \u201cexistence\u201d of such points become the problem of the consistency of the theory describing a generic point of this space. We show the consistency of this theory by building effectively and algebraically a topological model. As an application, we get a new, purely algebraic proof, of the minimal property of [3]. We show then in detail how this property can be used to give a proof of (a special case of) van der Waerden's theorem on arithmetical progression, that is \u201csimilar in structure\u201d to the topological proof [6, 8], but which uses a simple algebraic remark (Proposition 1) instead of Zorn's lemma. A last section tries to place this work in a wider context, as a reformulation of Hilbert's method of introduction\/elimination of ideal elements.<\/jats:p>","DOI":"10.2307\/2275567","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T23:01:58Z","timestamp":1146956518000},"page":"689-698","source":"Crossref","is-referenced-by-count":5,"title":["Minimal invariant spaces in formal topology"],"prefix":"10.1017","volume":"62","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200015978_ref013","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1986-0833712-3"},{"key":"S0022481200015978_ref001","first-page":"6","volume":"46","author":"Boileau","journal-title":"La logique des topos"},{"key":"S0022481200015978_ref016","unstructured":"van der Meiden W. , Point-free carrier space topology for commutative Banach algebra, Ph.D. thesis , Eindhoven, 1967."},{"key":"S0022481200015978_ref012","volume-title":"Notes on constructive mathematics","author":"Martin-L\u00f6f","year":"1970"},{"key":"S0022481200015978_ref002","unstructured":"Coquand Th. , A formal space of ultrafilter, 1994, manuscript."},{"key":"S0022481200015978_ref004","first-page":"467","article-title":"Notes on Gelfand's theory","volume":"31","author":"de Bruijn","year":"1968","journal-title":"Indigationes"},{"key":"S0022481200015978_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF02790008"},{"key":"S0022481200015978_ref005","first-page":"107","volume-title":"The L. E. J. Brouwer centenary symposium","author":"Fourman","year":"1982"},{"key":"S0022481200015978_ref007","volume-title":"Proof-theory and logical complexity","author":"Girard","year":"1987"},{"key":"S0022481200015978_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448445"},{"key":"S0022481200015978_ref010","volume-title":"Stone spaces","author":"Johnstone","year":"1981"},{"key":"S0022481200015978_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(94)00148-0"},{"key":"S0022481200015978_ref011","first-page":"37","volume":"24","author":"Lorenzen","year":"1959","journal-title":"Constructive definition of certain sets of numbers"},{"key":"S0022481200015978_ref015","first-page":"863","volume":"60","author":"Sambin","year":"1995","journal-title":"Pretopologies and completeness proofs"},{"key":"S0022481200015978_ref008","volume-title":"Ramsey theory","author":"Graham","year":"1980"},{"key":"S0022481200015978_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(91)90082-I"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200015978","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T20:25:06Z","timestamp":1557606306000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200015978\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,9]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,9]]}},"alternative-id":["S0022481200015978"],"URL":"https:\/\/doi.org\/10.2307\/2275567","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,9]]}}}