aws
Reputation
1,826
Top tag
Next privilege 2,000 Rep.
 Jan 28 answered Is there a conservative extension of IZF that extends IZF by a weak form of the axiom of choice? Jan 22 awarded Yearling Sep 10 revised Countable choice and term extraction added 546 characters in body Sep 10 comment Countable choice and term extraction I'm sorry but I was maybe unclear there. That's just why you're unlikely to see all the details written out, not that it's impossible or any harder than without choice. Formal proofs will always be longer than informal ones whether they use choice or not - that's why we use proof assistants instead of writing them out. If you're still happy with that I can edit it into the answer. Sep 10 comment Countable choice and term extraction I don't know any such worked examples off hand and unfortunately I think it's unlikely there are any, since the first step is to write out full formal proofs which can get quite long even for simple statements. You're more likely to find proof assistants that do this automatically but I have no idea which ones both allow countable choice and term extraction, and this is probably no more helpful than the proofs that it is possible in theory. Sep 10 comment Countable choice and term extraction As I've said, when we extract computational information from proofs the two definitions become essentially the same, so the algorithms we get will be roughly the same for either. Sep 10 comment Countable choice and term extraction Well, the definitions are not so different in the sense that a constructive proof that a particular sequence satisfies one definition will give us a proof that that particular sequence satisfies the other. But this is a metamathematical result. To say the implication holds internally in a theory is slightly different. Sep 10 comment Countable choice and term extraction I think the line you referred to in the paper is maybe not the best example of AC - it's not really clear what role it's playing there. A basic example of CC would be where you drop modulus function from the definition of real and instead require that for every $k$ there exists $N$ such that $|a_n - a_m| < 2^{-k}$ for $n, m > N$. This is different to having a modulus function because there could be more than 1 such N but a function would pick out exactly 1. However assuming CC the two definitions are equivalent. Sep 10 comment Countable choice and term extraction I think more generally I can't really give a solid philosophical argument for or against countable choice. The best I can say is that it's used a lot to make things easier but can often be avoided through more careful definitions and proofs and is in many cases known to be "harmless" anyway through metamathematical techniques like realizability. Sep 10 comment Countable choice and term extraction I had a little look at the paper you linked to. It looks like the formalism used there is a little unusual. It seems that logical formulas always implicitly refer to their Dialectica interpretation (Gödel's Dialectrica is another logical interpretation like realizability). By the "axiom" of choice, they really mean a certain theorem that holds (theorem 11, part 16 I think). Perhaps this is necessary to work with finitistic theories. Maybe that explains why the use of choice is a bit strange in that paper. Sep 9 comment Countable choice and term extraction I guess the main idea is that the only logical rules you have available are ones that preserve computational information, and the reason is that they really do fit with the BHK interpretation. For example to prove $(\exists n)\phi(n)$ the only ways you have available involve finding an actual witness. By the way you might prefer the type theory approach - instead of proving something and then extracting witnesses afterwards, proofs and computations are literally the same thing throughout. Sep 8 answered Countable choice and term extraction Sep 8 comment Hidden usage of countable choice I only have "dead tree" versions of the books I'm afraid. I'll put some different references in my answer to the other question. Sep 8 comment Hidden usage of countable choice @Wojowu if you're new to constructivism you might prefer Bishop and Bridges, Constructive Analysis. Sep 8 comment Hidden usage of countable choice @Wojowu In fact you can't even show that the supremum of $\{0, x \}$ is attained for every $x$ because this would imply $x \leq 0$ or $x \geq 0$ which can't be done constructively. In chapter 6, 1.10 in Troelstra, van Dalen Constructivism in Mathematics they show that the supremum of the range of $f : [a, b] \rightarrow \mathbb{R}$ is not always attained, but if you look at the proof it also applies to finite sets of the form $\{0, x\}$. (By the same argument I said but in more detail) Sep 8 comment Hidden usage of countable choice @CameronBuie I'm not assuming they are pairwise distinct - I guess I should have said finitely enumerable rather than finite. (Note that if the set is obtained by evaluating a function at finitely many points they might not be pairwise distinct) Sep 8 comment Hidden usage of countable choice @ValerySaharov I'm not sure if this has what you want, but there's a section on realizability in Troelstra, van Dalen, Constructivism in Mathematics which is chapter 4, section 4. I slightly glossed over some details. To get existence properties such as the numerical existence property and Church's rule (that I alluded to) we use a more sophisticated form of realizability - q realizability. This is in volume II of Troelstra, van Dalen (chapter 9, section 7). Sep 8 revised Hidden usage of countable choice added 20 characters in body Sep 7 answered Hidden usage of countable choice Apr 10 comment What is the origin of the use of $\Pi$ and $\Sigma$ for dependent function and dependent product types in type theory?