Ok, thank you so much for your time. You have been helpful, although I will reread your reply since the numbers on the left really confuse me. I will also ask my professor if I can avoid those numbers at the time of the exam. Unfortunately, I can't attend the logic class (since I can't leave work three times a week), and Forbes does not explain every detail in his book (I am a good reader, believe me).

By the way for proofs where I have to show that x=y, I suppose that x and y should pick the same referent. In other words, in a premise like (Ax)(Fx-->(Ey)(Gy & x=y)), I guess it is legitimate and helpful to substitute Fx with Fa and Gy with Ga (where both F and G predicates pick the same referent "a" and it becomes easy for me to show that x=y). Right?

Thank you again!

As I said, all help is appreciated for a beginner like me... and details are really important. Below I bring the second proof that gave me some hard time, since I am not sure what is the exact route of turning "=" into "≠". In the book I am given only the conclusion, no premises, and I try to solve it with some legitimate assumptions. I would greatly appreciate it if you or anyone else takes a little time with my solution to the exercise : Show |--NK (Ax)(Ay)((Fx & ~Fy)-->x≠y)

My proof:
1) Fa & ~Fb................................assumption
2) a=b..........................................assumption
3) Fa.................................. ........1&E
4) ~Fb................................ ........1&E
5) Fb............................................2,3 =E
6) ^^^contradiction^^^^.................. 4,5~E
7) ~(a=b)......................................2,6 ~I
8) (Fa & ~Fb)---> ~(a=b)....... ......1,7-->I
9) (Ay) ((Fa & ~Fy)--->a≠y).... ......8 AI -(as I said I am not sure how "=" turns into "≠" in a proof)
10) (Ax)(Ay)((Fx & ~Fy)---> x≠y)... 9 AI

jkg20

Insofar as everything depends on the details, I think you have been helpful already. My weakest point are assumptions (and I am confused with many braces and quantifiers as well). In the same book I am asked to show that |--NK (Ax)(Ay)((Fx & ~Fy)-->(x≠y) and again I am a little confused on whether (x≠y) can be equal to ~(x=y).

I guess in order to get such a conclusion I should start with: premise 1) Fa & ~Fb, premise 2) ~(a≠b). With the second premise I don't know what kind of proof or rules I may use (the chapter is referred to identity elimination rule =E), but I am not sure if premise 2 can be (a=b) --hoping to bring its opposite through introducing a negation (since I really do not know other way to turn = to ≠ in a proof).

Any ideas/suggestions on this last question? (I will try to solve it by myself also and hopefully will keep you updated).

Thank you for your support!

Nagase forgot this discussion :worry:

Anyone else willing to help?

Thanks!

Ok here is the solution I "found", without any sequent introductions... There seem to be many assumptions and I hope I have discharged them all.

1) (Ax)[(Ey)Tyx-->(Az)~Txz] premise
2) (Ax)[(Ey)Tyx-->Txx premise
3)(Ey)Tya-->Taa 2AE (viz. universal elimination of 2)
4) Tba-->Taa assumption
5)Tba assumption
6) Taa 4,5 -->E
7)(Ey)Tya-->(Az)~Taz 1AE
8) Tba-->(Az)~Taz assumption
9)Tba assumption (I assume it a second time since I am not sure if I should use line 5, already discharged, again)
10) (Az)~Taz 8,9 -->E
11) ~Taa 10AE
12) ^^^contradiction^^^ of 6 and 11
13) ~Tba 5,12~I
14) (Ay)~Tby 13AI
15) (Ax)(Ay)~Tby 14AI
16) (Ax)(Ay)~Tby 3,4,15 EE (viz. existential elimination)
17) (Ax)(Ay)~Tby 7,8,16 EE

By the way, these exercises do not help me pass the exam. I have to resolve them in order to make sense of everything and be able to interpret all the problems I will be given in the exam. Hence, I'd appreciate any corrections in my argument. Thank you again!

Ok, I appreciate your help. This is the example I am trying to resolve (from G. Forbes' book, p. 268, no answer is given though the author says there are 4 solutions/symbolizations).

With "Ax" are meant universal quantifiers, and with "Ex" existential quantifiers.

(Ax)[(Ey)Tyx--then-->(Az)~Txz], (Ax)[(Ey)Tyx--then-->Txx] |--NK (Ax)(Ay)~Txy

Thank you so much!!!