| | Who Cites RepsTruth? |
|
| RepsTruth | Def RepsTruth(L; Tr; tr) == ( S:Term. ( t:Term. S  = t)   L(SUBX(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 = t {Tr(SUBX(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 SUBX(t; e) == t[e/X] |
| | | Thm* t,r:Term. SUBX(t; r) Term |
|
| repst | Def x = y == x = y |
| | | Thm* t,x:Term. (t = 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 = y == x t & x = y t |
| | | Thm* t:(u Term), x:u. (t = x) Prop |
| | | Thm* t,x:Term. (t = x) Prop |
|
| rev_implies | Def P Q == Q P |
| | | Thm* A,B:Prop. (A B) Prop |
