Zulip Chat Archive

Stream: general

Topic: Is this provable constructively?


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kenny Lau (Jan 21 2020 at 15:59):

It is provable constructively.

view this post on Zulip Chris Hughes (Jan 21 2020 at 16:02):

How?

view this post on Zulip Kenny Lau (Jan 21 2020 at 16:04):

ah never mind my proof is circular.

view this post on Zulip Kenny Lau (Jan 21 2020 at 16:04):

however such an a can be found computably

view this post on Zulip Yury G. Kudryashov (Jan 21 2020 at 16:06):

But not in a predictable amount of time

view this post on Zulip Yury G. Kudryashov (Jan 21 2020 at 16:07):

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

view this post on Zulip Yury G. Kudryashov (Jan 21 2020 at 16:08):

Disclaimer: I'm not an expert in constructive math

view this post on Zulip 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.

view this post on Zulip 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} :=

view this post on Zulip Yury G. Kudryashov (Jan 21 2020 at 20:18):

Then see disclaimer ;)

view this post on Zulip 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