Selected Objects

Introduction		introductory remarks
def	termin	x IN t == PRIMITIVE
def	termof	A Term == {t:Term| t IN A }
THM	termof_wf	(A Term) Type
def	reps	x reps y t == x IN t & ref(x) = y t
THM	reps_wf	t:(u Term), x:u. (t reps x u) Prop
def	repst	x reps y == x reps y Term
THM	reps_wf2	t,x:Term. (t reps x Term) Prop
THM	repst_wf	t,x:Term. (t reps x) Prop
THM	up_reps	t:Term. q(t) reps t Term
THM	up_repst	t:Term. q(t) reps 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. Q(q(t)) reps q(t)
def	subx	t/e == t[e/X]
THM	subx_wf	t,r:Term. t/r Term
THM	qsubx_repst	t,r,t',r':Term. t reps t' & r reps r' SUBX(t; r) reps t'/r'
THM	qnot_subx	t,e:Term. NOT(t)/e = NOT(t/e)
def	f	f(t) == SUBX(q(t); SUBX(X; Q(X)))
THM	f_wf	t:Term. f(t) Term
def	s	s(t) == f(t)/q(f(t))
THM	s_wf	t:Term. s(t) Term
THM	s1	t:Term. s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))
THM	s2	t:Term. s(t) reps t/(f(t)/q(f(t)))
THM	s_reps	t:Term. s(t) reps 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 reps t (Tr(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 reps t) L(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))