How to prove this sequent using natural deduction?

Question

How do I prove $$S\rightarrow \exists xP(x) \vdash \exists x(S\rightarrow P(x))$$ using natural deduction? Just an alignment of which axioms or rules that one could use would be much appreciated.

Answer 1

1. $S \to \exists x P(x)$ [P]
2. 1. $S$ [A]
   2. $S \to \exists x P(x)$ [1 R]
   3. $\exists x P(x)$ [2.2 2.1 $\to$E]
   4. 1. $P(a)$ [A]
      2. 1. $S$ [A]
         2. $P(a)$ [2.4.1 R]
      3. $S \to P(a)$ [2.4.2.1 2.4.2.2 $\to$I]
      4. $\exists x [S \to P(x)]$ [2.4.3 $\exists$I]
   5. $\exists x [S \to P(x)]$ [2.3 2.4.1 2.4.4 $\exists$E]
3. $S \to \exists x [S \to P(x)]$ [2.1 2.5 $\to$I]
4. 1. $\neg S$ [A]
   2. 1. $S$ [A]
      2. $\neg S$ [4.1 R]
      3. $\neg S \lor P(a)$ [4.2.2 $\lor$I]
      4. $P(a)$ [4.2.3 4.2.1 $\lor$E]
   3. $S \to P(a)$ [4.2.1 4.2.4 $\to$I]
   4. $\exists x [S \to P(x)]$ [4.3 $\exists$E]
5. $\neg S \to \exists x [S \to P(x)]$ [4.1 4.4 $\to$I]
6. $S \lor \neg S$ [LEM]
7. $\exists x [S \to P(x)]$ [3 5 6 $\lor$E]

How to complicate everything, take #314159.

Answer 2

Here is a proof in the Fitch formal proof system: