nyuuzyou/wikis huggingface dataset:
Recursively Defined Mapping/Examples/Factorial

== Example of Recursively Defined Mapping ==
The facorial of a positive integer $n$ can be defined recursively as:
:$\map f n = \begin {cases} 0 & : n = 1 \\ n \map f {n - 1} & : n > 1 \end {cases}$
== Sources ==
* 
* 
Category:Examples of Recursively Defined Mappings
Recursively Defined Sequence/Examples/Minimum over k of Maximum of 1 plus Function of k and 2 plus Function of n-k

== Theorem ==
Consider the integer sequence $\sequence {\map f n}$ defined recusrively as:
:$\map f n = \begin{cases} 0 & : n = 1 \\
\ds \min_{0 \mathop < k \mathop < n} \map \max {1 + \map f k, 2 + \map f {n - k} } & : n > 1 \end{cases}$
$\map f n$ has a closed-form expression:
:$\map f n = m$ for $F_m < n \le F_{m + 1}$
where $F_m$ denotes the $m$th Fibonacci number.
== Proof ==
The proof proceeds by induction.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$\map f n = m$ for $F_m < n \le F_{m + 1}$
=== Basis for the Induction ===
$\map P 1$ is the case:
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P r$ is true, where $r \ge 1$, then it logically follows that $\map P {r + 1}$ is true.
So this is the induction hypothesis:
:$\map f r = m$ for $F_m < r \le F_{m + 1}$
from which it is to be shown that:
:$\map f {r + 1} = m$ for $F_m < {r + 1} \le F_{m + 1}$
=== Induction Step ===
This is the induction step:
So $\map P r \implies \map P {r + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 1}: \map f n = m$ for $F_m < n \le F_{m + 1}$
== Sources ==
* : $\S 1.2.8$: Fibonacci Numbers: Exercise $40$
Category:Integer Sequences
Category:Fibonacci Numbers
Recursively Defined Sequence/Examples/Term is Term of Index less 1 plus 6 times Term of Index less 2

== Theorem ==
Consider the integer sequence $\left\langle{a_n}\right\rangle$ defined recursively as:
:$a_n = \begin{cases} 0 & : n = 0 \\
1 & : n = 1 \\
a_{n - 1} + 6 a_{n - 2} & : \text{otherwise} \end{cases}$
$a_n$ has a closed-form expression:
:$a_n = \dfrac {3^n - \left({-2}\right)^n} 5$
== Proof ==
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $P \left({n}\right)$ be the proposition:
:$a_n = \dfrac {3^n - \left({-2}\right)^n} 5$
=== Basis for the Induction ===
$P \left({0}\right)$ is the case:
Thus $P \left({0}\right)$ is seen to hold.
$P \left({1}\right)$ is the case:
Thus $P \left({1}\right)$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $P \left({j}\right)$ is true, for all $j$ such that $0 \le j \le k$, then it logically follows that $P \left({k + 1}\right)$ is true.
This is the induction hypothesis:
:$a_k = \dfrac {3^k - \left({-2}\right)^k} 5$
and:
:$a_{k - 1} = \dfrac {3^{k - 1} - \left({-2}\right)^{k - 1} } 5$
from which it is to be shown that:
:$a_{k + 1} = \dfrac {3^{k + 1} - \left({-2}\right)^{k + 1} } 5$
=== Induction Step ===
This is the induction step:
So $P \left({k}\right) \implies P \left({k + 1}\right)$ and the result follows by the Second Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 0}: a_n = \dfrac {3^n - \left({-2}\right)^n} 5$
== Sources ==
* : $\S 1.2.8$: Fibonacci Numbers: Exercise $39$
Category:Integer Sequences
Recursively Enumerable Set is Image of Primitive Recursive Function

