Nuprl - Proof: Tarski 1 1 1 2 1

(13steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: Tarski 1 1 1 2 1

1. Tr: TermProp
2. tr: Term
3. L: TermProp
4. RespectsNot(Tr; L)
5. ReflectsProp(Tr; tr; Tr)
6. S: Term
7. S = s(NOT(tr))
8. S reps NOT(tr/S)
9. L(tr/S)

False

By: Unfold `ReflectsProp` 5 THEN InstHyp [NOT(tr/S);S] 5 THEN Thin 5

Generated subgoal:

1 5. S: Term
6. S = s(NOT(tr))
7. S reps NOT(tr/S)
8. L(tr/S)
9. Tr(tr/S) Tr(NOT(tr/S))
False 4 steps

About:

(13steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc