## Stream: general

### Topic: Is this provable constructively?

#### Vlad Firoiu (Jan 21 2020 at 13:22):

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 (Jan 21 2020 at 13:46):

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 (Jan 21 2020 at 15:59):

It is provable constructively.

How?

#### Kenny Lau (Jan 21 2020 at 16:04):

ah never mind my proof is circular.

#### Kenny Lau (Jan 21 2020 at 16:04):

however such an a can be found computably

#### Yury G. Kudryashov (Jan 21 2020 at 16:06):

But not in a predictable amount of time

#### Yury G. Kudryashov (Jan 21 2020 at 16:07):

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

#### Yury G. Kudryashov (Jan 21 2020 at 16:08):

Disclaimer: I'm not an expert in constructive math

#### Chris Hughes (Jan 21 2020 at 16:30):

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 (Jan 21 2020 at 16:54):

This is surprisingly hard to do constructively

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


#### Yury G. Kudryashov (Jan 21 2020 at 20:18):

Then see disclaimer ;)

#### Mario Carneiro (Jan 21 2020 at 21:27):

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

Last updated: May 06 2021 at 22:13 UTC