avewright/proofwiki-math huggingface dataset:
Theorem: Set of Total Functions is Not Recursive

The set $\operatorname{Tot}$ of natural numbers which code URM programs which compute total functions of one variable is not recursive.

Proof:
We perform a proof by Cantor's Diagonal Argument.
Suppose the contrary, that $\operatorname{Tot}$ is a recursive set.
First we define a recursive function $h$ which enumerates the code numbers of URM programs which compute total functions of one variable.
The program of this sort with the smallest code is:
{|
|-
! align="right" | Line !!
! align="left" | Command 
|-
| align="right" | $1$ ||
| align="left" | $\map Z n$ 
|}
which computes the zero function.
Its code number is $2^3 = 8$.
So we can define the recursive function $h$ as:
:$\map h n = \begin{cases}
8 & : n = 0 \\
\map {\mu z} {z \in \operatorname{Tot} \text { and } \map h {n - 1} < z} & : n > 0
\end{cases}$
where $\mu z$ is the minimization operation.
As there are infinitely many URM programs which compute a total function of one variable, $\map h n$ is always defined.
More importantly, if $f: \N \to \N$ is a total recursive function, there is some $m \in \N$ such that the URM program with code number $\map h n$ computes $f$.
Now we define the function $\Phi: \N^2 \to \N$ as:
:$\map \Phi {m, n} = \map {\Phi_1} {\map h m, n}$
where $\Phi_1$ is the universal URM computable function of one variable.
Then $\Phi$ is a total recursive function, because:
:$\Phi_1$ and $h$ are both recursive
:The program coded by $m$ halts for all inputs $n$.
It has the property that if $f: \N \to \N$ is a total recursive function, there is some $m \in \N$ such that $\map \Phi {m, n} = \map f n$ for all $n \in \N$.
Now we use Cantor's Diagonal Argument.
It follows immediately that the function $g: \N \to \N$ given by:
:$\map g n = \map \Phi {n, n} + 1$
is also recursive.
Hence there is some number $m_0$ such that:
:$\map g n = \map \Phi {m_0, n}$
for all $n \in \N$.
In particular:
:$\map g {m_0} = \map \Phi {m_0, m_0}$
But from the definition of $g$:
:$\map g {m_0} = \map \Phi {m_0, m_0} + 1$
This contradiction arose because we assumed that $\operatorname{Tot}$ is recursive.
Hence the result.
{{Qed}}
Category:URM Programs
Category:Recursion Theory
3buevrxyj6ccg35a3mm8yzh3hvdpgf7
Theorem: Infinitely Many Programs for URM Computable Function

Let $g: \N^k \to \N$ be a URM computable function.
Then there is an infinite number of URM programs which compute $g$.

Proof:
As $g$ is URM computable, there exists a URM program which computes it.
Let $Q$ be such a program.
Let $n \in \N$.
Increment the <tt>Jump</tt>s in $Q$ by $n$ lines<ref>To '''increment the <tt>Jump</tt>s by $r$''' for any normalized URM program is done by changing all <tt>Jump</tt>s of the form $J \left({m, n, q}\right)$ to $J \left({m, n, q+r}\right)$.</ref>. Call this amended version $Q'$.
This is because, as $Q$ was written so as to start from line 1, we need to move all the <tt>Jump</tt>s so as to point to the same lines relative to the start of $Q'$.
Then we can build the following URM program:
{|
|-
! align="right" | Line !!
! align="left" | Command 
|-
| align="right" | $1$ ||
| align="left" | $C \left({1, 1}\right)$ 
|-
| align="right" | $2$ ||
| align="left" | $C \left({1, 1}\right)$ 
|-
| align="right" | $\vdots$ ||
| align="left" | $\vdots$ 
|-
| align="right" | $n$ ||
| align="left" | $C \left({1, 1}\right)$ 
|-
| align="right" | $n + 1$ ||
| align="left" | The start of $Q'$ 
|}
...etc.
Each of the $C \left({1, 1}\right)$ instructions codes the identity function.
So adding it to the front of $Q$ has no effect on the behaviour of $Q$
It is clear that for each $n \in \N$ there is a different URM program which computes $f$.
The result follows from Infinite if Injection from Natural Numbers.
{{qed}}
Theorem: Bounds of GCD for Sum and Difference Congruent Squares

