Zulip Chat Archive

Stream: maths

Topic: Constructive Logic


view this post on Zulip Chris Hughes (Oct 15 2019 at 17:09):

Is there some meta theorem saying something like if PP is a decidable predicate and nN,P(n)\exists n \in \mathbb{N}, P(n) is provable with em or choice, than nN,P(n)\exists n \in \mathbb{N}, P(n) is provable without em or choice

view this post on Zulip Kenny Lau (Oct 15 2019 at 17:15):

sounds like Goodstein's theorem (where a forall-exists statement is provable with transfinite induction but not in peano arithmetic)

view this post on Zulip Kenny Lau (Oct 15 2019 at 17:15):

btw choice implies em so you can just say choice

view this post on Zulip Chris Hughes (Oct 15 2019 at 17:17):

btw choice implies em so you can just say choice

Updated to em or choice

view this post on Zulip Chris Hughes (Oct 15 2019 at 17:20):

sounds like Goodstein's theorem (where a forall-exists statement is provable with transfinite induction but not in peano arithmetic)

It was hearing about Goodstein's theorem that made me think about this question. The \exists on it's own version is more interesting. It occurred to me that there might be functions that don't terminate, but there is a nonconstructive proof that they do.

view this post on Zulip Gabriel Ebner (Oct 15 2019 at 17:32):

You need to require that decidable_pred P is provable without choice, consider for example ∃ n, ∀ p, p ∨ ¬ p which is equivalent to LEM.

example : decidable ( p, p  ¬ p) := is_true classical.em

view this post on Zulip Chris Hughes (Oct 15 2019 at 17:33):

Provable without choice was the meaning I intended.

view this post on Zulip Ulrik Buchholtz (Oct 15 2019 at 20:30):

This question is closely related to Markov's principle. If you believe in the soundness of em/choice, then you can just start searching for a witness, and you'll eventually find one.

view this post on Zulip Chris Hughes (Oct 15 2019 at 20:41):

But don't I need more than soundness to know that this will terminate? By incompleteness there will be sequences whose termination is independent of Lean, so it would be consistent to assume they did. Just because something doesn't terminate doesn't mean there's a proof of non-termination.

view this post on Zulip Ulrik Buchholtz (Oct 15 2019 at 20:44):

Here we're talking about Σ10 \Sigma^0_1 , not Π20 \Pi^0_2 , sentences. For the former, once you know the witness n n , you just give it to the decider and it spits out your proof. You're right in the latter case, where there's a parameter.

view this post on Zulip Chris Hughes (Oct 15 2019 at 21:21):

So I read the article and it seems that you need to believe in omega consistency rather than just consistency. So my question was more or less by definition "is the axiom of choice omega consistent?"

Thanks, you've given me some reading.

view this post on Zulip Chris Hughes (Oct 15 2019 at 21:45):

I think maybe I was conflating soundness and consistency.


Last updated: May 14 2021 at 20:13 UTC