== Theorem ==
Let $S \subseteq \N$ be recursively enumerable.
Suppose $S$ is non-empty.
Then there exists a primitive recursive function $f : \N^k \to \N$ such that:
:$\Img f = S$
=== Corollary ===
== Proof ==
By definition of recursively enumerable, there exists a recursive function $g : \N^\ell \to \N$ such that:
:$\Img g = S$
By definition of non-empty, there exists some $x \in S$.
By Kleene's Normal Form Theorem, there exist:
* A primitive recursive relation $T \subset \N^{\ell + 2}$
* A primitive recursive function $U : \N \to \N$
such that a partial function $h : \N^\ell \to \N$ is recursive there exists $e \in \N$ such that:
:$\map h {x_1, \dotsc, x_\ell} \approx \map U {\mu z \map T {e, x_1, \dotsc, x_\ell, z}}$
for every $\tuple {x_1, \dotsc, x_\ell} \in \N^\ell$.
Thus, as $g$ is recursive, there exists such an $e$.
Define $V : \N^{\ell + 1} \to \N$ as:
:$\map V {x_1, \dotsc, x_\ell, t} = \map {\mu z \le t} {\map T {e, x_1, \dotsc, x_\ell, z}}$
$V$ is primitive recursive by Bounded Minimization is Primitive Recursive.
Define $f : \N^{\ell + 1} \to \N$ as:
:$\map f {x_1, \dotsc, x_\ell, t} = \begin{cases}
\map U {\map V {x_1, \dotsc, x_\ell, t}} & : \map V {x_1, \dotsc, x_\ell, t} \le t \\
x & : \map V {x_1, \dotsc, x_\ell, t} > t
\end{cases}$
By Definition by Cases is Primitive Recursive and Ordering Relations are Primitive Recursive, $f$ is primitive recursive.
It remains to show that $\Img f = \Img g$.
Suppose $y \in \Img g$.
Then, for some $\tuple {x_1, \dotsc, x_\ell} \in \N^\ell$:
:$\map g {x_1, \dotsc, x_\ell} = y$
Thus, by definition of $T$ and $U$:
:$\map U {\map {\mu z} {\map T {e, x_1, \dotsc, x_\ell, z}}} = y$
Let $t = \map {\mu z} {\map T {e, x_1, \dotsc, x_\ell, z}}$.
Hence:
:$\map V {x_1, \dotsc, x_\ell, t} = \map {\mu z} {\map T {e, x_1, \dotsc, x_\ell, z}} = t$.
Therefore, as $t \le t$:
:$\map f {x_1, \dotsc, x_\ell, t} = \map U t = y$.
Thus, $y \in \Img f$.
Now, suppose $y \in \Img f$.
Then there exists $\tuple {x_1, \dotsc, x_\ell, t} \in \N^{\ell + 1}$ such that:
:$\map f {x_1, \dotsc, x_\ell, t} = y$
By the definition of $f$, either:
:$\map U {\map V {x_1, \dotsc, x_\ell, t}} = y$ and $\map V {x_1, \dotsc, x_\ell, t} \le t$, or
:$x = y$ and $\map V {x_1, \dotsc, x_\ell, t} > t$.
In the second case, $x \in S = \Img g$ by definition.
In the first, let $r = \map V {x_1, \dotsc, x_\ell, t}$.
As $r \le t$, by definition of $V$ and bounded minimization:
:$r = \map {\mu z} {\map T {e, x_1, \dotsc, x_\ell, z}}$
But then, $y = \map U r = \map U {\map {\mu z} {\map T {e, x_1, \dotsc, x_\ell, z}}} = \map g {x_1, \dotsc, x_\ell}$.
Therefore, $y \in \Img g$.
Category:Recursion Theory
Recursively Enumerable Set is Image of Primitive Recursive Function/Corollary

