Constructive Logic

Stream: maths

[Chris Hughes]

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]

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

[Kenny Lau]

btw choice implies em so you can just say choice

[Chris Hughes]

btw choice implies em so you can just say choice

Updated to em or choice

[Chris Hughes]

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]

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]

Provable without choice was the meaning I intended.

[Ulrik Buchholtz]

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]

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]

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]

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]

I think maybe I was conflating soundness and consistency.