Re: Need help with simple FOL proof -- without using existential quantifiers

On 26 Jan 2007 21:36:27 -0800, "Dan Christensen" <dchris@xxxxxxxxx>
wrote:


~Ax~AyRxy -> Ay~Ax~Rxy

1 (1) AyRay A
1 (2) Rab 1 AE
3 (3) Ax~Rxb A
3 (4) ~Rab 3 AE
1,3 (5) Rab & ~Rab 2,4 &I
3 (6) ~AyRay 1,5 ~I

Shouldn't this be ~Ax~Rxb, the negation of the assumption (premise) on
line 3?


No. It's the negation of the assumption in line 1 (which is discharged
by this application of ~I/RAA) but it still depends on assumption 3.


3 (7) Ax~AyRxy 6 AI
8 (8) ~Ax~AyRxy A
3,8 (9) Ax~AyRxy & ~Ax~AyRxy 7,8 &I
8 (10) ~Ax~Rxb 3,9 ~I
8 (11) Ay~Ax~Rxy 10 AI
(12) ~Ax~AyRxy -> Ay~Ax~Rxy 8,11 ->I



F.

--

E-mail: info<at>simple-line<dot>de
.