[kmill]

A way to think about whether something is constructive is that everything is decidable, in the sense that there is some procedure that will give you the answer in finite time.

In Kevin's example where you have two programs, one which depends on the Riemann hypothesis being true and the other which depends on it being false, is that you can't just execute the programs -- they might have undefined behavior since they depend on the truth of some statement during their executions, and there's no general algorithm to decide whether undefined behavior is happening. They depend on undecided facts, so you can't put them together into a single program that decides the result. (Maybe a slogan is "truth can be contingent, but data cannot be.")

In Lean syntax, this is an example type signature of something that takes two programs (h and h') that respectively take in the truth/proof of a proposition or its negation, along with a proof that there is at most one element of α, and produces that element. I don't think there's a way to write this definition in Lean without marking the definition noncomputable:

  def extract {p : Prop} {α : Type*}
    (h : p → α) (h' : ¬p → α)
    (unique : ∀ (x y : α), x = y) : α := sorry

(the sorry indicates a missing definition).

[auggierose]

Yeah, I really was joking.