Help with logic exam:

It'd be nice if you provided the specific rules that you are working with. This may sound surprising, but there are a lot of natural deduction systems out there, each one with its own idiosyncrasies, so it'll be hard to help without seeing the specific system with which you are working. Some examples of what you are attempting to do would be nice, too. That said, I'd say that at least with regards to question 2, the answer is probably yes.

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!!!

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!

Nagase forgot this discussion :worry:

Anyone else willing to help?

Thanks!

Reply to Eros1982 You discharge assumption (4) at step (6) by relying on assumption (5). You discharge assumption (8) at your step (10) but again you should be relying on (5) to do the discharging, you should not introduce (9). Since you now get your contradiction, and you only have assumption (5) left undischarged, you can discharge it by negating it. Does that help?

So, up to (8) everything is fine (except you forgot to close the brace at (2) - I know its nitpicking, but that's what formal logic requires). After (8) you should have:
(9) (Az)~Taz
(10) ~Taa
After that it depends what system of rules you are using, but when I learnt logic you would then do
(11) Taa & -Taa
(12) -Tba

The system I learnt also required that one list explicity at the end of each line which premises and assumptions were still "in play" in arriving at the line itself, which you are not doing above, but as Nagase says, it depends on the rules you've been given.

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!

Reply to jkg20

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

"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!"
- Eros1982

Sometimes I'm so glad that I have never taken a logic in philosophy course or something like it since it would likely make me hate the entire subject and make me never what to do it again for the rest of my life. When I was studying electronics I LOVED doing things like digital circuits, but it didn't have half the madness that logic entails.

While it is unlikely you will heed this advice, IMHO I believe it is best that you reading and writing about philosophy other than what you are doing to earn your degree on your own terms and doing what interests you. For if you don't there is a good chance that it will all will become just 'work' to you and it will become just as boring and tedious as whatever you did before you did for the government before you enrolled in the program you are now in.

OK, Eros, first thing is that after taking a quick look at the way Forbes gives his answers, each line of your answers need to be structured in the folloing way:
a/p1, a/p2, .... ( N ) Statement l1, l2... L/P1 L/P2...
a/p1 on the left refers to the undischarged assumptions or premises that support the Statement. N) is just the line number of the argument. l1,l2 refer to the preceding line numbers of the argument you are giving that are being used to make the Statement, and L/P1... to the logical laws/statement types you are availing yourself of or making. If you don't follow that form in all your answers you will be penalized in your examination. Depending how strict your examiners are you may not get a single mark: "almost right" doesn't cut it in formal logic. Here is a simple example using propositional rather than predicate logic, but which will give you the basic idea:
1 (1) A ? B Premise
2 (2) A? C Premise
3 (3) A Assumption
1,3 (4) B 1,3 ?E
2,3 (5) C 2,3 ? E
1,2,3 (6) B & C 4,5 &I
1,2 (7) A ? (B &C) 3,6 ?I

So take a look at line (6) for instance. ON the right we see that we are using steps 4 and 5 of the argument plus the law of conjunction introduction. However, on the left we must list the assumptions or premises that allow us to make the statement, and here we are relying on the two premises we introduced and the assumption we made, lines 1, 2 and 3. At line (7) we use the implication introduction rule plus lines (3) and (6), but since the implication introduction rule tells us that in introducing an assumption as the antecedent of an implication, we discharge that assumption, on the left we now only need to list (1) and (2) as the steps of the argument we are still relying on (i.e. just our two initial premises).

Exactly the same principles apply to arguments in predicate logic, but you have extra/differently expressed laws of inference (universal and existential introduction/elimination for instance). You need to get into the habit of using precisely the same format in your answers.

I was a little confused as to why you had a separate line to state the contradictions you draw, but I see from Forbes's examples that this is how he has specified the Law of Non Contradiction - the system I used didn't require a separate line for stating the contradiction, you could simply refer back to the individual lines where the two contradictory statements were initially made. Anyway, that changes nothing, it's a matter of taste, but since you will be marked according to Forbes's system, you should continue to do as you are doing and express the contradiction explicitly on its own line (although I would use the actual symbol Forbes introduces for this, which looks like an elaborate "^" . If you want to do that in any subsequent posts, go ahead, I'll understand.)

As for getting from -(a=y) to a?y, you need to look at exactly how Forbes deals formally with the law of identity, my guess is that he defines somewhere a rule that allows you to use the sign for non-identity (?) as logically equivalent to the negation of an identity -(x=y). I don't have a copy of the book, and the excerpts I can get online are limited, so you are on your own there I'm afraid.

So, first off, skim the Forbes to see what he has to say about the law of identity, and then redo both your solutions in the format that Forbes requires. Then we can see if there are any other issues to address.

Reply to jkg20

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!

Reply to Eros1982 You're welcome - actually enjoyed dredging up memories of undergraduate mathematical logic (I was pretty good at it back in the day :wink: ). If you are confused about the numbers on the left, ask me a question about them - you might find that in framing the question you arrive at the answer yourself, but if not, I'll be happy to respond as best I can.

As to your second paragraph above, I'm not quite sure what you are asking me, sorry. If you have this premise :
(Ax)(Fx-->(Ey)(Gy & x=y))
You can derive
(Fa-->(Ey)(Gy & a=y))
by univeral elimination. Universal elimination allows you to substitute a constant term or name ('a') for a variable (in this case 'x') wherever that variable is bound by the universal quantifier. However, you cannot get from
(Fa-->(Ey)(Gy & a=y))
to
(Fa-->Ga & a=a))
by making the same substitution - no rule of inference I know of would warrant that step.

