## Stream: maths

### Topic: Constructive Logic

#### Chris Hughes (Oct 15 2019 at 17:09):

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

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

#### Kenny Lau (Oct 15 2019 at 17:15):

btw choice implies em so you can just say choice

#### Chris Hughes (Oct 15 2019 at 17:17):

btw choice implies em so you can just say choice

Updated to em or choice

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

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


#### Chris Hughes (Oct 15 2019 at 17:33):

Provable without choice was the meaning I intended.

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

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

#### Ulrik Buchholtz (Oct 15 2019 at 20:44):

Here we're talking about $\Sigma^0_1$, not $\Pi^0_2$, sentences. For the former, once you know the witness $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.

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

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