# Zulip Chat Archive

## 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.

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

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