[TechSyndrome]

Hi! I'm really happy in that I've been able to learn Predicate Logic within just a couple of days - which is amazing! And thanks to YouTube! But, I am having small problem with a section on this YouTube video and I am hoping to get some help on this.

Here is an image of the Formal Proof:



From what I've learnt, when doing Indirect Proof (or Proof by Contradiction) you need to derive the contradiction from the negated consequence (assumption 2 in this case). But, wouldn't it have been better to isolate '~Hy' on line 5 and then use conjunction with Jy later on to continue the answer? Wouldn't that take it closer to its generalised form? I feel my understanding of contradiction is wrong...can someone kindly explain this concept of contradiction to me if that is where I am going wrong? My current understanding for truth tables is pretty much - when the values of final column are all false, then this is a contradiction...

Regards,

[JTHM]

I'm not sure precisely what you mean by "continue the answer," so I can't conclusively answer your question. However, (and forgive me if this is not at all germane) you might need to bear in mind that, when using reductio ad absurdum, you cannot use anything proven within the scope of the assumption you made once you return the broader proof. If I assume a proposition, reach a contradiction, and there are many intermediate propositions proven in between, I cannot make use of those propositions after completing the proof by contradiction. I have not actually proven any of those things; I have only proven them under some assumption. An assumption, incidentally, which has just been proven to be false.