I had the first post on rec.arts.sf.tv.quantum-leap .
The old newsgroup was called alt.tv.quantum-leap .

11.  Universal Elimination.Imagine S to be a well-formed logical statement.
     If I know (Ax)S, I can derive S(u/x).

12.  Universal Introduction.  If I can derive S(u/x) and u does not appear free in any given or
     assumptions so far, I can derive (Ax)S.
     In other words, if I can prove Pu and and u is so arbitrary that it
     does not appear in any assumptions so far, I can conclude (Ax)Px.
     If I know something is true about an element in the universe that
     is so random that I don't know any specific details about that
     element, then it must be true for all elements in the universe.

Given (Ax)(Px & Qx)
Derive:  (Ax)Px & (Ax)Qx

1.  Given (Ax)(Px & Qx)
2.  (Ax)(Px & Qx) (Given 1)
3.  Pu & Qu (2)
4.  Pu (3)
5.  (Ax)Px (4)
6.  Qu (3)
7.  (Ax)Qx (6)
8.  (Ax)Px & (Ax)Qx

1.  Conjunctive Elimination (If I know P & Q, I can derive P; I can derive Q)
2.  Conjunctive Introduction  (If I know P and I know Q, I can derive P&Q)
3.  Disjunctive Introduction (If I know P, I know P v Q;  I also know Q v P.)
4.  Disjunctive Elimination (If I know P v Q, and I can, assuming P, derive R, and assuming Q, derive R, than I can derive R.)
5.  Negation Elimination (If I know ~~P, I can derive P.)
6.  Negation Introduction (If, assuming P, I can derive Q and ~Q, I can deduce ~P).
7.  Conditional Elimination (If I know P=>Q and I know P, I can derive Q.)
8.  Conditional Introduction (If, assuming P, I can derive Q, then I can deduce P=>Q.)
9.  Biconditional Elimination (If I know P<=>Q, and I know P, I can derive Q.  If I know P<=>Q, and I know Q, I can derive P.)
10.  Biconditional Introduction (If assuming P, I can derive Q, and assuming Q, I can derive P, I can deduce P<=>Q.)


13.  Existential Introduction.  If I know S(u/x), I can derive (Ex)S.

In other words, if I know that Pu is true for some--ANY--value
of u, I know (Ex)Px.

14.  Existential Elimination.  If I know (Ex)S AND assuming S(u/x) I can derive T AND u does not appear free in T, S, or the assumptions or givens, I can deduce T.

In other words, If I know that Px is true for SOME value of x somewhere, I can, temporarily, assume a variable that makes it true, but I can't assume any specific properties of that variable; it has to be completely arbitrary.

Given:  there exists a red car.
Prove:  there exists a red Pontiac

OK, so I know there exists a red car.  Assume it's a Pontiac.  Therefore, there must be a red Pontiac.  BAD PROOF.


Given:  (Ex)(Px v Qx)
Prove:  (Ex)Px v (Ex)Qx

1.  Given (Ex)(Px v Qx)
2.  (Ex)(Px v Qx) (Given 2)
3.  	Assume Pu v Qu  <== Something makes line 2 work; for now, I'm calling it u.
4.	Pu v Qu (Assumption 3)
5.		Assume Pu
6.		Pu (Assumption 5)
7.		(Ex)Px (EI,6)
8.		(Ex)Px v (Ex)Qx (vI,7)

9.		Assume Qu
10.		Qu (Assumption 9)
11.		(Ex)Qx (EI,10)
12.		(Ex)Px v (Ex)Qx (vI,11)
13.	(Ex)Px v (Ex)Qx (vE,4,5-8,9-12) <== There are no u's in it
14.  (Ex)Px v (Ex)Qx (EE,2,3-13)


Given nothing:
Prove:  ~(Ax)Px <=> (Ex)~Px


1.	Assume (Ex)~Px
2.	(Ex)~Px (Assumption 1)
3.		Assume ~Pu
4.		~Pu (Assumption 3)
5.			Assume (Ax)Px
6.			(Ax)Px (Assumption 5)
7.			Pu (AE,6)
8.		~(Ax)Px (~I,5-(7,4))
9.	~(Ax)Px (EE,2,3-8)

10.	Assume ~(Ax)Px
11.	~(Ax)Px (Assumption 10)
12.		Assume ~(Ex)~Px
13.			Assume ~Pu
14.			~Pu (Assumption, 13)
15.			(Ex)~Px (EI,14)
16.			~(Ex)~Px (Assumption 12)
17.		~~Pu (~I,13-(15,16))
18.		Pu (~E,17)
19.		(Ax)Px (AI,18)
20.	~~(Ex)~Px (~I,12-(11,19))
21.	(Ex)~Px (~E,20)
22.  ~(Ax)Px <=> (Ex)~Px (10-21,1-9)