Timeline for Does the "propositions-as-types" paradigm match mathematical practice?
Current License: CC BY-SA 3.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 25, 2016 at 16:00 | comment | added | Adam Epstein | Even in reading ZF texts I find myself thinking something similar regarding class existence assertions. "There exists a (definable) class such that ..." is not even an honest paraphrase, where as "Here is a such a class" is. | |
| Sep 24, 2016 at 7:06 | comment | added | Andrej Bauer | See the introduction of tac.mta.ca/tac/volumes/30/37/30-37.pdf where there is a short discussion of the Problem/Construction style of writing. | |
| Sep 23, 2016 at 7:38 | comment | added | Andrej Bauer | If you're going to construct things, note that there can be more than one construction for a single problem, so you really should number the constructions as well as the problems, or stick to the convention that an unnumbered construction carries the same number as the corresponding problem. One day, when the math community is using computer proof assistants, we'll name theorems, proofs, problems and constructions need rather than number them. But we're not there yet. | |
| Sep 23, 2016 at 7:35 | comment | added | Andrej Bauer | I think you should credit Euclid for the original invention, as well as the recent efforts of Vladimir Voevodsky to bring this point to the attention of mathematical community. I'll try to find a good reference, but if you look at his recent arXiv papers, they're written in this style. | |
| Sep 22, 2016 at 21:57 | comment | added | André Henriques | At the next good opportunity, I will use "Problem 4.2: Give x such that θ(x) Construction. (Construction of x is given here.) DEFINED" in a paper of mine. Who should I credit for this? (this MO post?) Is this your idea, Andrej, to phrase things like that? Has this been used somewhere? (Euclid?) | |
| Sep 22, 2016 at 9:36 | comment | added | Andrej Bauer | By the way, we can use double negation in place of propositional truncation, in which case we get a known translation of classical logic into type theory. | |
| Sep 20, 2016 at 20:20 | comment | added | Andrej Bauer | Nope, propositional truncation is not double negation. Double negation deletes witnesses in a more radical way than propositional truncation, which lets you extract a witness provided that it does not matter which one got extracted (I am speaking informally). | |
| Sep 20, 2016 at 15:20 | comment | added | user44143 | If I try interpreting truncation as double negation, will that correctly predict the inferences among truncated and untruncated propositions? | |
| Sep 18, 2016 at 19:05 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 5 characters in body
|
| S Sep 17, 2016 at 19:46 | history | suggested | Max New | CC BY-SA 3.0 |
fix name mismatch
|
| Sep 17, 2016 at 19:38 | review | Suggested edits | |||
| S Sep 17, 2016 at 19:46 | |||||
| Sep 17, 2016 at 17:40 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 872 characters in body
|
| Sep 17, 2016 at 17:35 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 872 characters in body
|
| Sep 17, 2016 at 17:20 | history | answered | Andrej Bauer | CC BY-SA 3.0 |