Is this provable constructively?

Stream: general

[Vlad Firoiu]

I've been struggling to decide whether the following is provable constructively:
lemma not_forall_exists_nat (p : ℕ -> bool) : ¬ (∀ (a : ℕ), p a) -> ∃ (a : ℕ), ¬ p a

I don't see any way to prove it, so I've mostly given up hope that it is provable, but my intuition says that there is in fact a constructive procedure for producing the witness, which is to just check each natural in order. I imagine the way to show it is unprovable would be to exhibit some strange Godelian p.

[Anne Baanen]

I think it is unprovable constructively, with the counterexample Kripke model looking like ℕ union {*}, with * ≤ n for each n. At *, p never holds; at n, only p n holds. Then * |- ¬ (∀a, p a) (since at each point, at most one a satisfies p a), * ||- ∀ a, p a ∨ ¬ p a (since at each point n, just check whether n = a), but not * ||- ∃ a, ¬ p a (let n be the corresponding instantiation of a, then n ≥ * and p n is true but _|_ is false).

[Kenny Lau]

It is provable constructively.

[Chris Hughes]

How?

[Kenny Lau]

ah never mind my proof is circular.

[Kenny Lau]

however such an a can be found computably

[Yury G. Kudryashov]

But not in a predictable amount of time

[Yury G. Kudryashov]

As far as I understand, it is a requirement for a constructive proof

[Yury G. Kudryashov]

Disclaimer: I'm not an expert in constructive math

[Chris Hughes]

But not in a predictable amount of time

I don't think that's a requirement for constructiveness. Well foundedness of < on with_top nat can be proven constructively, but there's no bound on termination time.

[Chris Hughes]

This is surprisingly hard to do constructively

def find (h : ∃ n, p n) : {n // p n ∧ ∀ m, p m → n ≤ m} :=

[Yury G. Kudryashov]

Then see disclaimer ;)

[Mario Carneiro]

It is not provable constructively. This is also known as Markov's principle