Changing Scope of Quantifier Natural Deduction I am struggling to find a syntactic transformation for this:
$∀x(Pa∨Rx)$ to $Pa∨∀x(Rx)$
Using the natural deduction system outlined in Volker Halbach's 'The Logic Manual' my strategy has so far been to derive the conclusion from $Pa$ and from $Rb$ as both could be discharged using the premise after eliminating the universal quantifier. My problem is that I cannot derive the conclusion from $Rb$. How would I go about proving this, if my strategy seems to fail?
 A: One proof can be:

*

*$\forall x(Pa\lor Rx)$ - assumption

*$Pa\lor\lnot Pa$ - TND

*$\lceil$ $Pa$ - additional assumption

*$\lfloor$ $Pa\lor\forall xRx$ - introduction of disjunction on 3.

*$\lceil$ $\lnot Pa$ - additional assumption

*$\mid$ $\lceil$ u - new variable

*$\mid$ $\mid$ $Pa\lor Ru$ - elimination of $\forall$ from 1.

*$\mid$ $\lfloor$ $Ru$ - disjunctive syllogism on 5. and 7.

*$\mid$ $\forall xRx$ - introduction of $\forall$ on 6-8.

*$\lfloor$ $Pa\lor\forall xRx$ - introduction of disjunction on 9.

*$Pa\lor\forall xRx$ - elimination of disjunction from 2, 3-4. and 5-10.

Another proof is:

*

*$\forall x(Pa\lor Rx)$ - assumption

*$\lceil$ $\lnot(Pa\lor\forall xRx)$ - additional assumption

*$\mid$ $\lnot Pa\land \lnot\forall xRx$ - De Morgan's law on 2.

*$\mid$ $\lnot Pa$ - elimination of $\land$ from 3.

*$\mid$ $\lnot \forall xRx$ - elimination of $\land$ from 3.

*$\mid$ $\exists x\lnot Rx$ - De Morgan's law on 5.

*$\mid$ $\lnot Rb$ - elimination of $\exists$ from 6.

*$\mid$ $Pa\lor Rb$ - elimination of $\forall$ from 1.

*$\mid$ $Rb$ - disjunctive syllogism on 4. and 8.

*$\lfloor$ $\bot$ - elimination of $\lnot$ from 7. and 9.

*$\lnot\lnot(Pa\lor\forall x Rx)$ - introduction of $\lnot$ on 2-10.

*$Pa\lor\forall x Rx$ - elimination of $\lnot\lnot$ from 11.

A: 
Using the natural deduction system outlined in Volker Halbach's 'The Logic Manual' my strategy has so far been to derive the conclusion from $Pa$ and from $Rb$ as both could be discharged using the premise after eliminating the universal quantifier. My problem is that I cannot derive the conclusion from $Rb$. How would I go about proving this, if my strategy seems to fail?

I am not familiar with that text, but the basic principle is to use reduction to absurdity.
$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\boxed{\boxed{\fitch{~1.~\forall x~(Pa\vee Rx)\hspace{10ex}\textsf{Premise}}{\fitch{~~2.~\neg(Pa\vee \forall x~Rx)\hspace{6ex}\textsf{Assume}}{\fitch{~~3.~\boxed {\color{blue}b}\hspace{16ex}\textsf{Assume}}{~~4.~Pa\vee R\color{blue}b\hspace{10ex}\textsf{Universal Elimination (1)}\\\fitch{~~5.~Pa\hspace{14ex}\textsf{Assume}}{~~6.~Pa\vee\forall x~Rx\hspace{5ex}\textsf{Disjunction Introduction (5)}\\~~7.~\bot\hspace{15ex}\textsf{Negation Elimination (6,2)}\\~~8.~R\color{blue}b\hspace{13.5ex}\textsf{Explosion (7); }\textit{ex falso quodlibet}}\\\fitch{~~9.~R\color{blue}b\hspace{14ex}\textsf{Assume}}{}\\10.~R\color{blue}b\hspace{16ex}\textsf{Disjunction Elimination (4,5-8,9-9)}}\\11.~\forall x~Rx\hspace{15ex}\textsf{Universal Introduction (3-10)}\\12.~Pa\vee\forall x~Rx\hspace{9.5ex}\textsf{Disjunction Introduction (11)}\\13.~\bot\hspace{19.5ex}\textsf{Negation Elimination (12,2)}}\\14.~\neg\neg(Pa\vee\forall x~Rx)\hspace{7ex}\textsf{Negation Introduction (2-13)}\\15.~Pa\vee\forall x~Rx\hspace{12ex}\textsf{Double Negation Elimination (14)}}}}$
A: Using the system outlined in Volker Halbach's book, perhaps a possible proof of $\forall x(Pa \lor Rx) \vdash Pa \lor \forall xRx$ could be, I think:
$
\def\ae\qquad\mathbf{\forall Elim}
\def\ai\qquad\mathbf{\forall Intro}
\def\be\qquad\mathbf{\leftrightarrow Elim}
\def\bi\qquad\mathbf{\leftrightarrow Intro}
\def\oe\qquad\mathbf{\lor Elim}
\def\oi\qquad\mathbf{\lor Intro}
\def\ne\qquad\mathbf{\neg Elim}
\def\ni\qquad\mathbf{\neg Intro}
$
$
\begin{equation}
  \dfrac{
    \dfrac{
      \dfrac{
        \dfrac{
          \dfrac{\forall x(Pa \lor Rx)}{Pa \lor Rb}\ae
            \dfrac{\dfrac{[Pa]}{Pa \lor \forall xRx}\quad [\lnot(Pa \lor \forall xRx)]}{Rb }\ne \quad [Rb]
            }{
              Rb
            }\oe
            }{
              \forall xRx
            }\ai
          }{
            Pa \lor \forall xRx
          }\oi \quad [\lnot(Pa \lor \forall xRx)]
        }{
    Pa \lor \forall xRx
}\ne
\end{equation}
$