Reply to jkg20

Professor said that I can avoid the dependency numbers (on the left) in my exam :) This is good news, because when you have many assumptions in a proof you have to take your time looking which ones are not discharged yet in order to enlist them on the left (with the other numbers where the current line depends). The are almost 20 questions to be answered in two hours, and the more time I save the better :) I may come up with a few more issues in the near future.

Everyone enjoy your weekend!

Reply to jkg20

Ok I resolved the last exercise by myself, it turned to be easy.

Now there is one more conclusion. This is what I should prove (through using =E or =I rules):
|--nk (Ax)(x=b --> x=c)-->b=c

One way of proving this is...
1) (Ax)(x=b --> x=c)............. assumption
2) (a=b)--> (a=c)................ 1AE
3) a=b................................ assumption
4) a=c.................................2,3 -->E
5) b=a....... ........................3 COM (law of commutation)
6) b=c................................4,3 =E
7) (Ax) (x=b-->x=c)-->b=c

Does it look good?

I hope I am not boring you --you said you enjoyed memories from your undergraduate years (before you turned into a scientist I guess :), and I am trying all the available means in order not to fail again in the logic exam...

Reply to Eros1982 The problem as I see it with your answer is that you have the undischared assumption at line (3) still lingering around by the time you get to line 7. I think one way of doing might be as follows
1 (1) a=b Assumption
2 (2) a=c Assumption
1,2 (3) b=c 1,2 IE
2 (4) (a=b -> a=c) 1,2 ->I
(5) (a=b -> a=c) -> b=c 4,3 ->I
(6) Ax(x=b -> x=c)-> b=c 5, AI

I discharge all my assumptions by line (5) using conditional introduction, and since (5) depends on no undischared assumptions or any premises, I can use universal introduction to replace all occurrences of a.

As an aside, one good general technique when what you are aiming to prove is a conditional statement, you should be looking to make the antecedent of the conditional an assumption, and the negation of the consequent your second assumption, and then look to draw a contradiction. But in this case that doesn't seem necessary.

Reply to jkg20

It seems I am not well acquainted with discharging assumptions, and that's the real issue here. I thought that I had discharged assumption of line 3 on line 4, where I apply existential elimination rule on lines 2 and 3... but you say that 3 is not discharged. I will google more about dischrging assumptions, but it would be helpful if you could tell me why line 4 is not considered a discharge of the assumption in line 3. Can you do that?

Thank you again for your time!!!

Hi. Discharging assumptions basically means that you are no longer relying on the "fact" that they are true. Let's try putting your proof into "natural language". You have
2) If John is Jane, then John is Janice. (by Universal elimination)
3) John is Jane. (Assumption)
Given assumption (3) is true, then you infer:
4) John is Janice
from the conditional elimination rule applied to the conditional (2).
This is fine. However, the conditional elimination rule does not allow you to discharge assumptions. In using that rule you are in effect relying on the truth of the antecedent (in this case that John is Jane). So, the statement (4) that John is Janice is relying on your assumption that John is Jane.

There are three principle ways of discharging assumptions: conditional introduction, negation and existential elimination. I won't deal with the latter, as it is one of the more complicated inference rules, and to get an idea of what's going on with assumption discharge, we don't need to look into its deatils. So, for negation, if you introduce an assumption in your argument:
John is Jane
and then later on in the argument , one way or another - it doesn't matter how as long as you follow the rules - you arrive at the statement
It is not the case that John is Jane (or more colloquially, John is not Jane)
you have gotten rid of your initial assumption simply by "denying it".

A more subtle way of discharging an assumption is by introducing it as the antecedent of a conditional. The very basic way of doing this would be the following:
1) John is Jane Assumption
2) If John is Jane, then John is Jane ->I
Of course, you are not saying an awful lot in 2) - it's basically just an empty tautology - but never the less, you no longer are relying on the fact that John is Jane in order for (2) to be true.

