17
$\begingroup$

I've wondered how a type theory/proof assistant could manage to add countable choice (or its dependent choice version) as something primitive as well as to keep the computational properties, e.g., canonicity.

The axiom of countable choice is important in analysis that it allows real numbers behaving much familiar for classical-minded mathematicians. It is thought by some people "constructive" since it can be justified in effective topos. Also, it holds in many type theories as meta-theorem, at least in the empty context. However, it seems mainstream proof assistants do not incorporate it into their core languages. So I was wondering if anyone has ever figured out how to do that?

This question is related to What axioms have a computational interpretation? and Incorporating Markov's principle in various proof assistants.

P.S. Choice is subtle in type theory admittedly, so maybe I should add that we understand the axiom of choice as so-called Extensional Axiom of Choice or the propositional-truncated version in HoTT (c.f. HoTT Book Chapter 3.8), instead of the form "trivially true in constructive type theory" which has no essential logical consequence.

P.P.S. Other forms of choice are also welcomed!

P.P.P.S. I prefer answers about "computationally sensible type theory which validates countable choice" as elaborated shortly in Andrej Bauer's answer. I think cubical type theory is a perfect example that a new type Glue is introduced with full reduction rules so that axiom of univalence can be proved and computed. I want to know if similar things can be done for countable choice.

Improve this question
$\endgroup$
2
  • $\begingroup$ Huh so there's interpretations of LEM in substructural logic or more radically cointuitionistic logic but IDK about choice. I had some ideas about messing around with the category of well ordered sets or something to do with the category of commutative monoids (equivalent to presheafs over nats and so kind of like a free cocompletion of the nats and kind of like ordinals). IIRC assuming a group structure ~ choice Anyhow I never could figure any of it out . $\endgroup$
    – Molly Stewart-Gallus
    Mar 11, 2022 at 4:49
  • $\begingroup$ Also see here for the meaning of CC in a variety of contexts: ncatlab.org/nlab/show/countable+choice $\endgroup$
    – François G. Dorais
    Mar 11, 2022 at 5:22

2 Answers 2

Reset to default
5
$\begingroup$

It really depends on what you call countable choice, and in particular the semantics of your Prop fragment.

Assuming you phrase CC as (forall n : nat, ||P n||) -> ||forall n : nat, P n|| where P : nat -> Type and ||·|| as the boxing from Type to Prop, then there are basically two situations.

  • In a purely intuitionistic setting, CC is just true and behaves like the identity modulo boxing and unboxing. This is OK because Prop terms enjoy canonicity.

  • If you have classical logic in Prop, CC is nasty because it is an instance of double negation shift. One way to implement it is to encode functions nat -> X as a lazy streams with sharing. Essentially, you build finite prefixes of the choice function on demand.

Improve this answer
$\endgroup$
10
  • $\begingroup$ Thanks for your reply! But I'm not sure about the meaning of "CC is just true"... Do you mean something like "the plain form of choice axiom holds for MLTT trivially"? Could anyone use that to deduce the completeness of Cauchy reals? $\endgroup$
    – KANG Rongji
    Mar 10, 2022 at 18:17
  • $\begingroup$ Without some form of classical logic you won't go far proving the completeness of reals. So CC has a trivial computational content (essentially the identity) but it is useless. Up to impredicativity everything you do in Prop you could already do in Type. $\endgroup$
    – Pierre-Marie Pédrot
    Mar 10, 2022 at 21:46
  • 3
    $\begingroup$ @Pierre-MariePédrot Countable choice implies Cauchy Reals are isomorphic to Dedekind Reals, without classical logic. $\endgroup$
    – Trebor ♦
    Mar 11, 2022 at 0:13
  • $\begingroup$ CC means $\forall n, \Vert P n\Vert \to \Pi n, P n$ $\endgroup$
    – François G. Dorais
    Mar 11, 2022 at 3:10
  • 1
    $\begingroup$ What does "purely intuitionistic" mean? $\endgroup$
    – Andrej Bauer
    Mar 11, 2022 at 6:41
5
$\begingroup$

In realizability theory another computational interpretation of countable choice is a procedure for computing canonical forms of natural numbers. I explained this in detail in this answer to a similar question on MathOverflow.

There is a different sense in which one could approach the question, namely: can we decide a computationally sensible type theory which validates countable choice? To make the question interesting, such a theory should differentiate between $\exists$ and $\Sigma$ (because the axiom of choice stated using $\Sigma$ is trivially true). The French type theorists know a lot more about this than I do, so it would be better to consult them.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Your explanation on MathOverflow is great! But I was meant the ask about the latter point. I think the propositional truncation provided in HoTT is a way to distinguish ∃ and Σ. $\endgroup$
    – KANG Rongji
    Mar 12, 2022 at 2:13
  • $\begingroup$ Yes, it's one way of doing it, but not the only one. $\endgroup$
    – Andrej Bauer
    Mar 12, 2022 at 8:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.