Nuprl - Proof: RussellsParadox Frege 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: RussellsParadox Frege 1

1. A : Type
2. Q : A

Prop
3.

P:(A

Prop).

p:A.

x:A. Q(x,p)

P(x)

False

By:	Inst: Hyp:3 Using:[P(x):= Q(x,x)] THEN Reduce Hyp:3

Generated subgoal:

1 4. p:A. x:A. Q(x,p) Q(x,x)
False
4 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html