Nuprl Definition : set-axiom-of-choice
If we think of "sets" as types, then a family of non-empty sets is
given by an "index set" T and a function S ∈ T ⟶ Type such that
∀x:T. (S x). The condition ∀x:T. (S x) says that each "set" S x is inhabited.
Now, the constructive interpretation of ∀x:T. (S x) is a function of type ⌜x:T ⟶ (S x)⌝
, so one version of the axiom of choice is necessarily true.
But, if we require a "function" from the family of sets S x to members of those
sets, then the function must be extensional. That would mean that
when two sets S x and S y are extensionally the same set then the function
must choose the same value for S y that it chooses for S x.
We define here the statement of an axiom of choice that says that such
an extensional choice function exists. Instead of extensional equality of sets
we use extensional equality of types.
Following Diaconescu (or Goodman-Myhill) we can prove that this
version of AC implies the law of excluded middle
(set-axiom-of-choice-implies-xmiddle).
And therefore, it is proveably false in Nuprl
(set-axiom-of-choice-is-false).⋅
Set-AC == ∀T:Type. ∀S:T ⟶ Type. ((∀x:T. (S x)) ⇒ (∃f:x:T ⟶ (S x). ∀x,y:T. (S x ≡ S y ⇒ ((f x) = (f y) ∈ (S x)))))
Definitions occuring in Statement :
ext-eq: A ≡ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
universe: Type,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
ext-eq: A ≡ B,
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
set-axiom-of-choice
Latex:
Set-AC ==
\mforall{}T:Type. \mforall{}S:T {}\mrightarrow{} Type.
((\mforall{}x:T. (S x)) {}\mRightarrow{} (\mexists{}f:x:T {}\mrightarrow{} (S x). \mforall{}x,y:T. (S x \mequiv{} S y {}\mRightarrow{} ((f x) = (f y)))))
Date html generated:
2018_07_25-PM-02_34_08
Last ObjectModification:
2016_11_23-PM-05_12_42
Theory : subtype_1
Home
Index