Let $x, y, n$ be integers.
Let:
:$x \not \equiv \pm y \pmod n$
and:
:$x^2 \equiv y^2 \pmod n$
where $a \equiv b \pmod n$ denotes that $a$ is congruent to $b$ modulo $n$.
Then:
:$1 < \gcd \set {x - y, n} < n$
and:
:$1 < \gcd \set {x + y, n} < n$
where $\gcd \set {a, b}$ is the GCD of $a$ and $b$.

Proof:
{{begin-eqn}}
{{eqn | l = x^2
      | o = \equiv
      | r = y^2
      | rr= \pmod n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \divides
      | r = \paren {x^2 - y^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \divides
      | r = \paren {x + y} \paren {x - y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p
      | o = \divides
      | r = \paren {x + y} \paren {x - y}
      | c = for all prime divisors $p$ of $n$
}}
{{eqn | ll= \leadsto
      | l = p
      | o = \divides
      | r = \paren {x - y}
      | c = 
}}
{{eqn | lo= \lor
      | l = p
      | o = \divides
      | r = \paren {x + y}
      | c = 
}}
{{end-eqn}}
But since $x \not \equiv -y \pmod n$, then:
:$n \nmid \paren {x + y}$
and since $x \not \equiv y \pmod n$, then:
:$n \nmid \paren {x - y}$
Therefore:
:$\gcd \set {x - y, n} < n$
and:
:$\gcd \set {x + y, n} < n$
So if $p \divides \paren {x - y}$ then:
:$1 < \gcd \set {x - y, n} < n$
and also there exists $q$ such that:
:$q \divides n$
:$q \divides \paren {x + y}$
:$1 < q \le \gcd \set {x + y, n}$
Likewise if $p \divides \paren {x + y}$ then:
:$1 < \gcd \set {x + y, n} < n$
and also there exists $q$ such that:
:$q \divides n$
:$q \divides \paren {x - y}$
:$1 < q \le \gcd \set {x - y, n}$
{{qed}}
Category:Greatest Common Divisor
2ob6v1o7np6io1f9934hko48nro0o2v
Theorem: Triangle Angle-Side-Angle Congruence

If two triangles have:
:two angles equal to two angles, respectively
:the sides between the two angles equal
then the remaining angles are equal, and the remaining sides equal the respective sides.
That is to say, if two pairs of angles and the included sides are equal, then the triangles are congruent.

Proof:
:400px
Let $\angle ABC = \angle DEF$, $\angle BCA = \angle EFD$, and $BC = EF$.
{{AimForCont}} that $AB \ne DE$.
If this is the case, one of the two must be greater.
{{WLOG}}, we let $AB > DE$.
We construct a point $G$ on $AB$ such that $BG = ED$.
Using Euclid's first postulate, we construct the segment $CG$.
Now, since we have:
:$BG = ED$
:$\angle GBC = \angle DEF$
:$BC = EF$
it follows from Triangle Side-Angle-Side Congruence that:
:$\angle GCB = \angle DFE$
But from Euclid's fifth common notion:
:$\angle DFE = \angle ACB > \angle GCB$
which is a contradiction.
Therefore, $AB = DE$.
So from Triangle Side-Angle-Side Congruence:
:$\triangle ABC = \triangle DEF$
{{qed}}
{{Euclid Note|26|I|It appears to have originally been created by {{AuthorRef|Thales of Miletus}}.|part = first}}
Theorem: Triangle Side-Angle-Angle Congruence

If two triangles have:
:two angles equal to two angles, respectively
:the sides opposite one pair of equal angles equal
then the remaining angles are equal, and the remaining sides equal the respective sides.
That is to say, if two pairs of angles and a pair of opposite sides are equal, then the triangles are congruent.

Proof:
:360px
Let:
:$\angle ABC = \angle DEF$
:$\angle BCA = \angle EFD$
:$AB = DE$
{{AimForCont}} that $BC \ne EF$.
If this is the case, one of the two must be greater.
{{WLOG}}, let $BC > EF$.
We construct a point $H$ on $BC$ such that $BH = EF$, and then we construct the segment $AH$.
Now, since we have:
:$BH = EF$
:$\angle ABH = \angle DEF$
:$AB = DE$
from Triangle Side-Angle-Side Congruence we have:
:$\angle BHA = \angle EFD$
But from External Angle of Triangle is Greater than Internal Opposite, we have:
:$\angle BHA > \angle HCA = \angle EFD$
which is a contradiction.
Therefore $BC = EF$.
So from Triangle Side-Angle-Side Congruence:
:$\triangle ABC = \triangle DEF$
{{qed}}
Theorem: Equal Alternate Angles implies Parallel Lines

Given two infinite straight lines which are cut by a transversal, if the alternate angles are equal, then the lines are parallel.
{{:Euclid:Proposition/I/27}}

Proof:
:400px
Let $AB$ and $CD$ be two infinite straight lines.
Let $EF$ be a transversal that cuts them.
Let at least one pair of alternate angles be equal.
{{WLOG}}, let $\angle AHJ = \angle HJD$.
{{AimForCont}} that $AB$ and $CD$ are not parallel.
Then they meet at some point $G$.
{{WLOG}}, let $G$ be on the same side as $B$ and $D$.
Since $\angle AHJ$ is an exterior angle of $\triangle GJH$, from External Angle of Triangle is Greater than Internal Opposite, $\angle AHJ > \angle HJG$, which is a contradiction.
Similarly, they cannot meet on the side of $A$ and $C$.
Therefore, by definition, $AB$ and $CD$ are parallel.
{{qed}}
{{Euclid Note|27|I|{{EuclidNoteConverse|prop = 29|title = Parallelism implies Equal Alternate Angles|part = first}}}}
Theorem: Parallelism is Transitive Relation

Parallelism between straight lines is a transitive relation.
{{:Euclid:Proposition/I/30}}

Proof:
:300px
Let the straight lines $AB$ and $CD$ both be parallel to the straight line $EF$.
Let the straight line $GK$ be a transversal that cuts the parallel lines $AB$ and $EF$.
By Parallelism implies Equal Alternate Angles:
:$\angle AGK = \angle GHF$
By Playfair's Axiom, there is only one line that passes through $H$ that is parallel to $CD$ (namely $EF$).
Therefore the transversal $GK$ cannot be parallel to $CD$.
Hence the two lines must therefore intersect.
The straight line $GK$ also cuts the parallel lines $EF$ and $CD$.
So from Parallelism implies Equal Corresponding Angles:
:$\angle GHF = \angle GKD$.
Thus $\angle AGK = \angle GKD$.
So from Equal Alternate Angles implies Parallel Lines:
:$AB \parallel CD$
{{qed}}
Theorem: Sum from 1 to n of 1 over r(r+1)

:$\ds \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} } = \frac n {n + 1}$

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds \forall n \ge 1: \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} } = \frac n {n + 1}$
=== Basis for the Induction ===
$\map P 1$ is true, as this just says $\dfrac 1 2 = \dfrac 1 2$.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds \sum_{r \mathop = 1}^k \frac 1 {r \paren {r + 1} } = \frac k {k + 1}$
Then we need to show:
:$\ds \sum_{r \mathop = 1}^{k + 1} \frac 1 {r \paren {r + 1} } = \frac {k + 1} {k + 2}$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 1}^{k + 1} \frac 1 {r \paren {r + 1} }
      | r = \sum_{r \mathop = 1}^k \frac 1 {r \paren {r + 1} } + \frac 1 {\paren {k + 1} \paren {k + 2} }
      | c = 
}}
{{eqn | r = \frac k {k + 1} + \frac 1 {\paren {k + 1} \paren {k + 2} }
      | c = Induction hypothesis
}}
{{eqn | r = \frac {k \paren {k + 2} + 1} {\paren {k + 1} \paren {k + 2} }
      | c = 
}}
{{eqn | r = \frac {k^2 + 2 k + 1} {\paren {k + 1} \paren {k + 2} }
      | c = 
}}
{{eqn | r = \frac {\paren {k + 1}^2} {\paren {k + 1} \paren {k + 2} }
      | c = 
}}
{{eqn | r = \frac {k + 1} {k + 2}
      | c = 
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds \forall n \ge 1: \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} } = \frac n {n + 1}$
{{qed}}
Theorem: Sum from 1 to n of 1 over r(r+1)