== Theorem ==
Let $S \subseteq \N$ be recursively enumerable.
Suppose $S$ is non-empty.
Then there exists a primitive recursive function $f : \N \to \N$ such that:
:$\Img f = S$
== Proof ==
By Recursively Enumerable Set is Image of Primitive Recursive Function, there is some primitive recursive $g : \N^k \to \N$ such that:
:$\Img g = S$
As $S$ is non-empty, let $n \in S$.
Define:
:$\map f x = \begin{cases}
\map g {\map {\operatorname{pred}} {\paren{x}_1}, \dotsc, \map {\operatorname{pred}} {\paren{x}_k}} & : x \in \operatorname{Seq} \land \map {\operatorname{len}} x = k \\
n & : \text{otherwise}
\end{cases}$
That $f$ is primitive recursive follows from:
* Definition by Cases is Primitive Recursive/Corollary
* Predecessor Function is Primitive Recursive
* Set of Sequence Codes is Primitive Recursive
* Length Function is Primitive Recursive
* Equality Relation is Primitive Recursive
* Set Operations on Primitive Recursive Relations
* Prime Exponent Function is Primitive Recursive
Suppose $y \in \Img g$.
Then, there exist $\tuple {x_1, \dotsc, x_k} \in \N^k$ such that:
:$\map g {x_1, \dotsc, x_k} = y$
Let $X$ be the sequence coding for $\sequence {x_1 + 1, \dotsc, x_k + 1}$.
Then, $X \in \operatorname{Seq}$ and $\map {\operatorname{len}} X = k$.
Therefore, $\map f X = y$.
Now, suppose $y \in \Img f$.
Then, there exists $x \in \N$ such that:
:$\map f x = y$
If $x \in \operatorname{Seq} \land \map {\operatorname{len}} x = k$ holds, then:
:$y = \map g {\paren{x}_1 - 1, \dotsc, \paren{x}_k - 1}$
and thus $y \in \Img g$.
Otherwise, $y = n \in S$.
But as $S = \Img g$, it follows that $y \in \Img g$.
Category:Recursion Theory
Reduced Compton Wavelength of Electron

== Theorem ==
The Compton wavelength of the electron is:
=== Symbol ===
== Proof ==
By definition, the reduced Compton wavelength $\lambdabar_\E$ of an electron is given as:
:$\lambdabar_\E = \dfrac {\lambda_\E} {2 \pi}$
where $\lambda_\E$ denotes the Compton wavelength of the electron.
Then we have:
== Sources ==
* : $2$. Physical Constants and Conversion Factors: Table $2.3$ Adjusted Values of Constants
::which gives the mantissa as $3 \cdotp 861 \, 692$ with an uncertainty of $\pm 12$ corresponding to the $2$ least significant figures
Category:Reduced Compton Wavelength
Category:Electrons
Reduced Compton Wavelength of Proton

== Theorem ==
The Compton wavelength of the proton is:
=== Symbol ===
== Proof ==
By definition, the reduced Compton wavelength $\lambdabar_{\mathrm p}$ of a proton is given as:
:$\lambdabar_{\mathrm p} = \dfrac {\lambda_{\mathrm p} } {2 \pi}$
where $\lambda_{\mathrm p}$ denotes the Compton wavelength of the proton.
Then we have:
== Sources ==
* : $2$. Physical Constants and Conversion Factors: Table $2.3$ Adjusted Values of Constants
::which gives the mantissa as $3 \cdotp 861 \, 692$ with an uncertainty of $\pm 12$ corresponding to the $2$ least significant figures
Category:Reduced Compton Wavelength
Category:Protons
Reduced Echelon Matrix is Unique

== Theorem ==
Every $m \times n$ matrix is row equivalent to exactly one $m \times n$ reduced echelon matrix.
That is, the reduced echelon form of a matrix is unique.
== Proof ==
=== Proof of Existence ===
Proved in Matrix is Row Equivalent to Reduced Echelon Matrix.
=== Proof of Uniqueness ===
Category:Echelon Matrices
Reduced Gyromagnetic Ratio of Proton

== Theorem ==
The reduced gyromagnetic ratio of the proton is given by:
== Proof ==
By definition, the reduced gyromagnetic ratio of a proton is given as:
:$\dfrac {\gamma_{\mathrm p} } {2 \pi}$
where $\gamma_{\mathrm p}$ denotes the gyromagnetic ratio of the proton.
Then we have:
== Sources ==
* : $2$. Physical Constants and Conversion Factors: Table $2.3$ Adjusted Values of Constants
::which gives the mantissa as $4 \cdotp 257 \, 707$, with an uncertainty of $\pm 13$ corresponding to the $2$ least significant figures
Category:Reduced Gyromagnetic Ratio
Category:Protons
Reduced Gyromagnetic Ratio of Proton Uncorrected for Diamagnetism

