Selected Objects

THM	negnegelim_vs_bivalence	Double negation elimination is equivalent to bivalence. (P:Prop. P  P)  (P:Prop. P  P)
THM	disjunct_elim	P  Q  P  Q
THM	or_fused	Q  Q  Q
THM	guarded_prop_to_prop	The precise type of implication Q:Prop(given P). P  Q  Prop
THM	decidable__cand	Q:Prop(given P). Dec(P)  (P  Dec(Q))  Dec(P & Q)
THM	cand_is_prop	B:Prop(given A). (A & B)  Prop
def	equiv_rel_sep	EquivRel on A, R == EquivRel u,v:A. R(u,v)
def	allst	x:A st P(x). Q(x) == x:A. P(x)  Q(x)
def	allst_implicit	Q(x) ==  x:A st P(x). Q(x)
def	product_conventional_notation	product_conventional_notation(A; x.B(x)) == x:AB(x)
def	quotient_sep	A/E == u,v:A//E(u,v)
THM	decbl_iff_some_bool	Dec(P)  (b:. b  P)
def	isect_two	Intersection of two types AB == i:2. if i=0 A else B fi
THM	not_over_exists_imp	(x:T. Q(x))  (x:T. Q(x))
def	exteq	Extensional equality between types A =ext B == (x:A. x  B) & (x:B. x  A)
THM	exteq_sigma_st_dom	B:(AType), P:(AProp). (i:{i:A| P(i) }B(i)) =ext {v:(i:AB(i))| P(v/x,y. x) }
THM	singleton_eq_in_self	x:{a:A}. x = a  {a:A}
THM	singleton_singleton_self	{a:{a:A}} =ext {a:A}
def	fun_over_st	x:A st P(x)B(x) == x:{x:A| P(x) }B(x)
def	inhabited	(type A has a member) A == A
THM	inhab_choice	(x:A. B(x))  ((x:AB(x)))
THM	inhab_rep_axiom	A:Type{i}. P = (A)  Prop
THM	inhab_rep_eqv	F:(Prop{i}Prop{j}). (P:Prop{i}. F(P))  (A:Type{i}. F(A))
THM	inhabited_vs_exists	(A)  (x:A. True)
def	inhabited_uniquely	(type A has exactly one member) !A == {x:A| y:A. x = y }
THM	inhabited_uniquely_vs_exists	(!A)  (x:A. y:A. x = y)
THM	inhabited_uniquely_elim	(!A)  (x:A. y:A. x = y)
THM	unique_fn_over_empty	(A)  (!(AB))
THM	not_sq_iff_sq	P  P
THM	sq_not_iff_sq	(P)  P
THM	dec_imp_dec_sq	Dec(P)  Dec(P)
THM	sq_sq_iff_sq	P  P
THM	set_inc_wrt_imp	(x:A. B(x)  B'(x))  {x:A| B(x) }  {x:A| B'(x) }
def	xor	P XOR Q == P  Q & (P & Q)
THM	xor_vs_neg_n_dec	P XOR Q  (Q  P) & Dec(P)
THM	exteq_subset_vs_and	{x:{x:A| P(x) }| Q(x) } =ext {x:A| P(x) & Q(x) }
THM	subset_exteq	(x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })
THM	subset_to_squash	x:{x:A| B(x) }. B(x)
THM	squash_to_subset	x:A. B(x)  x  {x:A| B(x) }
THM	set_inc_wrt_imp_sq	(x:A. B(x)  B'(x))  {x:A| B(x) }  {x:A| B'(x) }
THM	subset_sq_exteq	(x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })
THM	subset_squash_exteq	{x:A| P(x) } =ext {x:A| P(x) }
THM	ifthenelse_distr_subtype	{x:A| if b P(x) else Q(x) fi } =ext if b {x:A| P(x) } else {x:A| Q(x) } fi
def	is_discrete	(equality over type A is effectively decidable) A Discrete == x,y:A. Dec(x = y)
THM	discrete_vs_bool	(A Discrete)  (e:(AA). x,y:A. (x e y)  x = y)
THM	discrete_vs_bool2	(A Discrete)  (e:(AA). IsEqFun(A;e))
def	pure_let	A form for function application with a special place for the argument let xa in b(x) == b(a)
def	pure_let2	let xa, yb in c(x;y) == c(a;b)
THM	no_prop_iff_its_neg (Proof Gloss)	No proposition is equivalent to its own negation. (P  P)
THM	RussellsParadox_Frege	Russell's Paradox There is no way to represent the all properties over a class by members of the class. (A:Type, Q:(AAProp). P:(AProp). p:A. x:A. Q(x,p)  P(x))
THM	RussellsParadox_Frege2	Russell's Paradox Full comprehension for sets is impossible. That is, there is no notion of set such that for every property of sets there is a set consisting of the sets having that property. (Set:Type, :(SetSetProp). (P:(SetProp). p:Set. x:Set. (x  p)  P(x))
THM	equivrel_characterization	A compact characterization of equivalence relations. R:(AAProp).  (EquivRel x,y:A. R(x,y)) (x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z))))
def	is_the	(x is the unique A such that P(x)) x is the u:A. P(u) == P(x) & (u:A. P(u)  u = x)
def	exists_unique	(there is a unique x in A such that P(x)) !x:A. P(x) == x:A. x is the x:A. P(x)
THM	exists_unique_elim	P:(AProp). (!u:A. P(u))  (y,z:A. P(y)  P(z)  y = z)
THM	dec_pred_iff_some_boolfun	A property is effectively decidable just when it is characterized by a boolean-valued function. (x:T. Dec(E(x)))  (f:(T). x:T. f(x)  E(x))
THM	dec_pred_imp_bool_decider_exists	P:(AType). (x:A. Dec(P(x)))  (!{p:(A)| x:A. p(x)  P(x) })
THM	inhabited_uniquely_vs_exists_unique	(!A)  (!x:A. True)
THM	indep_fun_extensional	Defintion of equality between functions. f,g:(AB). f = g  (x:A. f(x) = g(x))
THM	dep_ax_choice_version2	A choice principle. (x:A. y:B(x). Q(x,y))  (f:(x:AB(x)). x:A. Q(x,f(x)))
THM	fun_description	Existence of functions through description. (x:A. !y:B(x). P(x,y))  (f:(x:AB(x)). x:A. P(x,f(x)))
THM	unique_fun_description	B:(AType), P:(x:AB(x)Prop). (x:A. !y:B(x). P(x,y))  (!f:(x:AB(x)). x:A. P(x,f(x)))
THM	unique_fun_description2	B:(AType), P:(x:AB(x)Prop). (x:A. !y:B(x). P(x,y))  (!{f:(x:AB(x))| x:A. P(x,f(x)) })
THM	ax_choice_version2	A choice principle. (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))
THM	ax_choice_version3	A choice principle. (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))
THM	indep_fun_description	(x:A. !y:B. P(x,y))  (f:(AB). x:A. P(x,f(x)))
THM	unique_indep_fun_description	A,B:Type{i}, P:(ABProp{i}). (x:A. !y:B. P(x,y))  (!f:(AB). x:A. P(x,f(x)))
THM	range_restriction_dep	Typing a function with its range type. B:(AType), f:(x:AB(x)). f  x:A{f(x):B(x)}
THM	range_restriction_indep	Typing a function with its range type. f:(AB). f  A{y:B| x:A. f(x) = y }
def	diagonalize	Diagonalization (Diag f wrt y. e(y))(x) == e(f(x,x))
THM	diagonalization	R:(BBProp), e:(BB). (b:B. R(e(b),b)) (A:Type, f:(AAB). (a:A. R((Diag f wrt x. e(x))(a),f(a,a))))
THM	diagonalization_wrt_eq	e:(BB).  (b:B. e(b) = b) (A:Type, f:(AAB). (a:A. (Diag f wrt x. e(x)) = f(a)))

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html