|
|
|
|
|
|
by zozbot234
2041 days ago
|
|
|
> Why make them look at and manipulate all the transformed statements Broadly speaking, because it's useful to have a marker of "was this statement derived via a proof by contradiction, or something like that?", and using the negative form is a sensible way of showing this. > In my field (topology), ... at the proof level everything is classical. On the contrary, constructive logic is found quite naturally (even in ordinary mathematics!) as the "internal language/logic" of some structures that are of interest to topologists. HoTT itself was designed as a logical foundation that works naturally with homotopies. |
|
|
To whom? (That is rhetorical. The point is that this is not useful information for most mathematicians -- if you picked up a random graduate textbook in, say, algebra or combinatorics, I am certain the theorems will not be annotated with which are proved by contradiction. Quoting you from earlier, "With all due respect, that seems a bit vague to me.")
> are of interest to topologists
I didn't mean to suggest I was speaking for all of topology (more specifically, I'm interested in low-dimensional topology), but still topology is a large field and what you are talking about is a small part of it. Also, just because there are constructive internal logics, I'm not sure that means the system you use to study them has to be constructive itself, and if that's what you are interested in studying you might want a more specialized system anyway.
You don't need to convince me that these things are interesting -- I have some knowledge about internal logics and I do some higher category theory. It's just that languages should be ergonomic for their users. Saying something is easy does not prove it is ergonomic.
Think about this: Most mathematicians I know that use Lean seem to turn on all the additional features that make it as classical as possible. They don't even want the inconvenience of marking definitions noncomputable.
(Maybe you're already familiar with how Lean works, but LEM and double negation elimination do not let you leak values to the Type level from the Prop level. A proof that there is a number with a specific property doesn't mean you actually can have such a number. You need the noncomputable choice function to "obtain" a value from an existential.)