{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:09Z","timestamp":1753894389262,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T00:00:00Z","timestamp":1659398400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We define a point-free construction of real exponentiation and logarithms,\ni.e.\\ we construct the maps $\\exp\\colon (0, \\infty)\\times \\mathbb{R}\n\\rightarrow \\!(0,\\infty),\\, (x, \\zeta) \\mapsto x^\\zeta$ and $\\log\\colon\n(1,\\infty)\\times (0, \\infty) \\rightarrow\\mathbb{R},\\, (b, y) \\mapsto\n\\log_b(y)$, and we develop familiar algebraic rules for them. The point-free\napproach is constructive, and defines the points of a space as models of a\ngeometric theory, rather than as elements of a set - in particular, this allows\ngeometric constructions to be applied to points living in toposes other than\nSet. Our geometric development includes new lifting and gluing techniques in\npoint-free topology, which highlight how properties of $\\mathbb{Q}$ determine\nproperties of real exponentiation.\n  This work is motivated by our broader research programme of developing a\nversion of adelic geometry via topos theory. In particular, we wish to\nconstruct the classifying topos of places of $\\mathbb{Q}$, which will provide a\ngeometric perspective into the subtle relationship between $\\mathbb{R}$ and\n$\\mathbb{Q}_p$, a question of longstanding number-theoretic interest.<\/jats:p>","DOI":"10.46298\/lmcs-18(3:15)2022","type":"journal-article","created":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T21:09:51Z","timestamp":1659474591000},"source":"Crossref","is-referenced-by-count":0,"title":["Point-free Construction of Real Exponentiation"],"prefix":"10.46298","volume":"Volume 18, Issue 3","author":[{"given":"Ming","family":"Ng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Vickers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2022,8,2]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9879\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9879\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:19:44Z","timestamp":1687292384000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(3:15)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2104.00162v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2104.00162v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2104.00162","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2104.00162","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,8,2]]},"article-number":"7325"}}