== Theorem ==
The reduced gyromagnetic ratio of the proton, adjusted for diamagnetism, $\mathrm {H_2 O}$, is given by:
== Proof ==
== Sources ==
* : $2$. Physical Constants and Conversion Factors: Table $2.3$ Adjusted Values of Constants
Category:Gyromagnetic Ratio
Category:Protons
Reduced Residue System/Examples/Modulo 18/Arithmetic Sequence

== Examples of Reduced Residue Systems ==
The arithmetic sequence:
:$\set {5, 11, 17, 23, 29, 35}$
does not form a reduced residue system modulo $18$.
== Proof ==
We have:
Thus we see that:
:$\set {5, 11, 17, 23, 29, 35}$
is equivalent to:
:$\set {1, 5, 17}$
While $\set {1, 5, 17}$ are all coprime to $18$, they do not form a least positive reduced residue system modulo $18$, which is:
:$\set {1, 5, 7, 11, 13, 17}$
from Least Positive Reduced Residue System Modulo 18.
== Sources ==
* : $\text {4-2}$ Residue Systems: Exercise $2 \ \text {(b)}$
Category:Examples of Residue Systems
Reduced Residue System/Examples/Modulo 18/Least Positive Residues

== Examples of Reduced Residue Systems ==
The least positive reduced residue system of $18$ is the set of positive integers:
:$\set {1, 5, 7, 11, 13, 17}$
== Proof ==
The least positive residues of $18$ are:
:$S := \set {0, 1, 2, \dotsc, 17}$
We have that:
:$18 = 2 \times 3^2$
so the least positive reduced residue system of $18$ is the set of elements of $S$ which have neither $2$ or $3$ as a prime factor.
That is:
:$S \setminus \set {0, 2, 3, 4, 6, 8, 9, 10, 12, 14, 15, 16}$
Hence the result.
== Sources ==
* : $\text {4-2}$ Residue Systems: Exercise $2 \ \text {(d)}$
Category:Examples of Residue Systems
Reduced Residue System/Examples/Modulo 18/Powers of 5

== Examples of Reduced Residue Systems ==
The set of integers:
:$\set {1, 5, 25, 125, 625, 3125}$
forms a reduced residue system modulo $18$.
== Proof ==
We have:
Thus we see that:
:$\set {1, 5, 25, 125, 625, 3125}$
is equivalent to:
:$\set {1, 5, 7, 17, 13, 11}$
The result follows from Least Positive Reduced Residue System Modulo 18.
== Sources ==
* : $\text {4-2}$ Residue Systems: Exercise $2 \ \text {(a)}$
Category:Examples of Residue Systems
Reduced Residue System/Examples/Modulo 18/Square Numbers

== Examples of Reduced Residue Systems ==
The set of integers:
:$\set {1, 25, 49, 121, 169, 289}$
does not form a reduced residue system modulo $18$.
== Proof ==
We have:
Thus we see that:
:$\set {1, 25, 49, 121, 169, 289}$
is equivalent to:
:$\set {1, 7, 13}$
While $\set {1, 7, 13}$ are all coprime to $18$, they do not form a least positive reduced residue system modulo $18$, which is:
:$\set {1, 5, 7, 11, 13, 17}$
from Least Positive Reduced Residue System Modulo 18.
== Sources ==
* : $\text {4-2}$ Residue Systems: Exercise $2 \ \text {(c)}$
Category:Examples of Residue Systems
Reduced Residue System Modulo Prime

== Theorem ==
Let $p$ be a prime number.
The reduced residue system modulo $p$ contains $p - 1$ elements:
:$Z'_p = \set {\eqclass 1 m, \eqclass 2 m, \ldots, \eqclass {p - 1} m}$
and so can be defined as:
:$Z'_p = Z_p \setminus \set {\eqclass 0 m}$
== Proof ==
From Prime not Divisor implies Coprime, each of $1, 2, \ldots, p - 1$ is coprime to $p$.
The result follows by definition of reduced residue system modulo $p$.
== Sources ==
* : $\text {4-2}$ Residue Systems: Example $\text {4-9}$
Category:Reduced Residue Systems
Category:Prime Numbers
Reduced Residue System is Subset of Set of All Residue Classes

