|
| dang wrote:
| Discussed at the time:
|
| _Types versus sets (and what about categories?)_ -
| https://news.ycombinator.com/item?id=30697421 - March 2022 (31
| comments)
| gylterud wrote:
| > various versions of Martin-Lof's intuitionistic type theory and
| finally the calculus of constructions of Coquand and Huet. In
| every case, they were created with no interpretation in mind.
| They were justified syntactically, for example via proofs of
| strong normalisation. Models came later.
|
| Martin-Lof very explicitly discussed the denotational meaning of
| his theories. See for instance Section 5 of the SEoP entry on
| intuitionistic type theory.
|
| https://plato.stanford.edu/entries/type-theory-intuitionisti...
|
| TFA is correct that type theory is syntax, but it would be wrong
| to think of set theory as any less syntactic to the mind of an
| intuitionist. The semantics is the actual mathematical ideas
| going on within the head of the mathematician. Both type theory
| and set theory must be connected to these in order to be given
| meaning.
___________________________________________________________________
(page generated 2023-08-31 23:00 UTC) |