Any comments/answers concerning the block-quote (red) text would be appreciated.
I've been examining proofs of the Fundamental Theorem of Arithmetic and constructing my own using the method of infinite descent.
As I work on this it reminds me of theory of structured programming, regarding all the infinite descent proofs as code fragments.
I now believe any selection of these infinite descent proofs could be combined into one theorem that would 'crank it all out' together, with all the results being subtheorems.
The universal quantifier distributes over conjunciton and to prove, say
$$ \forall n\, P_1(n) \land \forall n\, P_2(n) \land \forall n\, P_3(n) \land \forall n\, P_4(n)$$
the infinite descent machinery would be applied to
$$ \exists n\, \neg P_1(n) \land \exists n\, \neg , P_2(n) \land \exists n\, \neg P_3(n) \land \exists n\, \neg P_4(n)$$
and the proof would be structured into cases but with a 'program flow'.
Here is a simple example of using infinite descent thinking along these terms, tackling a problem that usually is set up with weak induction and a base case.
$\quad S(n) : \sum_{k=1}^n k = \frac{(n+1)n}{2}$
$\quad P_1(n) : \forall n \ge 1\; \text{ If } n = 1 \text{ then } S(n) \quad$ (induction base case expressed here as a tautology)
$\quad P_2(n) : \forall n \ge 1\; S(n)$
Case 1: Return $P_1(n)$ as True.
Case 2:
Let $n \ge 1$ such that $\sum_{k=1}^n k \ne \frac{(n+1)n}{2}$. Since $P_1(n)$ is true, $n \gt 1$. It is easy to show that $S(n-1)$ is also false and $n -1 \ge 1$.
Return $\neg P_1(n-1)$ as True.
Program Execution Ends: $\forall n \ge 1 \; P_1(n) \land P_2(n)$ is TRUE.
I know that computers are proving theorems, and was wondering if this might be applicable.