== Theorem ==
Let $\Z_m$ be the set of set of residue classes modulo $m$.
Let $\Z'_m$ be the reduced residue system modulo $m$.
Then:
:$\forall m \in \Z_{> 1}: \O \subset \Z'_m \subset \Z_m$
== Proof ==
By definition of reduced residue system modulo $m$:
:$\Z'_m = \set {x \in \Z_m: x \perp m}$
From Subset of Set with Propositional Function:
:$\Z'_m \subseteq \Z_m$
We have that:
:$\gcd \set {m, 0} = m$
Thus it follows that:
:$m > 1 \implies \gcd \set {m, 0} \ne 1$
So:
:$\eqclass 0 m \notin \Z'_m$
However:
:$\eqclass 0 m \in \Z_m$
so:
:$\Z'_m \ne \Z_m$
Thus:
:$\Z'_m \subset \Z_m$
Then:
:$\eqclass 1 m = 1 \implies 1 \perp m$
So:
:$\forall m \in \Z: \eqclass 1 m \in \Z'_m$
Thus:
:$\Z'_m \ne \O$
and therefore:
:$\O \subset \Z'_m$
Category:Residue Classes
Category:Reduced Residue Systems
Reduced Residue System under Multiplication forms Abelian Group

== Theorem ==
Let $\Z_m$ be the set of set of residue classes modulo $m$.
Let $\struct {\Z'_m, \times}$ denote the multiplicative group of reduced residues modulo $m$.
Then $\struct {\Z'_m, \times}$ is an abelian group, precisely equal to the group of units of $\Z_m$.
=== Corollary ===
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Sources ==
* : $\S 3.4$: Cyclic groups
Category:Reduced Residue Systems
Category:Examples of Abelian Groups
Category:Multiplicative Groups of Reduced Residues
Category:Reduced Residue System under Multiplication forms Abelian Group
Reduced Residue System under Multiplication forms Abelian Group/Corollary

== Corollary of Reduced Residue System under Multiplication forms Abelian Group ==
Let $p$ be a prime number.
Let $\Z_p$ be the set of integers modulo $p$.
Let $\struct {\Z'_p, \times}$ denote the multiplicative group of reduced residues modulo $p$.
Then $\struct {\Z'_p, \times}$ is an abelian group.
== Proof ==
Suppose $p \in \Z$ be a prime number.
From the definition of reduced residue system modulo $p$, as $p$ is prime, $\Z'_p$ becomes:
:$\set {\eqclass 1 p, \eqclass 2 p, \ldots, \eqclass {p - 1} p}$
This is precisely $\Z_p \setminus \set {\eqclass 0 p}$ which is what we wanted to show.
The result follows from Reduced Residue System under Multiplication forms Abelian Group.
== Sources ==
* : $\S 1$: Some examples of groups: Example $1.11$
* : Chapter $2$: Examples of Group Structure: $\S 34$
* : $\text{I}$: Groups: $\S 1$: Semigroups, Monoids and Groups
* : $\text{I}$: Groups: $\S 1$: Semigroups, Monoids and Groups: Exercise $7$
* : $\S 34$. Examples of groups: $(3)$
Category:Reduced Residue System under Multiplication forms Abelian Group
Reduced Residue System under Multiplication forms Abelian Group/Proof 1

== Theorem ==
== Proof ==
From Ring of Integers Modulo m is Ring, $\struct {\Z_m, +, \times}$‎ forms a (commutative) ring with unity.
Then we have that the units of a ring with unity form a group.
By Multiplicative Inverse in Ring of Integers Modulo m we have that the elements of $\struct {\Z'_m, \times}$ are precisely those that have inverses, and are therefore the units of $\struct {\Z_m, +, \times}$‎.
The fact that $\struct {\Z'_m, \times}$ is abelian follows from Restriction of Commutative Operation is Commutative.
== Sources ==
* : Chapter $\text {I}$: Elementary Definitions: $\S 1$. Rings and Fields: Example $4$
Category:Reduced Residue System under Multiplication forms Abelian Group
Reduced Residue System under Multiplication forms Abelian Group/Proof 2

== Theorem ==
== Proof ==
Taking the group axioms in turn:
=== ===
From Modulo Multiplication on Reduced Residue System is Closed:
:$\struct {\Z'_m, \times}$ is closed.
=== ===
We have that Modulo Multiplication is Associative.
=== ===
From Modulo Multiplication has Identity, $\eqclass 1 m$ is the identity element of $\struct {\Z'_m, \times_m})$.
=== ===
From Multiplicative Inverse in Monoid of Integers Modulo m, $\eqclass k m \in \Z_m$ has an inverse in $\struct {\Z_m, \times_m}$ $k$ is coprime to $m$.
Thus every element of $\struct {\Z'_m, \times_m}$ has an inverse.
All the group axioms are thus seen to be fulfilled, and so $\struct {\Z'_m, \times_m}$ is a group.
== Sources ==
* : Chapter $\text {I}$: The Group Concept: $\S 6$: Examples of Finite Groups: $\text{(iii)}$: $(1.34)$
* : Chapter $2$: Examples of Group Structure: $\S 34$
* : $\text{I}$: Groups: $\S 1$: Semigroups, Monoids and Groups
Category:Reduced Residue System under Multiplication forms Abelian Group
Reduced Residue System under Multiplication forms Abelian Group/Proof 3

== Theorem ==
== Proof ==
Taking the finite group axioms in turn:
=== $\text {FG} 0$: Closure ===
From Modulo Multiplication on Reduced Residue System is Closed:
:$\struct {\Z'_m, \times}$ is closed.
=== $\text {FG} 1$: Associativity ===
We have that Modulo Multiplication is Associative.
=== $\text {FG} 2$: Finiteness ===
The order of $\struct {\Z'_m, \times}$ is $\map \phi n$ by definition, where $\map \phi n$ denotes the Euler $\phi$ function.
As $\map \phi n < n$ it follows that $\struct {\Z'_m, \times}$ is of finite order.
=== $\text {FG} 3$: Cancellability ===
We have that Modulo Multiplication on Reduced Residue System is Cancellable.
Thus all the finite group axioms are fulfilled, and $\struct {\Z'_m, \times}$ is a group.
It remains to note that Modulo Multiplication is Commutative to confirm that $\struct {\Z'_m, \times}$ is abelian.
== Sources ==
* : Chapter $\text {I}$: The Group Concept: $\S 6$: Examples of Finite Groups: $\text{(iii)}$: Theorem $2$
Category:Reduced Residue System under Multiplication forms Abelian Group
Reduced Residues Modulo 5 under Multiplication form Cyclic Group

== Theorem ==
Let $\struct {\Z'_5, \times_5}$ denote the multiplicative group of reduced residues modulo $5$.
Then $\struct {\Z'_5, \times_5}$ is cyclic.
== Proof ==
From Reduced Residue System under Multiplication forms Abelian Group‎ it is noted that $\struct {\Z'_5, \times_5}$ is a group.
It remains to be shown that $\struct {\Z'_5, \times_5}$ is cyclic.
It will be demonstrated that:
:$\gen {\eqclass 2 5} = \struct {\Z'_5, \times_5}$
That is, that $\eqclass 2 5$ is a generator of $\struct {\Z'_5, \times_5}$.
We note that $\eqclass 1 5$ is the identity element of $\struct {\Z'_5, \times_5}$.
Thus successive powers of $\eqclass 2 5$ are taken, until $n \in \Z$ is found such that $\eqclass 2 5^n = \eqclass 1 5$:
All elements of $\struct {\Z'_5, \times_5}$ are seen to be in $\gen {\eqclass 2 5}$.
Hence the result by definition of cyclic group.
Category:Multiplicative Groups of Reduced Residues
Category:Multiplicative Group of Reduced Residues Modulo 5
Category:Examples of Cyclic Groups
Category:Cyclic Group of Order 4
Reducible Fraction/Examples/4 over 6

== Example of Reducible Fraction ==
The vulgar fraction $\dfrac 4 6$ is an example of a reducible fraction:
:$\dfrac 4 6 = \dfrac {2 \times 2} {2 \times 3} = \dfrac 2 3$
== Sources ==
* 
* 
Category:Examples of Reducible Fractions
Reducible Polynomial/Examples/x^2-1

== Example of Reducible Polynomial ==
The polynomial over $\R$:
:$x^2 - 1$
is reducible, as it can be factorized as follows:
:$x^2 - 1 = \paren {x + 1} \paren {x - 1}$
== Sources ==
* 
* 
Category:Examples of Reducible Polynomials
Reductio ad Absurdum

== Proof Rule ==
Reductio ad Absurdum is a valid argument in certain types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not intuitionistic propositional logic.
=== Proof Rule ===
=== Sequent Form ===
== Explanation ==
== Variants ==
The following forms can be used as variants of this theorem:
=== Variant 1 ===
=== Variant 2 ===
== Also see ==
* Indirect Proof, of which this is an instance
* Definition:Logical Not
* Definition:Contradiction
* Clavius's Law
* Proof by Contradiction, often treated as another aspect of the same thing.
From the point of view of purely classical logic, this is acceptable. However, in the context of intuitionistic logic, it is essential to bear in mind that only the Proof by Contradiction is valid.
This is because Proof by Contradiction starts with a positive assumption $\phi$.
As a result, it does not depend on the Law of Excluded Middle.
== Linguistic Note ==
== Sources ==
* : $\S 1$: Some mathematical language: Axiom systems
* : $\S \text{I}$: The Logic of Statements $(1): \ 14$: A Short Cut to Truth-tables
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic
* 
* 
* : Chapter $1$: Elementary, my dear Watson: $\S 1.1$: You have a logical mind if...
* 
* 
Category:Reductio ad Absurdum
Category:Logical Negation
Category:Rules of Inference
Reductio ad Absurdum/Proof Rule

== Proof Rule ==
Reductio ad Absurdum is a valid argument in certain types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not intuitionistic propositional logic.
As a proof rule it is expressed in the form:
:If, by making an assumption $\neg \phi$, we can infer a contradiction as a consequence, then we may infer $\phi$.
:The conclusion $\phi$ does not depend upon the assumption $\neg \phi$.
It can be written:
:$\ds {\begin{array}{|c|} \hline \neg \phi \\ \vdots \\ \bot \\ \hline \end{array} \over \phi} \textrm{RAA}$
=== Tableau Form ===
== Explanation ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Linguistic Note ==
== Technical Note ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$
* : $\S 1.2.2$: Derived rules
Category:Reductio ad Absurdum
Category:Rules of Inference
Reductio ad Absurdum/Proof Rule/Technical Note

== Technical Note on ==
When invoking in a tableau proof, use the template:
:{{Reductio|line|pool|statement|start|end}}
where:
:line is the number of the line on the tableau proof where the is to be invoked
:pool is the pool of assumptions (comma-separated list)
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:start is the start of the block of the tableau proof upon which this line directly depends
:end is the end of the block of the tableau proof upon which this line directly depends
Category:Technical Notes
Reductio ad Absurdum/Sequent Form

== Proof Rule ==
The Reductio ad Absurdum can be symbolised by the sequent:
:$\paren {\neg p \vdash \bot} \vdash p$
== Proof ==
== Sources ==
* : $\S 1.2.2$: Derived rules
Category:Reductio ad Absurdum
Reductio ad Absurdum/Variant 1/Proof by Truth Table

== Theorem ==
== Proof ==
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|cccc||c|} \hline
\neg & p & \implies & \bot & p \\
\hline
\T & \F & \F & \F & \F \\
\F & \T & \T & \F & \T \\
\hline
\end{array}$
Category:Reductio ad Absurdum
Category:Truth Table Proofs