Epistemic disjunction, axiom or rule?

Question

Assume I have a minimal logic |- with disjunction v and implication ->. Now I want to represent some domain knowledge. One opponent says I should represent it as an axiom:

P -> U v V  (myAxiom)

Another opponent says I should represent it as an inference rule:

G, U |- D   G, V |- D
---------------------- (myRule)
      G, P |- D

In my opinion both the axiom and the rule lead to the same derivations, even without including some classical assumptions about negation. Is this true?

P.S.: This is a follow up to:
Disjunction in Intuitionistic Logic, what about $((P \to U \lor V) \to Z)$

Answer 1

Not much is needed to derive the axiom from the rule:

1. Note that $P, U \vdash U \lor V$ and $P, V \vdash U \lor V$, so $P \vdash U \lor V$ by the rule.
2. Using the deduction theorem, $\vdash P \to (U \lor V)$.

Similarly, if the axiom is given, then the rule is admissible:

1. If $G, U \vdash D$ and $G, V \vdash D$, then by the left $\lor$ rule, $G, U \lor V \vdash D$.
2. By modus ponens, $G, P \vdash U \lor V$.
3. Cutting, we get $G, P \vdash D$.