Chapter

PREDICATIVE EXPONENTIATION OF LOCALLY COMPACT FORMAL TOPOLOGIES OVER INDUCTIVELY GENERATED TOPOLOGIES

Maria Emilia Maietti

in From Sets and Types to Topology and Analysis

Published in print October 2005 | ISBN: 9780198566519
Published online September 2007 | e-ISBN: 9780191713927 | DOI: https://dx.doi.org/10.1093/acprof:oso/9780198566519.003.0013

Series: Oxford Logic Guides

 PREDICATIVE EXPONENTIATION OF LOCALLY COMPACT FORMAL TOPOLOGIES OVER INDUCTIVELY GENERATED TOPOLOGIES

Show Summary Details

Preview

Martin Hyland first classified the exponentiable locales as the locally compact ones. This chapter proves the counterpart of Hyland's result for inductively generated formal topologies. More precisely, by adapting Hyland's proofs to the context of formal topology, it proves that locally compact formal covers are the exponentiable objects in the category of inductively generated formal covers. Then, it deduces the analogous result for inductively generated formal topologies (that is, formal topologies with a unary positivity predicate). This demonstrates once more how impredicative reasoning can be unwound predicatively with great patience, but with the benefit of a quite explicit proof.

Keywords: exponentiation; locales; formal topology; formal covers; inductively generated formal topologies; Martin Hyland

Chapter.  14409 words. 

Subjects: Logic

Full text: subscription required

How to subscribe Recommend to my Librarian

Buy this work at Oxford University Press »

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.