:$\ds \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} } = \frac n {n + 1}$

Proof:
From Partial Fractions Expansion: $\dfrac 1 {x \paren {x + 1} }$:
:$\dfrac 1 {r \paren {r + 1} } = \dfrac 1 r - \dfrac 1 {r + 1}$
and that $\ds \sum_{r \mathop = 1}^n \paren {\frac 1 r - \frac 1 {r + 1} }$ is a telescoping series. 
Therefore:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} }
      | r = \sum_{r \mathop = 1}^n \paren {\frac 1 r - \frac 1 {r + 1} }
      | c = Telescoping Series: Example 1
}}
{{eqn | r = 1 - \frac 1 {n + 1}
      | c = 
}}
{{eqn | r = \frac n {n + 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum from 1 to n of 1 over r(r+1)

:$\ds \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} } = \frac n {n + 1}$

Proof:
Observe that:
{{begin-eqn}}
{{eqn | l = \int_r^{r + 1} {\dfrac {\rd x} {x^2} }
      | r = \intlimits {\dfrac {-1} x} r {r + 1}
      | c = Primitive of Power
}}
{{eqn | r = \dfrac 1 r - \dfrac 1 {r + 1}
}}
{{eqn | r = \dfrac 1 {r \paren {r + 1} }
      | c = 
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 1}^n \frac 1 {r \paren {r + 1} }
      | r = \sum_{r \mathop = 1}^n \int_r^{r + 1} {\dfrac {\rd x} {x^2} }
}}
{{eqn | r = \int_1^{n + 1} {\dfrac {\rd x} {x^2} }
}}
{{eqn | r = \intlimits {\dfrac {-1} x} 1 {n + 1}
      | c = Primitive of Power
}}
{{eqn | r = \frac n {n + 1}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Fibonacci Numbers

:$\ds \forall n \in \Z_{\ge 0}: \sum_{j \mathop = 0}^n F_j = F_{n + 2} - 1$

Proof:
Proof by induction:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \sum_{j \mathop = 0}^n F_j = F_{n + 2} - 1$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = F_0
      | r = 0
      | c = 
}}
{{eqn | r = 1 - 1
      | c = 
}}
{{eqn | r = F_2 - 1
      | c = 
}}
{{end-eqn}}
which is seen to hold.
Theorem: Sum of Sequence of Odd Index Fibonacci Numbers

