Changing Scope of Quantifier Natural Deduction

Question

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?

Answer 1

One proof can be:

1. $\forall x(Pa\lor Rx)$ - assumption
2. $Pa\lor\lnot Pa$ - TND
3. $\lceil$ $Pa$ - additional assumption
4. $\lfloor$ $Pa\lor\forall xRx$ - introduction of disjunction on 3.
5. $\lceil$ $\lnot Pa$ - additional assumption
6. $\mid$ $\lceil$ u - new variable
7. $\mid$ $\mid$ $Pa\lor Ru$ - elimination of $\forall$ from 1.
8. $\mid$ $\lfloor$ $Ru$ - disjunctive syllogism on 5. and 7.
9. $\mid$ $\forall xRx$ - introduction of $\forall$ on 6-8.
10. $\lfloor$ $Pa\lor\forall xRx$ - introduction of disjunction on 9.
11. $Pa\lor\forall xRx$ - elimination of disjunction from 2, 3-4. and 5-10.

Another proof is:

1. $\forall x(Pa\lor Rx)$ - assumption
2. $\lceil$ $\lnot(Pa\lor\forall xRx)$ - additional assumption
3. $\mid$ $\lnot Pa\land \lnot\forall xRx$ - De Morgan's law on 2.
4. $\mid$ $\lnot Pa$ - elimination of $\land$ from 3.
5. $\mid$ $\lnot \forall xRx$ - elimination of $\land$ from 3.
6. $\mid$ $\exists x\lnot Rx$ - De Morgan's law on 5.
7. $\mid$ $\lnot Rb$ - elimination of $\exists$ from 6.
8. $\mid$ $Pa\lor Rb$ - elimination of $\forall$ from 1.
9. $\mid$ $Rb$ - disjunctive syllogism on 4. and 8.
10. $\lfloor$ $\bot$ - elimination of $\lnot$ from 7. and 9.
11. $\lnot\lnot(Pa\lor\forall x Rx)$ - introduction of $\lnot$ on 2-10.
12. $Pa\lor\forall x Rx$ - elimination of $\lnot\lnot$ from 11.

Answer 2

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)}}}}$

Answer 3

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} $