Nuprl - Proof: Tarski 1 1 1

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

At: Tarski 1 1 1

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))

False

By: Assert (S reps NOT(tr/S))

Generated subgoals:

1 S reps NOT(tr/S) 3 steps

2 9. S reps NOT(tr/S)
False 6 steps

About:

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

1	`S reps NOT(tr/S)`	3 steps

2	9. `S reps NOT(tr/S)` `False`	6 steps