First of all you don't ever substitute quantifiers like " -(Ex)", you substitute only the variables bound by quantifiers (in this case "x"), so you don't ever substitute negations as such - you cannot negate an object, you can only negate sentences concerning objects.

Secondly, if you have a quantified sentence in first order predicate logic which is negated, you should transform the statement into an appropriately non-negative quantified sentence where the negation covers the statements over which the quantifiers have scope. As per my previous post, these are the basic rules to remember for transferring negated quantifications over statements into quantifications over negated statements:
-Ex(Fx) = Ax-(Fx)
-Ax(Fx) = Ex-(Fx)

So when you have :
-(Ex)(Ey)(x≠y & (Fx & Fy))
the negation at the beginning covers the entire sentence, and so is equivalent to
AxAy-(x≠y & (Fx & Fy))
If you now substitute x with a you get
Ay-(a≠y & (Fa & Fy))
Notice that the negation stays where it is, covering the entire compound statement over which the quantifiers have scope, and does not attach itself individually to the substitutions that are made.

I hope that clarifies things a little.

Ok. You have been very clear with the last two replies. Let us hope I can remember all those shift quantifiers --if in the test I'll have to deal with something similar to the domain with four objects.

With regard to your last reply, I am wondering if I can apply Double Negation to Ay-(a≠y & (Fa & Fy))...
viz:
1) Ay-(a≠y & (Fa & Fy)) (your suggestion)
2) -(a≠b & (Fa & Fb)) 1 AE for Uni Elim
3) a=b & (Fa & Fb) 2 DN

If step 3 is legitimate application of DN to step two, I think I have hopes to prove the conclusion....

The exercise I am trying to resolve is this: (Ex)Fx, -(Ex)(Ey)(x≠y & (Fx & Fy)) |-nk (Ex)(Ay)(x=y <->Fy)

I guess that since the conclusion is a biconditional, I may also assume one of its conditionals (viz. a=b-->Fb) with the hope of getting later the other way around (viz. Fb--> a=b), connect the two conditionals with &I rule, and get a binconditional with the biconditional intro rule (aka DF - rule of defnitions). That's my strategy, but there may be sequent introductions as well (which I do not remember very well) and I am not sure if the DF rule will help in discharging my assumption (a=b-->Fb). There may be other ways as well. I better try them tomorrow morning. I was wondering, however, what one may assume when the conclusion is a biconditional.

The negation in 2) above has widest scope of all the logical operators, so
-(a≠b & (Fa & Fb)) is not equivalent to
a=b & (Fa & Fb)
but to
(a=b V -(Fa & Fb))

a=b & (Fa & Fb) would be inferrable from (-(a≠b) &(Fa & Fb)) where the negation has scope only over the statement a≠b.

As for the technique to follow for the exercise, it is basically saying that given the two premises, the sequent follows. In this kind of circumstance it is often a good technique to make the assumption that the sequent is false and then aim to draw out a contradiction. So, I would try beginning your proof with
1) Ex(Fx) Premise
2) -(Ex)(Ey)(x≠y & (Fx & Fy)) Premise
3) -(Ex)(Ay)(x=y <->Fy) Assumption

and seeing how you can progress from there to get a contradiction which will allow you to discharge assumption (3) by negation and thus infer by double negation the sequent (Ex)(Ay)(x=y <->Fy). Bear in mind that the negation in 2) and 3) has widest scope and covers the entire statement in both cases, not just the identity statements.

Concerning your general remarks about proving biconditionals, certainly the way to do that is to prove both the conditionals, but in this case I'm not sure that would be the simplest way to go about the proof.

Remember, though, that in this case you are aiming to prove syntactic entailment, so you can only use the rules you've been given, so (unless you've been given them as a rule to use) you cannot just help yourself to my "short cuts" concerning conversion of negated quantifiers. Those short cuts are useful when one is dealing with proofs of semantic entailment (double turnstiles "|=", not single turnstiles "|-") where one is allowed to argue less formally in terms of interpretations.

Ok, I will give it a try after your suggestions and see where it leads.

One last question I have is whether it is legitimate in proofs to take three different variables (x,y,z) as being offered to two objects only (a,b,a)? I know that we can safely do that when we want to show that an argument is invalid, but I want to make sure if I can do that in provability as well. In the second post of this discussion, I brought such a proof that you saw and partly approved, but in the case that it slipped your attention here below I have attached the two premises where I take x and z as referring to the same object a..:

1) (Ax)[(Ey)Tyx-->(Az)~Txz] premise
2) (Ax)[(Ey)Tyx-->Txx premise

In the following lines I substitute the consequent (Az)~Txz with ~Taa and consequent Txx with Taa, in order to pave the way for the conclusion (Ax)(Ay)~Txy. But is it legitimate ?

Hi
If you mean that from 1) above you first use the universal elimination rule to derive
3) Ey(Tya->Az~(Taz))
and then use it again on 3) to get
Ey(Tya ->~(Taa))
Then that is fine, you have just used the universal elimination rule twice.
Generally speaking all you have to remember when applying universal elimination is that all of the occurrences of the variable bound by the quantifier must be replaced by the same name - in universal elimination you are free to choose the name you use to replace the bound variable, and that means you are free to choose a name you have already used. So if you have AxAyAz(......) you can replace all the x's with a all the y's with b and all the z's with a if it helps you prove what you are aiming to prove.

Good luck with the exam, by the way.

Thank you for your wishes, but the last exercise is not heading anywhere. It is 7:30 PM here, and I started working on the last exercise from 5 PM, without any success (unless I bring two disjunctions and 29 lines of proving). I will ask my professor also, cause either I am not good at quantifier shifts or there is some sequent intro I forget.

I am talking about: "1) Ex(Fx) Premise2) -(Ex)(Ey)(x≠y & (Fx & Fy)) Premise
3) -(Ex)(Ay)(x=y <->Fy) Assumption" which you suggest that I should resolve through turning -(Ex)(Ey)(x≠y & (Fx & Fy)) into (Ax)(Ay)~(x≠y & (Fx & Fy)) and through bringing a contradiction for the assumption at line three. I fail to do all this. Either I omit some details, or my mind is really slow lol

I will ask professor as well, to see what I do wrong.

I am happy to let you know that I passed the exam, and the questions turned to be much more easier than the ones we have been discussing here. Thank you so much for your time and patience! From this discussion I became aware that I should show more attention to the way I used/discharged assumptions, and that helped a lot in order to succeed in the exam. Enjoy your summer!

Congratulations, that's great news - the work you put in paid off. Now you can get on with enjoying some real philosophy ;-)

Incidently, I'd be interested to know what your prof told you regarding that last exercise we were struggling with - I only gave it a few moments of thought, admittedly, but even on the technique I suggested (negating the sequent as an assumption and aiming to find a contradiction) it looked like being a very long and tortuous proof. Did your prof have anything to say about finding an easier proof?

I lost my interest in logic already lol (all my interest was confined to the exam)

I already threw away all my notes on logic. But if I remember well, the only way to come with up with a contradiction in that sentence was through negating assumption Fb (for FY) three times, and bring a contradiction with the vE discharge... it took me more than 29 lines to do that.

Professor said he would work on it and answer later, but he never answered to my question...