Logical Preliminaries

  • Patrick Schultz
  • David I. Spivak
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 29)


In this chapter, we transition from an external point of view to an internal one. In Chap. 2 we defined the interval domain \(\mathbb {I\hspace {1.1pt} R}\), and in Chap. 3 we defined a quotient \(\mathcal {B}\cong \mathsf {Shv}(S_{\mathbb {I\hspace {1.1pt} R}/\rhd })\) of its topos of sheaves. A main goal of this book is to define a temporal type theory—including one atomic predicate and ten axioms—that has semantics in \(\mathcal {B}\); we do this in Chap. 5. In the present chapter, we attempt to provide the reader with a self-contained account of the sort of type theory and logic we will be using, as well as some important concepts definable therein.


  1. [BT09]
    Bauer, A., Taylor, P.: The Dedekind reals in abstract Stone duality. Math. Struct. Comput. Sci. 19(4), 757–838 (2009). ISSN:0960-1295. MathSciNetCrossRefGoogle Scholar
  2. [CH88]
    Coquand, T., Huet, G.: The calculus of constructions. Inform. Comput. 76(2–3), 95–120 (1988). ISSN:0890-5401. MathSciNetCrossRefGoogle Scholar
  3. [Ded72]
    Dedekind, R.: Stetigkeit und irrationale Zahlen. F. Vieweg und sohn (1872)Google Scholar
  4. [Gol11]
    Goldsztejn, A.: Modal intervals revisited, part 1: a generalized interval natural extension. Reliab. Comput. 16, 130–183 (2011). ISSN:1573–1340Google Scholar
  5. [Jac99]
    Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141, pp. xviii+ 760. North-Holland, Amsterdam (1999). ISBN:0-444-50170-3Google Scholar
  6. [Joh02]
    Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford Logic Guides, vol. 43, pp. xxii+ 468+ 71. New York: The Clarendon Press/Oxford University Press (2002). ISBN:0-19-853425-6Google Scholar
  7. [Kau80]
    Kaucher, E.: Interval analysis in the extended interval space IR. In: Fundamentals of Numerical Computation (Computer-Oriented Numerical Analysis), pp. 33–49. Springer, Berlin (1980)Google Scholar
  8. [LS88]
    Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7, pp. x+ 293. Reprint of the 1986 original. Cambridge University Press, Cambridge (1988). ISBN:0-521-35653-9Google Scholar
  9. [Mai05]
    Maietti, M.E.: Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Struct. Comput. Sci. 15(6), 1089–1149 (2005). ISSN:0960-1295. MathSciNetCrossRefGoogle Scholar
  10. [MM92]
    MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, New York (1992). ISBN:0387977104Google Scholar
  11. [Sai+14]
    Sainz, M.A., et al.: Modal Interval Analysis. Lecture Notes in Mathematics. New Tools for Numerical Information, vol. 2091, pp. xvi+ 316. Springer, Cham (2014). ISBN:978-3-319-01720-4.
  12. [Str05]
    Streicher, T.: Universes in toposes. In: From Sets and Types to Topology and Analysis. Oxford Logic Guides, vol. 48, pp. 78–90. Oxford Univ. Press, Oxford (2005). CrossRefGoogle Scholar
  13. [Voe+13]
    Voevodsky, V., et al.: Homotopy type theory: Univalent foundations of mathematics. In: Institute for Advanced Study (Princeton). The Univalent Foundations Program (2013)Google Scholar

Copyright information

© The Author(s) 2019

Authors and Affiliations

  • Patrick Schultz
    • 1
  • David I. Spivak
    • 1
  1. 1.Massachusetts Institute of TechnologyCambridgeUSA

Personalised recommendations