A comparison of type theory with set theory

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

A comparison of type theory with set theory

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

A comparison of type theory with set theory

Popis výsledku anglicky

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.

Druh

C - Kapitola v odborné knize

CEP obor

—

OECD FORD obor

60301 - Philosophy, History and Philosophy of science and technology

Projekt

<a href="/cs/project/GJ17-18344Y" target="_blank" >GJ17-18344Y: Logicko-filozofická analýza pojmu identity</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název knihy nebo sborníku

Reflections on the Foundations of Mathematics

ISBN

978-3-030-15654-1

Počet stran výsledku

22

Strana od-do

271-292

Počet stran knihy

494

Název nakladatele

Springer

Místo vydání

Cham

Kód UT WoS kapitoly

—