{{begin-eqn}}
{{eqn | q = \forall n \ge 1
      | l = \sum_{j \mathop = 1}^n F_{2 j - 1}
      | r = F_1 + F_3 + F_5 + \cdots + F_{2 n - 1}
      | c = 
}}
{{eqn | r = F_{2 n}
      | c = 
}}
{{end-eqn}}

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds \sum_{j \mathop = 1}^n F_{2 j - 1} = F_{2 n}$
Theorem: Sum of Sequence of Even Index Fibonacci Numbers

{{begin-eqn}}
{{eqn | q = \forall n \ge 1
      | l = \sum_{j \mathop = 1}^n F_{2 j}
      | r = F_2 + F_4 + F_6 + \cdots + F_{2 n}
      | c = 
}}
{{eqn | r = F_{2 n + 1} - 1
      | c = 
}}
{{end-eqn}}

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds \sum_{j \mathop = 1}^n F_{2 j} = F_{2 n + 1} - 1$
Theorem: Sum of Odd Sequence of Products of Consecutive Fibonacci Numbers

:$\ds \sum_{j \mathop = 1}^{2 n - 1} F_j F_{j + 1} = {F_{2 n} }^2$

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds \sum_{j \mathop = 1}^{2 n - 1} F_j F_{j + 1} = {F_{2 n} }^2$
Theorem: Lucas Number as Sum of Fibonacci Numbers

