Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Introduction Read chapter Read first chapter

2019 | OriginalPaper | Chapter

6. Semantics and Soundness

Authors : Patrick Schultz, David I. Spivak

Published in: Temporal Type Theory

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In this chapter, we prove that the temporal type theory developed in Chaps. 4 and 5 is sound in the topos \(\mathcal {B}\). To do so, we begin in Sect. 6.1 by recalling the Kripke–Joyal semantics by which to interpret type-theoretic formulas in the topos \(\mathcal {B}\). Then in Sect. 6.3 we discuss the sheaf of real numbers and Time. We then proceed to our main goal: proving that our type signature—i.e., the one atomic predicate symbol and the ten axioms presented in Chap. 5—are sound in \(\mathcal {B}\). This is done in Sect. 6.5, which begins with a Table 6.2 summarizing the type signature.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Axiomatics
next chapter Local Numeric Types and Derivatives
Footnotes
1
Recall from Definition 3.​5 that a wavy arrow \(\langle r,s\rangle \colon \ell ^{\prime }\rightsquigarrow \ell \) in \(\mathbb {I\hspace {1.1pt} R}_{/\rhd }^{\mathrm {op}}\) is an interval inclusion that is strict on both sides, i.e., where r > 0 and s > 0.
 
2
We will see in Proposition 7.​12 that there is also containment of types https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-00704-1_6/457670_1_En_6_IEq226_HTML.gif .
 
Literature
[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-3
[MM92]
MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, New York (1992). ISBN:0387977104
Metadata
Title
Semantics and Soundness
Authors
Patrick Schultz
David I. Spivak
Copyright Year
2019
Book
Temporal Type Theory

Print ISBN: 978-3-030-00703-4

Electronic ISBN: 978-3-030-00704-1

Copyright Year: 2019

DOI
https://doi.org/10.1007/978-3-030-00704-1_6

Premium Partner

    Image Credits