Timeline for Why in Martin-Löf type theory any natural number is assumed to be either $0$ or $S(a)$ for some $a\in\mathsf{N}$?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 11, 2022 at 14:33 | vote | accept | qk11 | ||
| Jan 11, 2022 at 10:33 | answer | added | Peter LeFanu Lumsdaine | timeline score: 11 | |
| Jan 10, 2022 at 21:28 | answer | added | L. Garde | timeline score: 2 | |
| Jan 10, 2022 at 21:28 | comment | added | Andrej Bauer | Yes, if you read old books on logic, then they do indeed describe inductive construtions as saying "things constructed this was an no other way". Such statements do not survive scrutiny and are just handwaving explanations. They may serve a pedagogical purpose, but they also do a good deal of harm, as the present discussion confirms. | |
| Jan 10, 2022 at 21:25 | comment | added | LSpice | @AndrejBauer, no reference other than what I have mentioned in a comment below: informal notes that say "terms constructed in this way are of type $\mathsf N$", and less informal notes that say "terms constructed in this way are of type $\mathsf N$, and no other terms are of this type." I did not mean to make a statement about the formal theory, just the sort of thing that one might encounter (or at least, I did) in introductory notes. (That's why I referred, obtusely, to an understanding (often elided in notes) rather than an assumption.) | |
| Jan 10, 2022 at 21:21 | answer | added | Andrej Bauer | timeline score: 11 | |
| Jan 10, 2022 at 20:49 | comment | added | Andrej Bauer | @LSpice: Nope, there is no such assumption in type theory. Do you have a reference? | |
| Jan 10, 2022 at 20:32 | answer | added | András Kovács | timeline score: 2 | |
| Jan 10, 2022 at 17:24 | comment | added | LSpice | In type theory, it is usually understood—not just for the natural-number type—that any terms constructed using the construction rules, and only terms so constructed, belong to the type. | |
| Jan 10, 2022 at 17:17 | history | asked | qk11 | CC BY-SA 4.0 |