Let $L_k$ be the $k$th Lucas number, defined as:
:$L_n = \begin{cases}
2 & : n = 0 \\
1 & : n = 1 \\
L_{n - 1} + L_{n - 2} & : \text{otherwise} \end{cases}$
Then:
:$L_n = F_{n - 1} + F_{n + 1}$

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$L_n = F_{n - 1} + F_{n + 1}$
Theorem: Sum of Sequence of Product of Lucas Numbers with Powers of 2

Let $L_k$ be the $k$th Lucas number.
Let $F_k$ be the $k$th Fibonacci number.
Then:
:$\ds \forall n \in \N_{>0}: \sum_{j \mathop = 1}^n 2^{j - 1} L_j = 2^n F_{n + 1} - 1$
That is:
:$2^0 L_1 + 2^1 L_2 + 2^2 L_3 + \cdots + 2^{n - 1} L^n = 2^n F_{n + 1} - 1$

Proof:
Proof by induction:
For all $\forall n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds \sum_{j \mathop = 1}^n 2^{j - 1} L_j = 2^n F_{n + 1} - 1$
Theorem: Sum of Odd Positive Powers

Let $n \in \N$ be an odd positive integer.
Let $x, y \in \Z_{>0}$ be (strictly) positive integers.
Then $x + y$ is a divisor of $x^n + y^n$.

Proof:
Given that $n \in \N$ be odd, it can be expressed in the form:
:$n = 2 m + 1$
where $m \in \N$.
The proof proceeds by strong induction.
For all $m \in \N$, let $\map P m$ be the proposition:
: $x^{2 m + 1} + y^{2 m + 1} = \paren {x + y} \paren {x^{2 m} + \cdots + y^{2 m} }$
$\map P 0$ is the case:
: $x + y = x + y$
which is trivially an identity.
Theorem: Infinite Sequence Property of Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Then $\RR$ is a well-founded relation {{iff}} there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$

Proof:
=== Reverse Implication ===
{{:Infinite Sequence Property of Well-Founded Relation/Reverse Implication/Proof 1}}{{qed|lemma}}
Theorem: Infinite Sequence Property of Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Then $\RR$ is a well-founded relation {{iff}} there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$

Proof:
Suppose $\RR$ is not a well-founded relation.
So by definition there exists a non-empty subset $T$ of $S$ which has no minimal element.
Let $a \in T$.
Since $a$ is not minimal in $T$, we can find $b \in T: \paren {b \mathrel \RR a} \text { and } \paren {b \ne a}$.
This holds for all $a \in T$.
Hence the restriction $\RR \restriction_{T \times T}$ of $\RR$ to $T \times T$ is a right-total endorelation on $T$.
So, by the Axiom of Dependent Choice, it follows that there is an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
then $\RR$ is a well-founded relation.
Theorem: Infinite Sequence Property of Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Then $\RR$ is a well-founded relation {{iff}} there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$

