Assumptions about data produced by `classical.choice`

Stream: general

[Jesse Michael Han]

I think of data produced by a choice principle as a "generic element" satisfying the given specification, so that e.g. it should not be possible to prove that

(classical.choice (by apply_instance) : nat) = 0

Is it inconsistent to assume something like this, though?

[Simon Hudon]

If that was inconsistent, wouldn't that mean that you could prove this?

(classical.choice (by apply_instance) : nat) ≠  0

[Jesse Michael Han]

ah yes, you're right

[Jesse Michael Han]

I guess Lean really doesn't decide such things (of course this generic nat must be interpreted literally as some nat if we take a model in ZFC, but there's no guarantee which one)

[Simon Hudon]

So you can construct a model where it gives you 0 and a different one where it gives you 1

[Jesse Michael Han]

another related question: if we can prove P (classical.choice (h : nonempty X) : X) then is it a (meta)theorem that this lifts to a proof of
(∀ x : X, P x)?

[Simon Hudon]

I don't think that's a theorem but I would think that it is a meta theorem

[Kevin Buzzard]

classical.choice is an axiom; my guess is that any statement you can make about the natural it produces will be independent.

[Chris Hughes]

What if P is λ x, x = (classical.choice (h : nonempty X) : X)?