Is this proof in natural deduction proof system correct?

Question

Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ is valid? And similarly, if I know that $\phi'\vdash \phi''$, can I use this when proving $\psi$? For example, if I know that $p\to q\vdash \neg q\to \neg p$ and $A\vdash \neg p$, then is this proof of the fact that $\vdash A\to (p\to q)$ is correct?

 0.                         (no premises)
   1.A                      (assumption)
       2.not(q)             (assumption)
       3.not(p)             (here we use that A proves not(p))
   4.not(q) → not(p)        (from 2,3)
   5.p → q                  (from 4; here we use that not(q) → not(p) proves p → q)
 6.A → (p → q)              (from 1,5)

If so, how do I justify formally that what was done in lines 3 and 5 is legit?

Answer 1

It is legitimate; it is kind of the point of why we prove things.   If you have already proven that a consequence is derivable from some premise, then you may immediately derive the consequence from the premise(s); there is no need repeat the process (you just need to be able to provide a citation).

This is sometimes called using a First Order Consequence (or FO Con).

But do notice that in line 5 you use $\lnot q\to\lnot p\vdash p\to q$ which is quite different from $p\to q\vdash \lnot q\to \lnot p$.

$$\begin{array}{|l} \\\hline~~ \begin{array}{|l} ~~1.~~A\\\hline ~~\begin{array}{|l} ~~2.~~\lnot q \\\hline ~~3.~~\lnot p \qquad 1,\text{FOCon }A\vdash \lnot p \end{array}\\~~4.~~\lnot q\to\lnot p\\~~5.~~p\to q\qquad 4,\text{FOCon }\lnot q\to\lnot p\vdash p\to q \end{array}\\~~6.~~ A\to(p\to q) \end{array}$$

Answer 2

In a mathematical proof, this would be the same as using Lemma's ... and everything you do here is logically correct. The question is: is this allowed in a formal proof?

Well, some formal proof systems have Lemma's as part of their arsenal ... but others don't, and so you will have to write out the steps.

Also, going from $\neg q \to \neg p$ to $p \to q$: some formal proof systems will have this as an explicit inference rule (typically called Contraposition) ... but again, others don't.

So, it all depends depend on how your formal proof system is defined, and what rules it has.