Proof:
Suppose $\RR$ is not a well-founded relation.
Hence there exists $T \subseteq S$ such that $T$ has no minimal element under $\RR$.
Let $a_0 \in T$.
We have that $a_0$ is not minimal in $T$.
So:
:$\exists a_1 \in T: \paren {a_1 \mathrel \RR a_0} \text { and } a_1 \ne a_0$
Similarly, $a_1$ is not minimal in $T$.
So:
:$\exists a_2 \in T: \paren {a_2 \mathrel \RR a_1} \text { and } a_2 \ne a_1$
Let $a_{k + 1}$ be an arbitrary element for which $a_{k + 1} \mathrel \RR a_k$ and $a_{k + 1} \ne a_k$.
In order to allow this to be possible in the infinite case, it is necessary to invoke the Axiom of Dependent Choice as follows:
Let $a_k \in T$.
Then as $a_k$ is not minimal in $T$:
:$\exists a_{k + 1} \in T: \paren {a_{k + 1} \mathrel \RR a_k} \text { and } \paren {a_{k + 1} \ne a_k}$
Hence by definition $\RR$ is a right-total relation.
So, by the Axiom of Dependent Choice, it follows that:
:$\forall n \in \N: \exists a_n \in T: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } a_{n + 1} \ne a_n$
Thus we have been able to construct an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } a_{n + 1} \ne a_n$
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } a_{n + 1} \ne a_n$
then $\RR$ is a well-founded relation.
Theorem: Subset Relation on Power Set is Partial Ordering

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $\struct {\powerset S, \subseteq}$ be the relational structure defined on $\powerset S$ by the subset relation $\subseteq$.
Then $\struct {\powerset S, \subseteq}$ is an ordered set.
The ordering $\subseteq$ is partial {{iff}} $S$ is neither empty nor a singleton; otherwise it is total.

Proof:
From Subset Relation is Ordering, we have that $\subseteq$ is an ordering on any set of subsets of a given set.
Suppose $S$ is neither a singleton nor the empty set.
Then $\exists a, b \in S$ such that $a \ne b$.
Then $\set a \in \powerset S$ and $\set b \in \powerset S$.
However, $\set a \nsubseteq \set b$ and $\set b \nsubseteq \set a$.
So by definition, $\subseteq$ is a partial ordering.
Now suppose $S = \O$.
Then $\powerset S = \set \O$ and, by Empty Set is Subset of All Sets, $\O \subseteq \O$.
Hence, trivially, $\subseteq$ is a total ordering on $\powerset S$.
Now suppose $S$ is a singleton: let $S = \set a$.
Then $\powerset S = \set {\O, \set a}$.
So there are only two elements of $\powerset S$, and we see that $\O \subseteq \set a$ from Empty Set is Subset of All Sets.
So, trivially again, $\subseteq$ is a total ordering on $\powerset S$.
{{qed}}
Theorem: Ordering is Equivalent to Subset Relation

Let $\struct {S, \preceq}$ be an ordered set.
Then there exists a set $\mathbb S$ of subsets of $S$ such that:
:$\struct {S, \preceq} \cong \struct {\mathbb S, \subseteq}$
where:
:$\struct {\mathbb S, \subseteq}$ is the relational structure consisting of $\mathbb S$ and the subset relation
:$\cong$ denotes order isomorphism.
Hence any ordering on a set can be modelled uniquely by a set of subsets of that set under the subset relation.
Specifically:
Let
:$\mathbb S := \set {a^\preceq: a \in S}$
where $a^\preceq$ is the lower closure of $a$.
That is:
:$a^\preceq := \set {b \in S: b \preceq a}$
Let the mapping $\phi: S \to \mathbb S$ be defined as:
:$\map \phi a = a^\preceq$
Then $\phi$ is an order isomorphism from $\struct {S, \preceq}$ to $\struct {\mathbb S, \subseteq}$.

