| | Who Cites RepsTruth? |
|
| RepsTruth | Def RepsTruth(L; Tr; tr) == ( S:Term. ( t:Term. S reps t)   L(tr/S)) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr) |
| | | Thm* Tr:(Term  Prop), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr)  Prop |
|
| ReflectsProp | Def ReflectsProp(P; qP; Tr) == t,qt:Term. qt reps t {Tr(qP/qt)  Tr(t)} |
| | | Thm* P:(TermProp), 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 |
|
| subx | Def t/e == t[e/X] |
| | | Thm* t,r:Term. t/r Term |
|
| repst | Def x reps y == x reps y Term |
| | | Thm* t,x:Term. (t reps x) Prop |
|
| iff | Def P Q == (P Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
|
| reps | Def x reps y t == x IN t & ref(x) = y t |
| | | Thm* t:(u Term), x:u. (t reps x u) Prop |
| | | Thm* t,x:Term. (t reps x Term) Prop |
|
| rev_implies | Def P Q == Q P |
| | | Thm* A,B:Prop. (A B) Prop |