In my version of the argument above, I use the conditional introduction rule twice in order to discharge assumptions. Picking on this threesome of John, Jane and Janice, I have
John is Jane Assumption
John is Janice Assumption
If John is Jane then John is Janice ->I
In making that move I discharge my assumption that John is Jane and leave everything about my argument hanging on whether or not John is Janice.

I hope that helps.

Reply to jkg20

It helps a lot, although I have to familiarize with proving conditionals --and reread your previous replies. From what you say, I have a to find a way to support/prove the antecedent before I arrive at the consequent (something like Modus Ponens). The difficult part, which I need to familiarize with, is to support my antecedents through relying on the given premises or assumptions.

Thank you!

Conditional elimination rule is basically just another name for modus ponens, so yes, if you are going to use it, you will need to either assume the truth of your antecedent, or to have derived that antecedent from other premises/assumptions you have already made in your argument. The thing to remember is that it is not an assumption discharging rule of inference: any assumptions you still have in play up to the point you use modus ponens/conditional elimination, remain in play after you have used that rule. Although the "numbers on the left" are apparently not obligatory for your exam, they can be very useful for keeping track of what you are still assuming in your argument (in fact, that is really what they are there for) so whilst you are revising, it might be worthwhile trying to use them, even if in the exam you can take a shortcut and forget about them.

Reply to jkg20

Regarding your solution... Do you mean identity elimination with IE on line 3? If yes, does IE allow us move b from the right of the first line to the left of the third line? I mean your proof looks good, but I need to know the rule that allows one change the place of b on line 3. Thanks!

jkg20:
1 (1) a=b Assumption
2 (2) a=c Assumption
1,2 (3) b=c 1,2 IE
2 (4) (a=b -> a=c) 1,2 ->I
(5) (a=b -> a=c) -> b=c 4,3 ->I
(6) Ax(x=b -> x=c)-> b=c 5, AI

Yes I do mean Identity Elimination, and its precise use for you will depend on exactly how the IE rule is defined by Forbes. However, as I was taught, the identity elimination rule basically just tell you that from a given identity statement
a=b
say
you can change any occurrence of 'a' in any other statement in which 'a' occurse with an occurence of 'b', and it would also allow any occurence of 'b' in any other statement to be replaced with an occurence of 'a'. So, in my argument I use the identity a=b to replace the 'a' in a=c with 'b'

If the IE rule you have been given requires that the subsitution made be sensitive to the exact order of the terms in the identity statement, then you may have to go through some additional steps of swapping the terms around, but the rules as I remember being taught them did not require this.

Reply to jkg20 Reply to Nagase

In ten days I have to take the exam and I still do not feel ready with everything....

Here is a conclusion that I am supposed to invalidate without any premises being given.

|? (Ex)(Ay)((Rxy & ~Ryx) --> (Rxx <-> Ryy)

I thought as a solution a domain with two members D= [a,b], where extension R=[, ], hoping in this way to make the antecedent (Rxy&~Ryx) true and the consequent of the conditional false (since I am supposed to invalidate the sentence above). The author, however, does not give a solution to this problem. He just says that it was invented by Mendelson (?) and it can be solved only with four objects in the Domain (D=a,b,c,d or D=0,1,2,3?).

I am now wondering why the solution I gave with two objects will not do?

That's a tough one. I guess you have to show that the negation of the formula can be true under some interpretation, which seems to be what you are getting at. What you have to show is that in some interpretation the following is true:
AxEy((Rxy & -Ryx) & -(Rxx <-> Ryy))
An interpretation with two objects a,b and the extension for R , would not do that (you can make all the substitutions to see for yourself that the above formula never turns out to be true). You'd then have to play around with a,b,c and the consequent possibilities for Ext R to see if you could get any further. I suppose if Forbes/Mendelson is correct you need at least four objects in the domain and an extension for R that is suitably restricted. Note that for -(Rxx <-> Ryy) to be true under an interpretation you need the truth values of Rxx and Ryy to be opposites of each other.
To be honest, I doubt you'll have anything as challenging as this to deal with in your exam.

@Eros1982Maybe I could have been a little clearer about why the formula AxEy((Rxy & -Ryx) & -(Rxx <-> Ryy)) is not true in the domain you give.
The interpretation contains a and b, with extension for R and .
Within the context of that interpretation, elimination of universal quantification allows us to infer
Ey((Rby & -Ryb) & -(Rbb <->Ryy))
The extension for R you give does not allow for (Rby & -Ryb) to be true no matter whether you replace y by a or by b, but those are the only two possible replacements in your interpretation. This means that in the interpretation you give, the universal claim made by the formula just is not true. Obviously, adding and to the extension of R is not going to help. So, there is the need to have more than two objects in the domain in order to allow for the necessary flexibility in the extension of R, in order that we can get the universal claim to be true for all possible substitution instances of x. If you reiterate this kind of reasoning my guess is you will end up showing that AxEy((Rxy & -Ryx) & -(Rxx <-> Ryy)) is true for a domain with four objects (a,b,c,d) and some appropriately chosen extension for R. Hope that helps.

This forum is a good platform for learners. Thank you for posting.

Reply to Leesa Johnson Happy to (try to) help:smile:

Reply to jkg20

Thank so much for you for your time. I will reread your replies in the weekend when I am off, with the hope that my mind will be sharper lol :)

