marking definitions as arbitrary

Stream: general

[Mirek Olšák]

This topic was touched in more threads, so I thought of making a thread on its own. Currently, Lean does not distinguish choice and unique choice. The question is what would be a good way of tracing which definitions do not depend on particular values of the choice function.

[Mirek Olšák]

Why should we want this:

• More completeness. If a claim does not use a choice-dependent definition, it is more likely to be provable or disprovable.
• Modelling with ZFC. In logic based on set-theory, uniqueness if often an essential fact about a definition. For example I believe Mizar requires a proof of uniqueness to make a definition (although I don't know the details).
• Better order in the definitions. Currently, definitions using choice just have it mentioned in the doc-string.

[Mirek Olšák]

Why it is not as simple

• Arbitrary choice doesn't matter if it hidden in a proof. So adding a unique_choice axiom, and wanting non-arbitrary definitions to only depend on that is too restrictive.
• There is no way to make Ordinal.ToType or Cardinal.outnon-arbitrary in Lean due to universe constraints (although it doesn't feel like making arbitrary choices).
• choice is sometimes used for dummy values (for example in limUnder) which is unfortunate. If Lean starts caring about arbitrary definitions at some point, it should perhaps reconsider such cases

[Mirek Olšák]

In another thread, @Kyle Miller mentioned we could perhaps add a tag arbitrary (like uncomputable) which could track that the definition uses Classical.choice in an essential way.

[Violeta Hernández]

I don't believe you're going to gain much traction in adding new axioms to Mathlib.

[Mirek Olšák]

Adding a new axiom is not the suggestion. I rather explained in the first point of "Why it is not as simple" why adding an axiom is not a solution.

[Notification Bot]

This topic was moved here from #general > marking definitions as aritrary by Mirek Olšák.

[Johan Commelin]

You could prove a lemma that the choice is unique. And potentially register an attribute that such lemmas can be tagged with.

[Mirek Olšák]

I don't think it is possible to state "Function f doesn't depend on the values of Classical.choice." as a lemma.

[Mirek Olšák]

It is rather a meta-property.

[Johan Commelin]

But you can prove that some predicate is satisfied uniquely, right? Maybe I'm missing something obvious...

[James E Hanson]

I think Mirek is talking about functions whose definitions depend on Classical.choice and you're talking about the things one applies Classical.choice to.

[James E Hanson]

Given a function already defined in terms of Classical.choice, there's no internal way to extract a parameterized version of the function that depends on an explicit choice of choice function.

[James E Hanson]

But one certainly could write a script that produces such a thing, which is maybe what you're thinking of.

[Johan Commelin]

Aha, thanks for clarifying!

[Violeta Hernández]

My general opinion on matters surrounding choice is that Mathlib does not and should not shy away from the axiom.

[Violeta Hernández]

We could certainly be more careful with it, avoiding it when unnecessary, adding decidability assumptions everywhere, cataloguing which uses are of unique choice and which uses are "real" choice. But that would be more annoying for everyone at the convenience of like five people. That ship sailed long ago.

[Ruben Van de Velde]

Turning it around, if there's things that can be done that don't increase the maintenance burden on other mathlib contributors and maintainers, but do improve the situation for people who care about constructivism, I don't see a reason to reject those out of hand. But that's a big "if".

[Mirek Olšák]

I don't think mathematicians care about constructivism, but they care about explicit (non-choicy) definitions.

[Mirek Olšák]

Maybe, we could just first write an analysis tool which checks which Mathlib definitions are choice-dependent.

[Artie Khovanov]

Isn't it (theoretically) possible to make computable any definition that does not "really" make use of choice?
Like you can imagine checking every possible value and terminating at the first one that works, and then you prove that such a value exists and is unique.

[Artie Khovanov]

In this case avoiding (Lean's version of) choice is the same as just giving a construction

[Mirek Olšák]

That requires countability of the domain, and decidability of the predicate.

[Trebor Huang]

Artie Khovanov said:

Isn't it (theoretically) possible to make computable any definition that does not "really" make use of choice?
Like you can imagine checking every possible value and terminating at the first one that works, and then you prove that such a value exists and is unique.

This is essentially Markov's principle, which is one of the main logical principles that are "computable" (ie. true in some realizability interpretation) but not strictly constructive.