Nuprl - Proof: Tarski 1 1 1 2

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

At: Tarski 1 1 1 2

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

False

By: InstHyp [S] 4 THENA Witness NOT(tr/S) THEN Thin 4

Generated subgoal:

1 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 5 steps

About:

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