This strategy of turning |?(Ex)(Ay)((Rxy & ~Ryx) --> (Rxx <-> Ryy) into AxEy((Rxy & -Ryx) & -(Rxx <-> Ryy)) is mentioned by the author as well, but I am a little confused why turning (Ex)(Ay) to (Ax)(Ey) would somehow help to invalidate the first.

It's basically to do with the negation of quantifiers. If I say everything is red , Ax(Rx), then the negation of that claim is equivalent to saying that there is at least one thing which is not red, i.e. Ex-(Rx). If I say that at least one thing is red, Ex(Rx), the negation of that claim is equivalent to saying that everything is not red, i.e. Ax-(Rx). So, negating the whole of a quantified statement is essentially the same as switching the quantifier type and negating the proposition governed by the quantifier (this can be proved in first order predicate logic, but I won't bore you with that). The same principle works when quantifiers are compounded, so that the negation of AxAy(Rxy) becomes ExEy-(Rxy), the negation of ExEy(Rxy) becomes AxAy-(Rxy), the negation of ExAy(Rxy) becomes AyEx-(Rxy) and the negation of AxEy(Rxy) becomes ExAy-(Rxy). Suppose for instance that R is the relation 'is uglier than'. AxAy(Rxy) says that everyone is uglier than everyone else, and its negation is simply that there are at least two people such that one of them is not uglier than the other. ExAy(Rxy) states that there is at least one person that is uglier than everyone else - i.e. there is at least one contender for the title "ugliest person of the year". The negation states there is no such person, which is equivalent to saying that everyone is such that we can find someone who is uglier than they are - basically, no matter who you choose, they are better looking than at least someone else. Formalised, then, -(ExAy(Rxy)) is equivalent to AxEy-(Rxy). Now, it doesn't matter whether we replace Rxy by some more complicated compound sentence (although it becomes more difficult to find "real world" examples). So, if we replace Rxy by ((Rxy & -Ryx) -> (Rxx<->Ryy)), we will still be able to infer from -(ExAy((Rxy & -Ryx) -> (Rxx<->Ryy))) to AyEx-((Rxy & -Ryx) -> (Rxx<->Ryy)). You know already from basic first order calculus that -(A->B) is logically equivalent to A & -B. So, replacing A with (Rxy & -Ryx) and B with (Rxx<->Ryy), we end up with the conclusion that -(ExAy((Rxy & -Ryx) -> (Rxx<->Ryy))) is logically equivalent to AyEx((Rxy & -Ryx) & -(Rxx<->Ryy)). Now the claim |?(Ex)(Ay)((Rxy & ~Ryx) --> (Rxx <-> Ryy) is essentially saying that there is at least one interpretation in which (Ex)(Ay)((Rxy & ~Ryx) --> (Rxx <-> Ryy)) comes out false, i.e. where -((Ex)(Ay)((Rxy & ~Ryx) --> (Rxx <-> Ryy))) is true for at least one interpretation, which, by the foregoing reasoning is equivalent to saying that there is an interpretation in which AyEx((Rxy & -Ryx) & -(Rxx<->Ryy)) is true. The challenge is to find the simplest interpretation which does the job (and apparently it is an interpretation with four objects).
Hope that helps.

Reply to jkg20

I will reread your last reply tomorrow (when I will switch provability with demonstrating invalidity :)

There is one more question I'd like to ask, and I hope it is not difficult to you...

When there are two existential quantifiers stacked at the beginning of a premise, I first replace the first variable with a substituting instance (instead of Ex I assume "a"), and then the second variable (instead of Ey I assume "b"). I am not sure, however, what I am supposed to do when the existential quantifier I wish to substitute has a negation. For example: -(Ex)(Ey)(x?y & (Fx & Fy)).


Should I substitute -(Ex) with negations only, e.g. (Ey)(-a ? y & (-Fa & Fy)) --and after think of a Sequent/Theorem Introduction (if there is one) that turns -a ? y to a=y--, or is there any other way to deal with quantifiers which contain negations?


Thank you!

Reply to Eros1982 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.

Reply to jkg20

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.

Reply to jkg20

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.

Reply to jkg20

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.

Reply to jkg20

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.

Reply to jkg20

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!

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

Reply to Eros1982 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?

Reply to jkg20

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...