Hoare logic, proving conjunction rule from basic rules, possible or not?

Question

(This is HW.) Suppose I have these following proof rules given.

I am currently considering if I can prove the conjunction rule (given below) from the above given Hoare logic rules.

My answer would be "no", because from the proof rules of Hoare logic, I can neither use the Implied rule to prove it (because from $A$ I cannot infer $A \wedge B$) nor introduce it anywhere from the first four proof rules (the only one which introduces conjunction in the post-condition requires a while). I am fairly confident that this line of reasoning is correct, but am I missing anything? For example, can I argue on a the propositional logic level that since I have $P$ as a precondition, and I have $Q_1$ and $Q_2$ as postconditions, I can simply introduce conjunction on the propositional logic level (instead of inferring purely on Hoare logic)?

Answer 1

Your reasoning is fine as far as the derivability of this rule. To respond to the latter part of your last paragraph, if the rules you've listed are all the rules available, then those are the only rules you can use. A derivation is a tree of applications of rules. You need to be able to state what rule you're using at each node in that tree. A(n explicit) proof that this rule was derivable would be an actual derivation, i.e. tree of rule applications.

There's a different and (slightly) harder question that you probably were not asked which is whether the Conjunction Rule is admissible. That is, could the Conjunction Rule be added without causing any problems, i.e. unsoundness.