| | Some definitions of interest. |
|
| ReflectsProp | Def ReflectsProp(P; qP; Tr) ==  t,qt:Term. qt reps t   {Tr(qP/qt)  Tr(t)} |
| | | Thm* P:(Term  Prop), qP:Term, L:(TermProp). ReflectsProp(P; qP; L)  Prop |
|
| RespectsNot | Def RespectsNot(Tr; L) == t:Term. Tr(NOT(t)) L(t) &  Tr(t) |
| | | Thm* Tr,L:(TermProp). RespectsNot(Tr; L) Prop |
|
| iff | Def P Q == (P Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| repst | Def x reps y == x reps y Term |
| | | Thm* t,x:Term. (t reps x) Prop |
|
| s | Def s(t) == f(t)/q(f(t)) |
| | | Thm* t:Term. s(t) Term |
|
| subx | Def t/e == t[e/X] |
| | | Thm* t,r:Term. t/r Term |
