A comparison of type theory with set theory
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985955%3A_____%2F19%3A00511657" target="_blank" >RIV/67985955:_____/19:00511657 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-030-15655-8_12" target="_blank" >http://dx.doi.org/10.1007/978-3-030-15655-8_12</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-15655-8_12" target="_blank" >10.1007/978-3-030-15655-8_12</a>
Alternative languages
Result language
angličtina
Original language name
A comparison of type theory with set theory
Original language description
This paper discusses some of the ways in which Martin-Löf type theory differs from set theory. The discussion concentrates on conceptual, rather than technical, differences. It revolves around four topics: sets versus types, syntax, functions, and identity. The difference between sets and types is spelt out as the difference between unified pluralities and kinds, or sorts. A detailed comparison is then offered of the syntax of the two languages. Emphasis is put on the distinction between proposition and judgement, drawn by type theory, but not by set theory. Unlike set theory, type theory treats the notion of function as primitive. It is shown that certain inconveniences pertaining to function application that afflicts the set-theoretical account of functions are thus avoided. Finally, the distinction, drawn in type theory, between judgemental and propositional identity is discussed. It is argued that the criterion of identity for a domain cannot be formulated in terms of propositional identity. It follows that the axiom of extensionality cannot be taken as a statement of the criterion of identity for sets.
Czech name
—
Czech description
—
Classification
Type
C - Chapter in a specialist book
CEP classification
—
OECD FORD branch
60301 - Philosophy, History and Philosophy of science and technology
Result continuities
Project
<a href="/en/project/GJ17-18344Y" target="_blank" >GJ17-18344Y: A logico-philosophical analysis of the notion of identity</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Book/collection name
Reflections on the Foundations of Mathematics
ISBN
978-3-030-15654-1
Number of pages of the result
22
Pages from-to
271-292
Number of pages of the book
494
Publisher name
Springer
Place of publication
Cham
UT code for WoS chapter
—