avewright/proofwiki-math huggingface dataset:
Theorem: Inverse of Injective and Surjective Mapping is Mapping

Let $f: S \to T$ be a mapping such that:
:$(1): \quad f$ is an injection
:$(2): \quad f$ is a surjection.
Then the inverse $f^{-1}$ of $f$ is itself a mapping.

Proof:
Let $f: S \to T$ be a mapping such that:
::$(1): \quad f$ is an injection
::$(2): \quad f$ is a surjection.
Let $t \in T$.
Then as $f$ is a surjection:
:$\exists s \in S: t = \map f s$
As $f$ is an injection, there is only one $s \in S$ such that $t = \map f s$.
Define $\map g t = s$.
As $t \in T$ is arbitrary, it follows that:
:$\forall t \in T: \exists s \in S: \map g t = s$
such that $s$ is unique for a given $t$.
That is, $g: T \to S$ is a mapping.
By the definition of $g$:
:$(1): \quad \forall t \in T: \map f {\map g t} = t$
Let $s \in S$.
Let:
:$(2): \quad s' = \map g {\map f s}$
Then:
{{begin-eqn}}
{{eqn | l = \map f {s'}
      | r = \map f {\map g {\map f s} }
      | c = 
}}
{{eqn | r = \map f s
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = s
      | r = s'
      | c = as $f$ is an injection
}}
{{eqn | r = \map g {\map f s}
      | c = from $(2)$
}}
{{end-eqn}}
Thus $f: S \to T$ and $g: T \to S$ are inverse mappings of each other.
{{qed}}
Theorem: Inverse is Mapping implies Mapping is Injection and Surjection

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let the inverse $f^{-1} \subseteq T \times S$ itself be a mapping.
Then:
:$(1): \quad f$ is an injection
:$(2): \quad f$ is a surjection.

Proof:
This is divided into two parts:
Theorem: Maximal Left and Right Ideal iff Quotient Ring is Division Ring/Quotient Ring is Division Ring implies Maximal Right Ideal

Let $R$ be a ring with unity.
Let $J$ be an ideal of $R$.
If the quotient ring $R / J$ is a division ring then $J$ is a maximal right ideal.

Proof:
Let $K$ be a right ideal of $R$ such that $J \subsetneq K \subset R$.
Let $x \in K \setminus  J$.
As $x \notin J$ then $x + J \ne J$, the zero in $R / J$.
As $R / J$ is a division ring then $x + J \in R / J$ has an inverse, say $s + J$.
That is:
:$1_R + J = \paren {x + J} \circ \paren {s + J} = \paren {x \circ s} + J$
By Left Cosets are Equal iff Product with Inverse in Subgroup then:
:$1_R - x \circ s \in J \subsetneq K$
By the definition of a right ideal:
:$x \in K$ and $s \in R \implies x \circ s \in K$
:$1_R - x \circ s \in K$ and $x \circ s \in K \implies \paren {1_R - x \circ s} + \paren {x \circ s} = 1_R \in K$
:$1_R \in K \implies \forall y \in R, 1_R \circ y = y \in K$
Hence $K = R$
The result follows.
Theorem: Maximal Left and Right Ideal iff Quotient Ring is Division Ring/Quotient Ring is Division Ring implies Maximal Left Ideal

Let $R$ be a ring with unity.
Let $J$ be an ideal of $R$.
If the quotient ring $R / J$ is a division ring then $J$ is a maximal left ideal.

Proof:
Let $K$ be a left ideal of $R$ such that $J \subsetneq K \subset R$.
Let $x \in K \setminus J$.
As $x \notin J$, then $x + J \ne J$, the zero in $R / J$.
As $R / J$ is a division ring, $x + J \in R / J$ has an inverse, say $s + J$.
That is:
:$1_R + J =  \paren {s + J} \circ \paren {x + J} = \paren {s \circ x} + J$
By Left Cosets are Equal iff Product with Inverse in Subgroup then:
:$1_R - s \circ x \in J \subsetneq K$
By the definition of a left ideal then:
:$x \in K$ and $s \in R \implies s \circ x \in K$
:$1_R - s \circ x \in K$ and $s \circ x \in K \implies \paren {1_R - s \circ x} + \paren {s \circ x } = 1_R \in K$
:$1_R \in K \implies \forall y \in R, y \circ 1_R = y \in K$
Hence $K = R$
The result follows.
Theorem: Quotient Ring of Cauchy Sequences is Division Ring

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\CC$ be the ring of Cauchy sequences over $R$.
Let $\NN$ be the set of null sequences.
Then the quotient ring $\CC / \NN$ is a division ring.

Proof:
By Null Sequences form Maximal Left and Right Ideal then $\NN$ is an ideal of the ring $\CC$ that is also a maximal left ideal.
By Maximal Left and Right Ideal iff Quotient Ring is Division Ring then the quotient ring $\CC / \NN$ is a division ring
{{qed}}
Theorem: Hilbert Proof System Instance 2 Independence Results/Independence of A1

Axiom $(A1)$ is independent from $(A2)$, $(A3)$, $(A4)$.

Proof:
Denote with $\mathscr H_2 - (A1)$ the proof system resulting from $\mathscr H_2$ by removing axiom $(A1)$.
Consider $\mathscr C_2$, Instance 2 of constructed semantics.
We will prove that:
* $\mathscr H_2 - (A1)$ is sound for $\mathscr C_2$;
* Axiom $(A1)$ is not a tautology in $\mathscr C_2$
which leads to the conclusion that $(A1)$ is not a theorem of $\mathscr H_2 - (A1)$.
Theorem: Embedding Ring into Ring Structure Induced by Ring Operations

Let $\struct {R, +, \circ}$ be a ring.
Let $S$ be a non-empty set.
Let $\struct {R^S, +', \circ'}$ be the ring of mappings, where $+'$ and $\circ'$ are the pointwise operations induced on $R^S$ by $+$ and $\circ$.
For each $r \in R$, let $f_r: S \to R$ be the mapping defined by:
:$\forall s \in S, \map {f_r} s = r$
That is, $f_r$ is the constant mapping from $S$ to $r$.
Let $\phi: R \to R^S$ be the mapping from the ring $R$ to the ring $R^S$ defined by:
:$\forall r \in R: \map \phi r = f_r$
Then:
:$\phi$ is a ring monomorphism.

Proof:
By the definition of a ring monomorphism it is sufficient to prove for all $r, r' \in R$ that:
:$\quad \map \phi {r + r'} = \map \phi r +' \map \phi {r'}$
:$\quad \map \phi {r \circ r'} = \map \phi r \circ' \map \phi {r'}$
:$\quad r \ne r' \implies \map \phi r \ne \map \phi {r'}$
That is, for all $r, r' \in R$ it needs to be shown that:
:$(1): \quad f_{r + r' } = f_r +' f_{r'}$
:$(2): \quad f_{r \circ r' } = f_r \circ' f_{r'}$
:$(3): \quad r \ne r' \implies f_r \ne f_{r'}$
Theorem: Embedding Normed Division Ring into Ring of Cauchy Sequences

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\CC$ be the ring of Cauchy sequences over $R$
Let $\phi: R \to \CC$ be the mapping from $R$ to $\CC$ defined as:
:$\forall a \in R: \map \phi a = \tuple {a, a, a, \dots}$
where $\tuple {a, a, a, \dots}$ is the constant sequence.
Then $\phi$ is a ring monomorphism.

Proof:
By Cauchy Sequences form Ring with Unity, $\CC$ is a subring of the ring of sequences over $R$.
Let $i: \CC \to  R^\N$ be the inclusion mapping of $\CC$ into the ring of sequences.
By Embedding Ring into Ring Structure Induced by Ring Operations the composition $i \circ \phi: R \to R^\N$ is a ring monomorphism.
Since for all $a \in R$, we have that:
:$\map {\paren {i \circ \phi} } a = \map \phi a$
The result follows.
{{qed}}
Theorem: Hilbert Proof System Instance 2 Independence Results/Independence of A2

Axiom $(A2)$ is independent from $(A1)$, $(A3)$, $(A4)$.

Proof:
Denote with $\mathscr H_2 - (A2)$ the proof system resulting from $\mathscr H_2$ by removing axiom $(A2)$.
Consider $\mathscr C_3$, Instance 3 of constructed semantics.
We will prove that:
* $\mathscr H_2 - (A2)$ is sound for $\mathscr C_3$;
* Axiom $(A2)$ is not a tautology in $\mathscr C_3$
which leads to the conclusion that $(A2)$ is not a theorem of $\mathscr H_2 - (A2)$.
Theorem: Definition:Constructed Semantics/Instance 3/Rule of Idempotence

The Rule of Idempotence:
:$(p \lor p) \implies p$
is a tautology in Instance 3 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Idempotence can be written as:
: $\neg \left({p \lor p}\right) \lor p$
This evaluates as follows:
:$\begin{array}{|cccc|c|c|} \hline
\neg & (p & \lor & p) & \lor & p \\
\hline
2 & 0 & 0 & 0 & 0 & 0 \\
1 & 1 & 1 & 1 & 1 & 1 \\
0 & 2 & 2 & 2 & 0 & 2 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
asmpzabvq5k0cfuq8tclysj6vp07fjk
Theorem: Definition:Constructed Semantics/Instance 3/Rule of Commutation

The Rule of Commutation:
:$\left({p \lor q}\right) \implies \left({q \lor p}\right)$
is a tautology in Instance 3 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Commutation can be written as:
:$\neg \left({p \lor q}\right) \lor \left({q \lor p}\right)$
This evaluates as follows:
:$\begin{array}{|cccc|c|ccc|} \hline
\neg & (p & \lor & q) & \lor & (q & \lor & p) \\
\hline
2 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\
2 & 0 & 0 & 1 & 0 & 1 & 0 & 0 \\
2 & 0 & 0 & 2 & 0 & 2 & 0 & 0 \\
2 & 1 & 0 & 0 & 0 & 0 & 0 & 1 \\
1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 \\
0 & 1 & 2 & 2 & 0 & 2 & 2 & 1 \\
2 & 2 & 0 & 0 & 0 & 0 & 0 & 2 \\
0 & 2 & 2 & 1 & 0 & 1 & 2 & 2 \\
0 & 2 & 2 & 2 & 0 & 2 & 2 & 2 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
04e31w1poro9dfijnymy5oqr9occrh6
Theorem: Definition:Constructed Semantics/Instance 3/Factor Principle

The Factor Principle:
:$\paren {p \implies q} \implies \paren {\paren {r \lor p} \implies \paren {r \lor q} }$
is a tautology in Instance 3 of constructed semantics.

Proof:
{{handwaving}}
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Factor Principle can be written as:
:$\neg \paren {\neg p \lor q} \lor \paren {\neg \paren {r \lor p} \lor \paren {r \lor q} }$
This evaluates as follows:
:$\begin{array}{|ccccc|c|cccccccc|} \hline
\neg & (\neg & p & \lor & q) & \lor & (\neg & (r & \lor & p) & \lor & (r & \lor & q)) \\
\hline
0 & 2 & 0 & 0 & 0 & 0 & 2 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\
0 & 2 & 1 & 0 & 0 & 0 & 2 & 0 & 0 & 1 & 0 & 0 & 0 & 0 \\
0 & 2 & 2 & 0 & 0 & 0 & 2 & 0 & 0 & 2 & 0 & 0 & 0 & 0 \\
0 & 2 & 0 & 0 & 0 & 0 & 2 & 1 & 0 & 0 & 0 & 1 & 0 & 0 \\
0 & 2 & 1 & 0 & 0 & 0 & 1 & 1 & 1 & 1 & 0 & 1 & 0 & 0 \\
0 & 2 & 2 & 0 & 0 & 0 & 0 & 1 & 2 & 2 & 0 & 1 & 0 & 0 \\
0 & 2 & 0 & 0 & 0 & 0 & 2 & 2 & 0 & 0 & 0 & 2 & 0 & 0 \\
0 & 2 & 1 & 0 & 0 & 0 & 0 & 2 & 2 & 1 & 0 & 2 & 0 & 0 \\
0 & 2 & 2 & 0 & 0 & 0 & 0 & 2 & 2 & 2 & 0 & 2 & 0 & 0 \\
0 & 2 & 0 & 0 & 1 & 0 & 2 & 0 & 0 & 0 & 0 & 0 & 0 & 1 \\
1 & 1 & 1 & 1 & 1 & 0 & 2 & 0 & 0 & 1 & 0 & 0 & 0 & 1 \\
2 & 0 & 2 & 2 & 1 & 0 & 2 & 0 & 0 & 2 & 0 & 0 & 0 & 1 \\
0 & 2 & 0 & 0 & 1 & 0 & 2 & 1 & 0 & 0 & 2 & 1 & 1 & 1 \\
1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 \\
2 & 0 & 2 & 2 & 1 & 0 & 0 & 1 & 2 & 2 & 0 & 1 & 1 & 1 \\
0 & 2 & 0 & 0 & 1 & 0 & 2 & 2 & 0 & 0 & 2 & 2 & 2 & 1 \\
1 & 1 & 1 & 1 & 1 & 0 & 0 & 2 & 2 & 1 & 0 & 2 & 2 & 1 \\
2 & 0 & 2 & 2 & 1 & 0 & 0 & 2 & 2 & 2 & 0 & 2 & 2 & 1 \\
0 & 2 & 0 & 2 & 2 & 0 & 2 & 0 & 0 & 0 & 0 & 0 & 0 & 2 \\
0 & 1 & 1 & 2 & 2 & 0 & 2 & 0 & 0 & 1 & 0 & 0 & 0 & 2 \\
2 & 0 & 2 & 0 & 2 & 0 & 2 & 0 & 0 & 2 & 0 & 0 & 0 & 2 \\
0 & 2 & 0 & 2 & 2 & 0 & 2 & 1 & 0 & 0 & 2 & 1 & 2 & 2 \\
0 & 1 & 1 & 2 & 2 & 0 & 1 & 1 & 1 & 1 & 2 & 1 & 2 & 2 \\
2 & 0 & 2 & 0 & 2 & 0 & 0 & 1 & 2 & 2 & 0 & 1 & 2 & 2 \\
0 & 2 & 0 & 2 & 2 & 0 & 2 & 2 & 0 & 0 & 2 & 2 & 2 & 2 \\
0 & 1 & 1 & 2 & 2 & 0 & 0 & 2 & 2 & 1 & 0 & 2 & 2 & 2 \\
2 & 0 & 2 & 0 & 2 & 0 & 0 & 2 & 2 & 2 & 0 & 2 & 2 & 2 \\
\hline
\end{array}$
{{qed}}
{{proofread}}
Category:Formal Semantics
sct445blae6xeaskx2zcx2toqh9j1dr
Theorem: Hilbert Proof System Instance 2 Independence Results/Independence of A3

Axiom $(A3)$ is independent from $(A1)$, $(A2)$, $(A4)$.

Proof:
{{tidy}}
Denote with $\mathscr H_2 - (A3)$ the proof system resulting from $\mathscr H_2$ by removing axiom $(A3)$.
Consider $\mathscr C_4$, Instance 4 of constructed semantics.
We will prove that:
* $\mathscr H_2 - (A3)$ is sound for $\mathscr C_4$;
* Axiom $(A3)$ is not a tautology in $\mathscr C_4$
which leads to the conclusion that $(A3)$ is not a theorem of $\mathscr H_2 - (A3)$.
Theorem: Definition:Constructed Semantics/Instance 4/Rule of Idempotence

The Rule of Idempotence:
:$(p \lor p) \implies p$
is a tautology in Instance 4 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Idempotence can be written as:
: $\neg \left({p \lor p}\right) \lor p$
This evaluates as follows:
:$\begin{array}{|cccc|c|c|} \hline
\neg & (p & \lor & p) & \lor & p \\
\hline
1 & 0 & 0 & 0 & 0 & 0 \\
0 & 1 & 1 & 1 & 0 & 1 \\
0 & 2 & 2 & 2 & 0 & 2 \\
2 & 3 & 3 & 3 & 0 & 3 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
01yq3v78ftnoxwrey60d9xk091x9ahx
Theorem: Definition:Constructed Semantics/Instance 4/Rule of Addition

The Rule of Addition:
:$q \implies (q \lor p)$
is a tautology in Instance 4 of constructed semantics.

Proof:
{{handwaving}}
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Addition can be written as:
: $\neg q \lor \left({p \lor q}\right)$
This evaluates as follows:
:$\begin{array}{|cc|c|ccc|} \hline
\neg & q & \lor & (p & \lor & q) \\
\hline
1 & 0 & 0 & 0 & 0 & 0 \\
0 & 1 & 0 & 0 & 0 & 1 \\
0 & 2 & 0 & 0 & 0 & 2 \\
2 & 3 & 0 & 0 & 0 & 3 \\
1 & 0 & 0 & 1 & 0 & 0 \\
0 & 1 & 0 & 1 & 1 & 1 \\
0 & 2 & 0 & 1 & 2 & 2 \\
2 & 3 & 0 & 1 & 3 & 3 \\
1 & 0 & 0 & 2 & 0 & 0 \\
0 & 1 & 0 & 2 & 2 & 1 \\
0 & 2 & 0 & 2 & 2 & 2 \\
2 & 3 & 0 & 2 & 0 & 3 \\
1 & 0 & 0 & 3 & 0 & 0 \\
0 & 1 & 0 & 3 & 3 & 1 \\
0 & 2 & 0 & 3 & 3 & 2 \\
2 & 3 & 0 & 3 & 3 & 3 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
5hf2kbaogy667algmc2jorctor673g1
Theorem: Cardinality of Set of Surjections

Let $S$ and $T$ be finite sets.
Let $\card S = m, \card T = n$.
Let $C$ be the number of surjections from $S$ to $T$.
Then:
:$C = n! \ds {m \brace n}$
where $\ds {m \brace n}$ denotes a Stirling number of the second kind.

Proof:
Let $T$ be the codomain of a surjection $f$ from $S$ to $T$.
By the Quotient Theorem for Surjections, $f$ induces an equivalence $\RR_f$ on $T$:
:$f = r \circ q_{\RR_f}$
where:
:$\RR_f$ is the equivalence induced by $f$ on $T$
:$r: S / \RR_f \to T$ is a bijection from the quotient set $S / \RR_f$ to $T$
:$q_{\RR_f}: S \to S / \RR_f$ is the quotient mapping induced by $\RR_f$.
From the Fundamental Theorem on Equivalence Relations, $\RR_f$ induces a partition on $S$.
From Cardinality of Set of Induced Equivalence Classes of Surjection, $\RR_f$ has $m$ components.
From Number of Set Partitions by Number of Components, there are $\ds {m \brace n}$ different ways of performing such a partitioning.
From Cardinality of Set of Injections, there are $n!$ different bijections from $S / \RR_f \to T$.
The total number of surjections is then the product of these:
:$C = n! \ds {m \brace n}$
{{qed}}
Theorem: Hilbert Proof System Instance 2 Independence Results/Independence of A4

Axiom $(\text A 4)$ is independent from $(\text A 1)$, $(\text A 2)$, $(\text A 3)$.

Proof:
Denote with $\mathscr H_2 - (\text A 4)$ the proof system resulting from $\mathscr H_2$ by removing axiom $(\text A 4)$.
Consider $\mathscr C_5$, Instance 5 of constructed semantics.
We will prove that:
* $\mathscr H_2 - (\text A 4)$ is sound for $\mathscr C_5$;
* Axiom $(\text A 4)$ is not a tautology in $\mathscr C_5$
which leads to the conclusion that $(\text A 4)$ is not a theorem of $\mathscr H_2 - (\text A 4)$.
Theorem: Image of Set Difference under Mapping/Corollary 3

Let $f: S \to T$ be a surjection.
Let $A \subseteq S$ be a subset of $S$.
Then:
:$T \setminus f \sqbrk A \subseteq f \sqbrk {S \setminus A}$
where $\setminus$ denotes set difference.

Proof:
As $T$ is a surjection, $T = f \sqbrk S$.
Thus Image of Set Difference under Mapping can be applied:
:$f \sqbrk S \setminus f \sqbrk A \subseteq f \sqbrk {S \setminus A}$
{{qed}}
Theorem: Definition:Constructed Semantics/Instance 5/Rule of Idempotence

The Rule of Idempotence:
:$(p \lor p) \implies p$
is a tautology in Instance 5 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Idempotence can be written as:
: $\neg \left({p \lor p}\right) \lor p$
This evaluates as follows:
:$\begin{array}{|cccc|c|c|} \hline
\neg & (p & \lor & p) & \lor & p \\
\hline
1 & 0 & 0 & 0 & 0 & 0 \\
0 & 1 & 1 & 1 & 0 & 1 \\
3 & 2 & 2 & 2 & 0 & 2 \\
0 & 3 & 3 & 3 & 0 & 3 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
5wfsgwvosz5m5ujv2gjtoogcqm6423d
Theorem: Additive Function is Linear for Rational Factors

Let $f: \R \to \R$ be an additive function.
Then:
:$\forall r \in \Q, x \in \R: \map f {x r} = r \map f x$

Proof:
Trivially, we have:
:$\forall x \in \R: \map f {1 \cdot x} = 1 \map f x$
Next, suppose that:
:$\map f {n x} = n \map f x$
By additivity of $f$, we have:
{{begin-eqn}}
{{eqn | l = \map f {\paren {n + 1} x}
      | r = \map f {n x + x}
      | c = 
}}
{{eqn | r = \map f {n x} + \map f x = n \map f x + \map f x
      | c = 
}}
{{eqn | r = \paren {n + 1} \map f x
      | c = 
}}
{{end-eqn}}
Hence by the Principle of Mathematical Induction:
:$\forall n \in \N, x \in \R: \map f {n x} = n \map f x$
As Additive Function is Odd Function and Odd Function of Zero is Zero, we conclude:
:$\forall p \in \Z, x \in \R: \map f {p x} = p \map f x$
Let $p \ne 0$.
By substituting $y = p x$, the above gives:
:$\forall p \in \Z \setminus \set 0, y \in \R: \map f y = p \map f {\dfrac y p}$
In other words:
:$\forall p \in \Z \setminus \set 0, y \in \R: \map f {\dfrac y p} = \dfrac 1 p \map f y$
Given $p, q \in \Z, q \ne 0$, we have:
{{begin-eqn}}
{{eqn | l = \map f {\dfrac p q} x
      | r = \map f {p \dfrac x q}
      | c = 
}}
{{eqn | r = p \map f {\dfrac x q}
      | c = 
}}
{{eqn | r = p \dfrac {\map  f x } q
      | c = 
}}
{{eqn | r = \dfrac p q \map f x
      | c = 
}}
{{end-eqn}}
Therefore we conclude:
:$\forall r \in \Q, x \in \R: \map f {r x} = r \map f x$
{{qed}}
Category:Additive Functions
eqdjuus0anhucf1i4tkx21zvf7hvhwr
Theorem: Definition:Constructed Semantics/Instance 5/Rule of Addition

The Rule of Addition:
:$q \implies (q \lor p)$
is a tautology in Instance 5 of constructed semantics.

Proof:
{{handwaving}}
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Addition can be written as:
: $\neg q \lor \left({p \lor q}\right)$
This evaluates as follows:
:$\begin{array}{|cc|c|ccc|} \hline
\neg & q & \lor & (p & \lor & q) \\
\hline
1 & 0 & 0 & 0 & 0 & 0 \\
0 & 1 & 0 & 0 & 0 & 1 \\
3 & 2 & 0 & 0 & 0 & 2 \\
0 & 3 & 0 & 0 & 0 & 3 \\
1 & 0 & 0 & 1 & 0 & 0 \\
0 & 1 & 0 & 1 & 1 & 1 \\
3 & 2 & 0 & 1 & 2 & 2 \\
0 & 3 & 0 & 1 & 3 & 3 \\
1 & 0 & 0 & 2 & 0 & 0 \\
0 & 1 & 0 & 2 & 2 & 1 \\
3 & 2 & 0 & 2 & 2 & 2 \\
0 & 3 & 0 & 2 & 0 & 3 \\
1 & 0 & 0 & 3 & 0 & 0 \\
0 & 1 & 0 & 3 & 3 & 1 \\
3 & 2 & 0 & 3 & 0 & 2 \\
0 & 3 & 0 & 3 & 3 & 3 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
9qn6oodis4tald5nfqxy6512l4cavu8
Theorem: Definition:Constructed Semantics/Instance 5/Rule of Commutation

The Rule of Commutation:
:$\left({p \lor q}\right) \implies \left({q \lor p}\right)$
is a tautology in Instance 5 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Commutation can be written as:
:$\neg \left({p \lor q}\right) \lor \left({q \lor p}\right)$
This evaluates as follows:
:$\begin{array}{|cccc|c|ccc|} \hline
\neg & (p & \lor & q) & \lor & (q & \lor & p) \\
\hline
1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\
1 & 0 & 0 & 1 & 0 & 1 & 0 & 0 \\
1 & 0 & 0 & 2 & 0 & 2 & 0 & 0 \\
1 & 0 & 0 & 3 & 0 & 3 & 0 & 0 \\
1 & 1 & 0 & 0 & 0 & 0 & 0 & 1 \\
0 & 1 & 1 & 1 & 0 & 1 & 1 & 1 \\
3 & 1 & 2 & 2 & 0 & 2 & 2 & 1 \\
0 & 1 & 3 & 3 & 0 & 3 & 3 & 1 \\
1 & 2 & 0 & 0 & 0 & 0 & 0 & 2 \\
3 & 2 & 2 & 1 & 0 & 1 & 2 & 2 \\
3 & 2 & 2 & 2 & 0 & 2 & 2 & 2 \\
1 & 2 & 0 & 3 & 0 & 3 & 0 & 2 \\
1 & 3 & 0 & 0 & 0 & 0 & 0 & 3 \\
0 & 3 & 3 & 1 & 0 & 1 & 3 & 3 \\
1 & 3 & 0 & 2 & 0 & 2 & 0 & 3 \\
0 & 3 & 3 & 3 & 0 & 3 & 3 & 3 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
emlja2kbsygf1qleayueqncwq850mjn
Theorem: Additive Function of Zero is Zero

Let $f: \R \to \R$ be an additive function.
Then:
:$\map f 0 = 0$

Proof:
As $f$ is additive, we have:
{{begin-eqn}}
{{eqn | l = \map f 1
      | r = \map f {0 + 1}
      | c = Real Addition Identity is Zero
}}
{{eqn | r = \map f 0 + \map f 1
      | c = {{Defof|Additive Function (Algebra)|Additive Function}}
}}
{{end-eqn}}
that is:
:$\map f 0 = 0$
{{qed}}
Category:Additive Functions
3ioacdfc93s5jdeuwntlbgb3vkqokgv
Theorem: Additive Function is Odd Function

Let $f: \R \to \R$ be an additive function.
Then $f$ is an odd function.

Proof:
From Additive Function of Zero is Zero:
:$\map f 0 = 0$
Thus, for all $x \in \R$, we have:
{{begin-eqn}}
{{eqn | l = 0
      | r = \map f 0
      | c = 
}}
{{eqn | r = \map f {x + \paren {-x} }
      | c = 
}}
{{eqn | r = \map f x + \map f {-x}
      | c = 
}}
{{end-eqn}}
It follows that the function $f$ is odd:
:$\forall x \in \R: \map f {-x} = -\map f x$.
{{qed}}
Category:Additive Functions
Category:Odd Functions
b5l5j526vnkbkn4xsi5hkzkgoz8cynj
Theorem: Difference of Images under Mapping not necessarily equal to Image of Difference

Let $f: S \to T$ be a mapping.
The image of the set difference of two subsets of $S$ is not necessarily equal to the set difference of the images.
That is:
Let $S_1$ and $S_2$ be subsets of $S$.
Then it is not always the case that:
:$f \sqbrk {S_1} \setminus f \sqbrk {S_2} = f \sqbrk {S_1 \setminus S_2}$
where $\setminus$ denotes set difference.

Proof:
Note that from Image of Set Difference under Mapping:
:$f \sqbrk {S_1} \setminus f \sqbrk {S_2} \subseteq f \sqbrk {S_1 \setminus S_2}$
By Proof by Counterexample it is demonstrated that the inclusion does not necessarily apply in the other direction.
Let:
:$S_1 = \set {x \in \Z: x \le 0}$
:$S_2 = \set {x \in \Z: x \ge 0}$
:$f: \Z \to \Z: \forall x \in \Z: \map f x = x^2$
We have:
:$S_1 \setminus S_2 = \set {-1, -2, -3, \ldots}$
:$f \sqbrk {S_1} = \set {0, 1, 4, 9, 16, \ldots} = f \sqbrk {S_2}$
Then from Set Difference with Self is Empty Set:
:$f \sqbrk {S_1} \setminus f \sqbrk {S_2} = \O$
but:
:$f \sqbrk {S_1 \setminus S_2} = f \sqbrk {\set {x \in \Z: x > 0} } = \set {1, 4, 9, 16, \ldots}$
Theorem: Cross-Relation on Real Numbers is Equivalence Relation

Let $\R^2$ denote the cartesian plane.
Let $\alpha$ denote the relation defined on $\R^2$ by:
:$\tuple {x_1, y_1} \mathrel \alpha \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
Then $\alpha$ is an equivalence relation on $\R^2$.

Proof:
$\alpha$ is an instance of a cross-relation.
We also have that Real Addition is Commutative.
The result therefore follows from Cross-Relation is Equivalence Relation.
{{qed}}
Theorem: Cross-Relation on Real Numbers is Equivalence Relation/Geometrical Interpretation

The equivalence classes of $\alpha$, when interpreted as points in the plane, are the straight lines of slope $1$.

Proof:
We have from Cross-Relation on Real Numbers is Equivalence Relation that $\alpha$ is an equivalence relation.
Thus:
{{begin-eqn}}
{{eqn | l = \tuple {x_1, y_1}
      | o = \alpha
      | r = \tuple {x_2, y_2}
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = x_1 + y_2
      | r = x_2 + y_1
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = x_1 - y_1
      | r = x_2 - y_2
      | c =
}}
{{end-eqn}}
Thus each equivalence classes consists of sets of points such that:
:$x - y = c$
That is:
:$y = x + c$
Thus from Equation of Straight Line in Plane, this is the equation of a straight line whose slope is $1$.
{{qed}}
Theorem: Subtraction on Numbers is Anticommutative/Natural Numbers

The operation of subtraction on the natural numbers $\N$ is anticommutative, and defined only when $a = b$:
That is:
:$a - b = b - a \iff a = b$

Proof:
$a - b$ is defined on $\N$ only if $a \ge b$.
If $a > b$, then although $a - b$ is defined, $b - a$ is not.
So for $a - b = b - a$ it is necessary for both to be defined.
This happens only when $a = b$.
Hence the result.