Proof of $\vdash P \rightarrow (Q\lor P)$

Question

I was wondering how to go about proving this tautology. It seems quite simple to just answer:

$$\dfrac{\dfrac{[P]^*}{Q\lor P}\lor_I}{P\rightarrow (Q\lor P)} \to_I^* $$

Is this sufficient or does one also have to deduce the implication $P\rightarrow (Q\lor P)$ from EFQ?

Answer 1

Your derivation is absolutely correct! There is no need for EFQ, the rules $\lor_I$ ($\lor$-introduction) and $\to_I$ ($\to$-introduction) that you have used in your derivation are sufficient to prove $P \to (Q \lor P)$.

Remark: This means that $P \to (Q \lor P)$ is provable not only in classical and intuitionistic logic, but also in minimal logic.