Selected Objects

Introduction		introductory remarks
def	termin	x t == PRIMITIVE
def	termof	A Term == {t:Term| t A }
THM	termof_wf	(A Term) Type
def	reps	x = y == x t & x = y t
THM	reps_wf	t:(u Term), x:u. (t = x) Prop
def	repst	x = y == x = y
THM	reps_wf2	t,x:Term. (t = x) Prop
THM	repst_wf	t,x:Term. (t = x) Prop
THM	up_reps	t:Term. t = t
THM	up_repst	t:Term. t = t
def	term_closed	closed(t) == s,v:Term. t[s/v] = t
THM	term_closed_wf	t:Term. closed(t) Prop
THM	up_term_closed	t:Term. closed(t)
THM	qup_up_repst	t:Term. UP(t) = t
def	subx	SUBX(t; e) == t[e/X]
THM	subx_wf	t,r:Term. SUBX(t; r) Term
THM	qsubx_repst	t,r,t',r':Term. t = t' & r = r' SUBX(t; r) = SUBX(t'; r')
THM	qnot_subx	t,e:Term. SUBX(NOT(t); e) = NOT(SUBX(t; e))
def	f	f(t) == SUBX(t; SUBX(X; UP(X)))
THM	f_wf	t:Term. f(t) Term
def	s	s(t) == SUBX(f(t); f(t))
THM	s_wf	t:Term. s(t) Term
THM	s1	t:Term. s(t) = SUBX(t; SUBX(f(t); UP(f(t))))
THM	s2	t:Term. s(t) = SUBX(t; SUBX(f(t); f(t)))
THM	s_reps	t:Term. s(t) = SUBX(t; s(t))
def	RespectsNot	RespectsNot(Tr; L) == t:Term. Tr(NOT(t)) L(t) & Tr(t)
THM	RespectsNot_wf	Tr,L:(TermProp). RespectsNot(Tr; L) Prop
def	ReflectsProp	ReflectsProp(P; qP; Tr) == t,qt:Term. qt = t (Tr(SUBX(qP; qt)) Tr(t))
THM	ReflectsProp_wf	P:(TermProp), qP:Term, L:(TermProp). ReflectsProp(P; qP; L) Prop
def	RepsTruth	RepsTruth(L; Tr; tr) == (S:Term. (t:Term. S = t) L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)
THM	RepsTruth_wf	Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr) Prop
THM	prop_and_iff	B (A B & C) (A C)
THM	prop_iff_trans	(A B) (B C) (A C)
THM	prop_iff_contra	(P P) False
THM	Tarski	(Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))