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

`∀F:Type ⟶ 𝔹`
`  ((∀X,Y:Type.  (X ~ Y `` F X = F Y)) `` (∀X,Y:Type.  (F X = F Y ∨ (∃p:ℕ∞ ⟶ 𝔹. ((∀n:ℕ. (¬↑(p n∞))) ∧ (↑(p ∞)))))))`

Proof

Definitions occuring in Statement :  nat-inf-infinity: `∞` nat2inf: `n∞` nat-inf: `ℕ∞` equipollent: `A ~ B` nat: `ℕ` assert: `↑b` bool: `𝔹` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` decidable: `Dec(P)` or: `P ∨ Q` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` and: `P ∧ Q` so_apply: `x[s]` guard: `{T}` exists: `∃x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` bfalse: `ff` cand: `A c∧ B` not: `¬A` false: `False` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` uimplies: `b supposing a` bnot: `¬bb` ifthenelse: `if b then t else f fi ` squash: `↓T` true: `True` compose: `f o g` assert: `↑b` sq_type: `SQType(T)`
Lemmas referenced :  decidable__equal_bool exists_wf nat-inf_wf bool_wf all_wf nat_wf not_wf assert_wf nat2inf_wf nat-inf-infinity_wf equal_wf equipollent_wf nat-inf-attach bnot_wf assert_of_bnot assert_elim bfalse_wf and_wf btrue_neq_bfalse assert_functionality_wrt_uiff squash_wf true_wf compose_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin applyEquality functionExtensionality hypothesisEquality universeEquality cumulativity hypothesis unionElimination inlFormation isectElimination functionEquality sqequalRule lambdaEquality productEquality inrFormation instantiate productElimination independent_functionElimination equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation voidElimination independent_pairFormation independent_isectElimination addLevel levelHypothesis dependent_set_memberEquality applyLambdaEquality setElimination rename impliesFunctionality imageElimination natural_numberEquality imageMemberEquality baseClosed allFunctionality promote_hyp because_Cache

Latex:
\mforall{}F:Type  {}\mrightarrow{}  \mBbbB{}
((\mforall{}X,Y:Type.    (X  \msim{}  Y  {}\mRightarrow{}  F  X  =  F  Y))
{}\mRightarrow{}  (\mforall{}X,Y:Type.    (F  X  =  F  Y  \mvee{}  (\mexists{}p:\mBbbN{}\minfty{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(p  n\minfty{})))  \mwedge{}  (\muparrow{}(p  \minfty{})))))))

Date html generated: 2017_10_01-AM-08_29_37
Last ObjectModification: 2017_07_26-PM-04_24_06

Theory : basic

Home Index