axiom of countable choice

短语

释义与例句

n.
  1. 1.

    A weaker form of the axiom of choice that states that every countable collection of nonempty sets must have a choice function; equivalently, the statement that the direct product of a countable collection of nonempty sets is nonempty.

    数学 可数

    we have no way to infer ∃R∀n[P0n→∀x(R_nx→Fx)∧n=Nx:R_nx)] without an axiom of countable choice.

    2013, Valentin Blot, Colin Riba, On Bar Recursion and Choice in a Classical Setting, Chung-chien Shan (editor), Programming Languages and Systems: 11th International Symposium, APLAS 2013, Proceedings, Springer, LNCS 8301, page 349, We show how Modified Bar-Recursion, a variant of Spector's Bar-Recursion due to Berger and Oliva can be used to realize the Axiom of Countable Choice in Parigot's Lambda-Mu-calculus, a direct-style language for the representation and evaluation of classical proofs.