Proof:
From Subset Relation is Ordering, we have that $\struct {\mathbb S, \subseteq}$ is an ordered set.
Then let $T$ be defined as:
:$T := \set {a^\prec: a \in S}$
Let the mapping $\phi: S \to T$ be defined as:
:$\map \phi a = a^\prec$
We are to show that $\phi$ is an order isomorphism.
$\phi$ is clearly surjective, as every $a^\prec$ is defined from some $a \in S$.
Now suppose $x^\prec, y^\prec \in T: x^\prec = y^\prec$.
Then:
:$\set {b \in S: b \preceq x} = \set {b \in S: b \preceq y}$
We have that:
:$x \in x^\prec = y^\prec$ and $y \in y^\prec = x^\prec$
which means:
:$x \preceq y$ and $y \preceq x$
So as an ordering is antisymmetric, we have $x = y$ and so $\phi$ is injective.
Hence by definition, $\phi$ is a bijection.
Now let $a_1 \preceq a_2$.
Then by definition:
:$a_1 \in {a_2}^\prec$
Let $a_3 \in {a_1}^\prec$.
Then by definition:
:$a_3 \preceq a_1$
As an ordering is transitive, it follows that:
:$a_3 \preceq a_2$
and so:
:$a_3 \in {a_2}^\prec$
So by definition of a subset:
:${a_1}^\prec \subseteq {a_2}^\prec$
Therefore, $\phi$ is order-preserving
Conversely, suppose that ${a_1}^\prec \subseteq {a_2}^\prec$.
Then, since $a_1 \in {a_1}^\prec$, also $a_1 \in {a_2}^\prec$ by definition of subset.
By definition of ${a_2}^\prec$:
:$a_1 \preceq a_2$
Hence it is seen that $\phi^{-1}$ is also order-preserving.
Thus it follows that $\phi$ is an order isomorphism between $\struct {S, \preceq}$ and $\struct {\mathbb S, \subseteq}$.
{{qed}}
Theorem: Ordering is Equivalent to Subset Relation

Let $\struct {S, \preceq}$ be an ordered set.
Then there exists a set $\mathbb S$ of subsets of $S$ such that:
:$\struct {S, \preceq} \cong \struct {\mathbb S, \subseteq}$
where:
:$\struct {\mathbb S, \subseteq}$ is the relational structure consisting of $\mathbb S$ and the subset relation
:$\cong$ denotes order isomorphism.
Hence any ordering on a set can be modelled uniquely by a set of subsets of that set under the subset relation.
Specifically:
Let
:$\mathbb S := \set {a^\preceq: a \in S}$
where $a^\preceq$ is the lower closure of $a$.
That is:
:$a^\preceq := \set {b \in S: b \preceq a}$
Let the mapping $\phi: S \to \mathbb S$ be defined as:
:$\map \phi a = a^\preceq$
Then $\phi$ is an order isomorphism from $\struct {S, \preceq}$ to $\struct {\mathbb S, \subseteq}$.

Proof:
First a lemma:
=== Lemma ===
{{:Ordering is Equivalent to Subset Relation/Lemma}}{{qed|lemma}}
From Subset Relation is Ordering, we have that $\struct {\mathbb S, \subseteq}$ is an ordered set.
We are to show that $\phi$ is an order isomorphism.
$\phi$ is clearly surjective, as every $a^\preceq$ is defined from some $a \in S$.
By the Lemma, $\phi$ is order-preserving.
Suppose that ${a_1}^\preceq \subseteq {a_2}^\preceq$.
We have that:
:$a_1 \in {a_1}^\preceq$
Thus by definition of subset:
:$a_1 \in {a_2}^\preceq$
By definition of ${a_2}^\preceq$:
:$a_1 \preceq a_2$
Thus $\phi$ is also order-reflecting.
Thus it follows that $\phi$ is an order isomorphism between $\struct {S, \preceq}$ and $\struct {\mathbb S, \subseteq}$.
{{qed}}