Nuprl Definition : choice-principle
If P is a family of propositions (i.e. types) indexed by type T,
then for each t:T, P[t] is a type.
The type ∀t:T. P[t] is by definition the dependent function type
t:T ⟶ P[t]
One way to say that a type A is inhabited is the "truncation"
or "half squash" ⇃(A) which is the quotient A//True.
The choice principle for T says that every P[t] is inhabited
if and only if the function type t:T ⟶ P[t] is inhabited.
We prove that ChoicePrinciple(T) ⇐⇒ ⇃(canonicalizable(T))
(see choice-iff-canonicalizable).
Therefore we can prove ChoicePrinciple(ℕ) and ChoicePrinciple(ℕ ⟶ ℕ)
but we can also prove ¬ChoicePrinciple((ℕ ⟶ ℕ) ⟶ ℕ)
(see not-choice-baire-to-nat).
So the choice principle is true for type 0 and type 1 but false for type 2.⋅
ChoicePrinciple(T) == ∀P:T ⟶ ℙ. (∀t:T. ⇃(P[t]) ⇐⇒ ⇃(∀t:T. P[t]))
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
true: True,
function: x:A ⟶ B[x]
Definitions occuring in definition :
function: x:A ⟶ B[x],
prop: ℙ,
iff: P ⇐⇒ Q,
quotient: x,y:A//B[x; y],
all: ∀x:A. B[x],
so_apply: x[s],
true: True
FDL editor aliases :
choice-principle
Latex:
ChoicePrinciple(T) == \mforall{}P:T {}\mrightarrow{} \mBbbP{}. (\mforall{}t:T. \00D9(P[t]) \mLeftarrow{}{}\mRightarrow{} \00D9(\mforall{}t:T. P[t]))
Date html generated:
2018_07_29-AM-09_23_38
Last ObjectModification:
2018_07_25-PM-00_23_36
Theory : continuity
Home
Index