Timeline for Does the "propositions-as-types" paradigm match mathematical practice?
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 18, 2016 at 12:33 | comment | added | Neal | My first seems to come across as snark, so I apologize. I am genuinely curious. | |
| Sep 18, 2016 at 11:03 | comment | added | Adam Epstein | @Neal As such a mathematician, I might be given the right motivation. | |
| Sep 17, 2016 at 18:45 | comment | added | Qfwfq | @Neal: is it really relevant? | |
| Sep 17, 2016 at 17:20 | answer | added | Andrej Bauer | timeline score: 24 | |
| Sep 17, 2016 at 16:08 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
edited title
|
| Sep 17, 2016 at 16:03 | comment | added | user40276 | Let me go back to the philosophical foundations. From andrew.cmu.edu/user/ulrikb/80-518-818/MartinLof83.pdf, one can conclude that to know something is same thing as knowing that someone knows something. So why would you want to know? This is one problem (discovered by a friend of mine), for instance. | |
| Sep 17, 2016 at 16:00 | comment | added | user40276 | ...A problem is that the notion of truth and knowledge turns out the be a little redundant and some ontology is lost (this is in the philosophical foundations). Now from the perspective of the practical context (that is from the ML theory), there's the problem (essentially appearing in all intuitionist theory) of identifying the knowledge about the object and the object itself. Furthermore, I don't know if any (homotopy) type corresponds to a meaningful proposition, in other words, if the proofs of propositions (say in Peano arithmetic) exhausts all (homotopy) types. | |
| Sep 17, 2016 at 15:58 | comment | added | user40276 | If you mean ML type theory, connectives are not "in the theory", just meaningful propositions and judgements. But it's correct that ML type unifies the two layer metatheory and theory but this can be problematic. First, let me clarify that the philosophical foundations of ML are problematic and do not present the theory properly (the action of constructing is not faithful with the one in the theory). ... | |
| Sep 17, 2016 at 13:06 | comment | added | Neal | I wonder how many mathematicians working outside logic concern themselves with this distinction in their work. | |
| Sep 17, 2016 at 12:49 | review | First posts | |||
| Sep 17, 2016 at 12:56 | |||||
| Sep 17, 2016 at 12:49 | history | asked | user98585 | CC BY-SA 3.0 |