Nuprl Definition : choice-principle

If is family of propositions (i.e. types) indexed by type T,
then for each t:T, P[t] is type.
The type ∀t:T. P[t] is by definition the dependent function type
   t:T ⟶ P[t]
One way to say that type is inhabited is the "truncation" 
or "half squash" ⇃(A) which is the quotient A//True.

The choice principle for 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 and type 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: ⇐⇒ Q true: True function: x:A ⟶ B[x]
Definitions occuring in definition :  function: x:A ⟶ B[x] prop: iff: ⇐⇒ Q quotient: x,y:A//B[x; y] all: x:A. B[x] so_apply: x[s] true: True
FDL editor aliases :  choice-principle

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