Yes; thank you. Well, I came here to find the answer to a simple question and I ended up learning much more, so thanks to everyone. And, by the way, I was asked to use the Fitche System to derive the conclusion.

Two Universal Eliminations and I get to p(x,y); don't know what to do next?

Interesting! Well, I asked because I don't really have any express, concrete end by which to justify my self-study of logic; I just enjoy learning it. I just got a bachelor degree in Biology and am switching to a double major in Literature/History, so I guess that I'm just very sporadic and eclectic; but sometimes I ask myself whether the time spent learning logic won't come at an opportunity-cost; and I wonder whether it will really yield any benefits that suit my future projects. But I can't know before I try, right?

I know. God, I spent so much time fretting and thinking about what I might've possibly missed, all under the assumptions that the course material had to be correct.
Anyway; I wanted to ask you something: how did you learn propositional logic? On your own or in university? Has it actually affected or improved your thinking? Very naive question, I know; but I'm a beginner, so I guess that that is a good excuse to ask naive questions

Yes, I edited the last post to include the link

I am following Stanford's introduction to propositional logic and at the end of each section they provide exercises and the answers to those exercises in order that you check whether your responses are correct.
Well, when I click on “show answers,” it says that the claim “If Γ ⊨ ¬φ[τ] for some ground term τ, then Γ ⊭ ∀x.φ[x]” is false, whereas I think that it is true; and you seem to agree with me..
Here is the link: http://intrologic.stanford.edu/exercises/exercise_06_07.html

I have another question though; so, Γ is a set of Relational Logic sentences, and φ and ψ are individual Relational Logic sentences.
Now, I am aksed whether this claim is true or false:

If Γ ⊨ ¬φ[τ] for some ground term τ, then Γ ⊭ ∀x.φ[x]; true or false?

Isn't it true? I mean, if Γ entails ¬φ for some given ground term, here τ, then it cannot be that Γ⊨ ∀x.φ[x], that is, it cannot be that Γ entails φ for all x; therefore, Γ ⊭ ∀x.φ[x].
Am I missing something? Because when I check the answers, it turns out that it is false...

Hold on; there is something I actually didn't get. You said that we can interpret above(x,y) as always true, for any x and any y, and, then, you gave me the example that ‘‘above’’ might mean ‘‘is a block’’. But isn't above a binary relation constant? It can't be is a block. And I can't think of any interpretation under which above(x,y) is true for any x and any y.

Edit: I got where I am wrong; I'm allowing implicit assumptions to infect my reasoning. I shouldn't think about it in terms of whether I can find concrete linguistic examples of relation constants which satisfy the sentence, but, rather, I should think in terms of truth tables; is that right?

Thank you very much! Yes, I was injecting a lot of implicit assumptions.

In particular, if ~on(c,a) is not provable then it is possible for on to mean 'to the left of' and the blocks to be arranged in a ring — andrewk

~on(c,a) is part of the axiomatisation of on; therefore, on cannot mean to the left of.

ask the question whether what you have described as a 'relation' in the OP is supposed to be an axiom. — andrewk

Yes, it is an axiom.

Here is the link to the exercise: http://intrologic.stanford.edu/exercises/exercise_06_05.html
That'll be better than me trying to explain it

Yes, it does help, thank you!

Can we exit a subproof only by using Implication Introduction?

1 P => Q => R Assumption
2 P => Q Assumption
3 P Assumption
4 Q Implication Elimination 2, 3
5 Q => R Implication Elimination 1, 3
6 R Implication Elimination 5, 4
7 P=>R Implication Introduction 3, 6
8 P => Q => R => R Implication Introduction 2, 7
9 ( P => ( Q => R ) ) => (( P => Q ) => ( P => R ) ) Implication Introduction 1, 8

In this case, line 2 to 7 is a subproof, and 3 to 6 a subproof of that subproof. I deduced R on line 6 after deriving Q => R on line 5. I hadn't done it before because I thought that I could not apply a rule of inference on elements that were at two removes from each other so to speak. To deduce Q => R in line 5, one has to apply Implication Elimination on 1 and 3. What bothered me is that 3 was a subproof of a subproof of the super-proof in which line 1 is nested, and I thought that this made it impossible to apply the rule; I thought that the two elements on which one applies the rule of inference had to be no more than at one remove from each other as it were. I don't know where I got that idea.
And how exactly does one ‘‘close’’ a subproof? Does that mean that it can't end with an assumption?

All right; so, I assumed what was on the left:

1 P => Q => R Assumption
2 P=>Q Assumption
3 P Assumption
4 Q Implication Elimination 2, 3
5 R Assumption
6 P=>R Implication Introduction 3, 5
7 P => Q => R => R Implication Introduction 2, 6
8 ( P => ( Q => R ) ) => (( P => Q ) => ( P => R ) ) Implication Introduction 1, 7

Is this correct? I suspect the Assumption of R in 5 to be incorrect. I thought about deriving Q => R by applying Implication Elimination on the Premise 1 and the Assumption 3 and then by proving R, but I'm not sure that it's possible.
And, by the way, 2 to 6 is a subproof, and 3 to 5 a subproof to that subproof

That's a useful trick! I'll try to apply it and see how well it goes

Well, let's say that most of what I've been practising is just that, namely finding definitions and principles, whereas I haven't really paid much attention to, literally, the other side of the argument

I have another question though. I'm learning logic for the sake of it; I love philosophy. Nonetheless, I'd like to know if learning logic will bring me any practical benefits, for example in verifying the validity of some arguments or stuff like that.

All right, thank you!