Selected Objects

def	lem	lem == PRIMITIVE
def	lem_2	lem_2 == PRIMITIVE
THM	excluded_middle	XM
FIAT	ext_axiom	A = B  A  B & B  A
def	prop_to_bool	P == InjCase(lem(P) ; true; false)
def	prop_to_bool_2	P == InjCase(lem_2(P) ; true; false)
THM	prop_to_bool_char	(P)  P
THM	prop_to_bool_2_char	P:Prop{2}. (P)  P
THM	prop_to_bool_char_2	P:. (P) = P
def	stype	S == {T:Type| x:T. True }
THM	lem_extensionality_axiom	'a:S, P:('aProp). lem('a) = lem({x:'a| True })  'a
def	arb	arb(T) == InjCase(lem(T); x. x, "uu")
def	choose	@x:T. P(x) == InjCase(lem({x:T| P(x) }); x. x, arb(T))
THM	choose_functionality_axiom	T:S, P,Q:(TType). (x:T. P(x)  Q(x))  (@x:T. P(x)) = (@x:T. Q(x))
THM	choose_unique	P:('aType), x:'a. P(x)  (y:'a. P(y)  x = y)  (@y:'a. P(y)) = x
THM	choose_true	P:('aProp), x:'a. P(x)  P(@x:'a. P(x))
THM	choose_elim_neg	'a:S, P,Q:('aProp). (x:'a. Q(x)  P(x))  ((x:'a. Q(x))  (x:'a. P(x)))  P(@x:'a. Q(x))
THM	choose_elim_pos	'a:S, P,Q:('aProp). (x:'a. Q(x)  P(x))  (x:'a. Q(x))  P(@x:'a. Q(x))
def	ball	x:T. P(x) == (x:T. P(x))
THM	assert_of_ball	P:(T). (x:T. P(x))  (x:T. P(x))
def	bexists	x:T. P(x) == (x:T. P(x))
THM	assert_of_bexists	P:(T). (x:T. P(x))  (x:T. P(x))
def	bequal	x = y == (x = y  T)
THM	btrue_neq_bfalse_simp_1	true = false  False
THM	btrue_neq_bfalse_simp_2	false = true  False
THM	assert_of_bequal	x,y:T. (x = y)  x = y
THM	bequal_bools	x,y:. x = y  (x  y)
THM	assert_of_bequal_bools	x,y:. (x = y)  (x  y)
THM	assert_of_btrue	true  True
THM	assert_of_bfalse	false  False
def	type_if	A[P] == PA
def	bif	bif(b; bx.x(bx); by.y(by)) == if b x(*) else y(x.x) fi
THM	ext_simp_1	f,g:('a'b). (x:'a. f(x)) = (x:'a. g(x))  (x:'a. f(x) = g(x))
THM	ext_simp_2	f,g:('a'b). f = (x:'a. g(x))  (x:'a. f(x) = g(x))
def	isr	isr(x) == InjCase(x; y. false; z. true)
def	type_definition	type_definition('a;'b;P;rep) == (x',x'':'b. rep(x') = rep(x'')  'a  x' = x'') == & (x:'a. (P(x))  (x':'b. x = rep(x')))
def	iso_pair	iso_pair('a;'b;P;rep;abs) == (r:'b. abs(r) = (@a:'a. (r = rep(a)))) & type_definition('b;'a;P;rep)
THM	type_def_iso	'a,'b:S, P:('b), rep:('a'b), abs:('b'a). iso_pair('a;'b;P;rep;abs)  (rep':('a'b). type_definition('b;'a;P;rep'))
THM	bnot_bexists	T:S, P:(T). (x:T. P(x)) = (x:T. P(x))
THM	bnot_ball	T:S, P:(T). (x:T. P(x)) = (x:T. P(x))
THM	not_exists	T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))
THM	not_all	T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))
THM	not_and	p,q:. (p & q)  p  q
THM	not_or	p,q:. (p  q)  p & q
THM	not_le_int	i,j:. ij  j<i
THM	not_lt_int	i,j:. i<j  ji
THM	not_not	p:. p  p
THM	iso_pair_char	'a,'b:S, P:('b), rep:('a'b), abs:('b'a). iso_pair('a;'b;P;rep;abs) (a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) = r))
THM	iso_pair_rep_to_abs	'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'a, r:'b. iso_pair('a;'b;P;rep;abs)  rep(a) = r  a = abs(r)
THM	rep_prod_axiom	'a,'b:S. (p:'a'b. a:'a. b:'b. (a = 1of(p))(b = 2of(p))) = (@rep:'a'b'a'b (@((p',p'':'a'b.  ((rep(p')) = (rep(p'')))(p' = p'')) (@(x:'a'b. ((his_pair('a; 'b)(x)) = (p':'a'b. (x = (rep(p'))))))))
def	type_tag	type_tag(x;'a) == x
def	eq_pred	eq('a) == {f:('a'a)| f = (x:'a. y:'a. x = y) }
THM	eq_pred_inc	eq('a)  ('a'a)
THM	eq_pred_char	f:eq('a). f = (x:'a. y:'a. x = y)  'a'a
def	eq_pred_marker	<eq_pred:x> == x
THM	eq_pred_abstraction	P:(('a'a)Prop). P(<eq_pred:(x:'a. y:'a. x = y)>)  (f:eq('a). P(f))
THM	eq_pred_unabstraction	'a:S, P:(eq('a)Prop). (f:eq('a). P(f))  P(<eq_pred:(x:'a. y:'a. x = y)>)
THM	add_eq_pred_qf	P  (f:eq('a). P)
THM	true_and	True & P  P
THM	or_true	P  True  True
THM	false_or	False  P  P
THM	or_false	P  False  P
THM	true_or	True  P  True
THM	and_true	P & True  P
THM	false_and	False & P  False
THM	and_false	P & False  False
THM	imp_false	(P  False)  P
THM	imp_true	(P  True)  True
THM	false_imp	(False  P)  True
THM	true_imp	(True  P)  P
THM	all_true	(x:A. True)  True
THM	all_false	A:S. (x:A. False)  False
THM	exists_false	(x:A. False)  False
THM	exists_explicit_1	x:A. (y:A. y = x)  True
THM	exists_explicit_2	x:A. (y:A. x = y)  True
THM	not_true	True  False
THM	not_false	False  True
THM	eq_refl	t:A. t = t  True
THM	assert_imp_eq_btrue	b:. b  b = true
THM	not_assert_imp_eq_bfalse	b:. b  b = false

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