[zozbot234]

> Sure, you can 'just' stick to the negative fragment, but that 'just' is sweeping a lot of questions of ergonomics under the rug.

With all due respect, that seems a bit vague to me. What are the "questions of ergonomics" you're thinking of here? Choosing the negative form of a goal whenever you have to prove something non-constructively seems even easier ergonomically than, e.g. adding LEM as an axiom. You basically don't have to change your proof methods as long as the statement you're proving is of the appropriate form.

[kmill]

Ergonomics to me means "what is the moment-to-moment experience of a user of the language, in particular frictions between what the user wants to say and how it must be said." For someone who does not care much about constructibility, it is better not having to do anything differently depending on whether or not something is constructive. The workaround for such people could be to always include at least one negation for every statement, but that's a pervasive reminder of questions of constructibility! If practitioners are going to be using this transformation by default, then the language would be more ergonomic if it was just automatic.

I don't think having to think about constructibility all the time is more ergonomic than accepting that the system has a well-accepted axiom. There doesn't need to be a one-true system, of course, and for people interested in foundations, reverse mathematics, constructive mathematics, higher category theory, and homotopy type theory, there are other systems. Most mathematicians don't study these things, and accepting LEM is natural for them.

[zozbot234]

> For someone who does not care much about constructibility, it is better not having to do anything differently depending on whether or not something is constructive.

Well, there are many possible constructive 'versions' of any non-constructive statement, so 'not having to do anything or be reminde[d] of questions of constructivity', strictly speaking, leads to just sticking to the non-constructive version by default. Since it's easy, even in constructive logic, to derive the non-constructive 'version' of some statement from a constructive one, this transformation (properly understood) is as good as automatic.

[kmill]

Right, that's what I am getting at. If it is as good as automatic, why make a mathematician do the transformation themselves? Why make them look at and manipulate all the transformed statements when they're working out a tactic proof?

Whether or not a proposition is constructive is not something I've ever heard any mathematicians in my department ever worry about. I have only ever heard about, for example, showing a certain bound was "effective" after showing that there was a bound at all. Effective means that there is some procedure to construct the number -- but no one cares about whether the argument that shows this number is an upper bound is itself constructive. Lean with its Prop, Type 0, Type 1, ... universe hierarchy is sort of well suited for this.

I'm sure that there are interesting questions that hinge on constructibility in a proof, but again, mathematicians I talk to have never seriously thought about these things. In my field (topology), we do worry about constructing objects and invariants (and sometimes we even care about the complexity class), but at the proof level everything is classical.

If you're involved in developing proof assistants and you want mathematicians to use it, then I would suggest making it so you can change the "reasoning monad" in a file. If you put it in classical mode, it should look like you're able to use LEM, etc., and the goal window should show only untransformed statements, but then when outside the classical monad a constructivist would see the transformed statements. This would be sufficiently ergonomic.

[zozbot234]

> 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.

[kmill]

> it's useful to have a marker

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.)