### Nuprl Lemma : Rice-theorem-for-Type

`∀F:Type ⟶ 𝔹. ((∀X,Y:Type.  (X ~ Y `` F X = F Y)) `` ((F = (λT.tt) ∈ (Type ⟶ 𝔹)) ∨ (F = (λT.ff) ∈ (Type ⟶ 𝔹))))`

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` bfalse: `ff` btrue: `tt` bool: `𝔹` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  not: `¬A` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` compose: `f o g` false: `False` assert: `↑b` ifthenelse: `if b then t else f fi ` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` exists: `∃x:A. B[x]` bfalse: `ff` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` so_apply: `x[s]` so_lambda: `λ2x.t[x]` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  equal-wf-base-T equal-wf-T-base btrue_neq_bfalse assert_elim false_wf assert_wf iff_imp_equal_bool iff_weakening_equal subtype_rel_self true_wf squash_wf nat-inf_wf compose_wf nat-inf-limit nat-inf-infinity_wf nat2inf_wf nat_wf nat-inf-attach bfalse_wf assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert btrue_wf eqtt_to_assert bool_wf equal_wf equipollent_wf all_wf
Rules used in proof :  inrFormation functionExtensionality inlFormation voidEquality independent_pairFormation baseClosed imageMemberEquality natural_numberEquality imageElimination rename voidElimination independent_functionElimination dependent_functionElimination promote_hyp dependent_pairFormation because_Cache independent_isectElimination productElimination equalitySymmetry equalityTransitivity equalityElimination unionElimination applyEquality hypothesis hypothesisEquality functionEquality cumulativity lambdaEquality sqequalRule universeEquality isectElimination sqequalHypSubstitution extract_by_obid introduction instantiate thin cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}F:Type  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}X,Y:Type.    (X  \msim{}  Y  {}\mRightarrow{}  F  X  =  F  Y))  {}\mRightarrow{}  ((F  =  (\mlambda{}T.tt))  \mvee{}  (F  =  (\mlambda{}T.ff))))

Date html generated: 2018_07_29-AM-09_29_31
Last ObjectModification: 2018_07_27-PM-04_34_49

Theory : basic

Home Index