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

On 27 Jan 2007 14:28:14 -0800, "Dan Christensen" <dchris@xxxxxxxxx>
wrote:


I guess, in your system the following proof should go through:

(1) | ~Ax~AyRxy A
(2) | | Ax~Rxb A
(3) | | ~Rab 2 AE
(4) | | | AyRay A
(5) | | | Rab 4 AE
(6) | | ~AyRay 4,3,5 RAA
(7) | | Ax~AyRxy 6 AI
(8) | ~Ax~Rxb 2,1,7 RAA
(9) | Ay~Ax~Rxy 8 AI
(10) ~Ax~AyRxy -> Ay~Ax~Rxy 1,9 ->I


Here is the link to my version: http://www.dcproof.com/frege.html

Right. If we use a version of RAA which is applied upon an explicitly
stated contradiction (i.e. a statement of the form A & ~A), we will
get the following proof:

(1) | ~Ax~AyRxy A
(2) | | Ax~Rxb A
(3) | | ~Rab 2 AE
(4) | | | AyRay A
(5) | | | Rab 4 AE
(6) | | | Rab & ~Rab 3,5 &I
(7) | | ~AyRay 4,6 RAA
(8) | | Ax~AyRxy 7 AI
(9) | | Ax~AyRxy & ~Ax~AyRxy 1,8 &I
(10) | ~Ax~Rxb 2,9 RAA
(11) | Ay~Ax~Rxy 10 AI
(12) ~Ax~AyRxy -> Ay~Ax~Rxy 1,11 ->I


F.

--

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