avewright/proofwiki-math huggingface dataset:
Theorem: Sigmoid Function is Strictly Increasing

The real sigmoid function $\map S x$ is strictly increasing.
{{expand|Add a proof based on the derivative being everywhere positive}}

Proof:
By Cumulative Distribution Function of Logistic Distribution, $S$ is the cumulative distribution function of a logistic distribution, with $\mu = 0$ and $s = 1$.
By Cumulative Distribution Function is Increasing, $S$ is an increasing real function.
{{AimForCont}}, suppose that $S$ is not strictly increasing.
Then there are $a < b$ such that $\map S a = \map S b$.
Thus:
{{begin-eqn}}
{{eqn | l = \map S a
      | r = \map S b
}}
{{eqn | l = \frac 1 {1 + \map \exp {-a} }
      | r = \frac 1 {1 + \map \exp {-b} }
      | c = {{Defof|Sigmoid Function}}
}}
{{eqn | l = 1 + \map \exp {-a}
      | r = 1 + \map \exp {-b}
}}
{{eqn | l = \map \exp {-a}
      | r = \map \exp {-b}
}}
{{eqn | l = -a
      | r = -b
      | c = Exponential is Strictly Increasing and Strictly Monotone Real Function is Bijective
}}
{{eqn | l = a
      | r = b
}}
{{end-eqn}}
which contradicts $a < b$.
Therefore, by Proof by Contradiction, the real sigmoid function is strictly increasing.
{{qed}}
Category:Sigmoid Function
lw7bqqstx0lhogqczrvvvoubhc62qam
Theorem: Range of Sigmoid Function

Let $S$ be the real sigmoid function.
Then the range of $S$ is $\openint 0 1$.

Proof:
By Sigmoid Function is Continuous, $S$ is a continuous real function.
By Image of Real Interval under Continuous Real Function is Real Interval, the range of $S$ is an interval $I$.
By Cumulative Distribution Function of Logistic Distribution, $S$ is the cumulative distribution function of a logistic distribution, with $\mu = 0$ and $s = 1$.
By Bounds for Cumulative Distribution Function:
:$0 \le \map S x \le 1$
for every $x \in \R$.
Therefore, $I \subseteq \closedint 0 1$.
{{AimForCont}}, suppose the left hand endpoint of $I$ is $a > 0$.
By Limit of Cumulative Distribution Function at Negative Infinity, there is some $x^- \in \R$ such that:
:$\size {\map S {x^-} - 0} < a$
Therefore, $\map S {x^-} < a$, contradicting that $a$ is the left hand endpoint.
Hence, by Proof by Contradiction, $a = 0$.
Likewise, Limit of Cumulative Distribution Function at Positive Infinity proves that the right hand endpoint is $1$.
Therefore, $I \supseteq \openint 0 1$.
{{AimForCont}}, suppose $0 \in I$.
Then, $\map S {x_0} = 0$, for some $x_0 \in \R$.
But as Sigmoid Function is Strictly Increasing, every $x < x_0$ must have $\map S x < 0$, contradicting $0 \le \map S x$ above.
Thus, by Proof by Contradiction, $0 \notin I$.
By the same argument, $1 \notin I$.
Therefore, $I = \openint 0 1$.
{{qed}}
Category:Sigmoid Function
f8l13cfgc7jkaj1xdf1931voie2k70k
Theorem: Inequality of Natural Numbers is Provable

Let $x, y \in \N$ be natural numbers.
Suppose $x \ne y$.
Let $\sqbrk a$ denote the unary representation of $a \in \N$.
Then $\sqbrk x \ne \sqbrk y$ is a theorem of minimal arithmetic.

Proof:
=== Lemma ===
{{:Inequality of Natural Numbers is Provable/Lemma}}{{qed|lemma}}
As $x \ne y$, by Ordering on Natural Numbers is Trichotomy, either $x < y$ or $y < x$.
If $y < x$, the result follows from the lemma.
{{qed|lemma}}
If $x < y$, then:
:$\sqbrk y \ne \sqbrk x$
is a theorem by the lemma.
Hence, the following formal proof:
:By Rule of Assumption, suppose $\sqbrk x = \sqbrk y$
:By Equality is Symmetric, $\sqbrk y = \sqbrk x$
:By Principle of Non-Contradiction, this contradicts $\sqbrk y \ne \sqbrk x$
:By Proof by Contradiction, $\sqbrk x \ne \sqbrk y$
demonstrates the result.
{{qed|lemma}}
The overall result follows from Proof by Cases.
{{qed}}
Category:Inequality of Natural Numbers is Provable
Category:Natural Numbers
Category:Proofs by Induction
5d7owyr5fjy44vchqvfl757vz0j1ppo
Theorem: Sine Integral Function is Bounded

Let $\Si: \R \to \R$ denote the sine integral function.
Then $\Si$ is bounded.

Proof:
By Limit at Infinity of Sine Integral Function and its corollary:
{{begin-eqn}}
{{eqn | l = \lim _{x \mathop \to +\infty} \size {\map \Si x}
      | r = \lim _{x \mathop \to -\infty} \size {\map \Si x}
}}
{{eqn | r = \dfrac \pi 2
}}
{{end-eqn}}
Thus there is a $M > 0$ such that for all $x \in \R$:
:$\size x > M \implies \size {\map \Si x} \le \dfrac \pi 2 + 1$
On the other hand, if $\size x \le M$, then:
{{begin-eqn}}
{{eqn | l = \size {\map \Si x}
      | r = \size {\int_0 ^x \dfrac {\sin t} t \rd t }
}}
{{eqn | o = \le
      | r = \int _0 ^{\size x} \size { \dfrac {\sin t} t} \rd t
}}
{{eqn | o = \le
      | r = \int _0 ^{\size x} 1 \rd t
}}
{{eqn | r = \size x
}}
{{eqn | o = \le
      | r = M
}}
{{end-eqn}}
Thus:
:$\forall x \in \R : \size {\map \Si x} \le \max \set {\dfrac \pi 2 + 1 , M}$
{{finish|more details}}
Category:Sine Integral Function
bm5pki5ay1uelve7b2wz2i15aqw8iib
Theorem: Negation of Ordering of Natural Numbers is Provable

Let $x, y \in \N$ be natural numbers.
Suppose $x \ge y$.
Let $\sqbrk a$ denote the unary representation of $a \in \N$.
Then:
:$\neg \paren {\sqbrk x < \sqbrk y}$
is a theorem of minimal arithmetic.

Proof:
Fix $x \in \N$.
Proceed by induction on $y$.
Theorem: Lévy's Inversion Formula/Integrable Characteristic Function

Let $X$ be a real-valued random variable.
Let $P_X$ be the probability distribution of $X$.
Let $\phi : \R \to \C$ be the characteristic function of $X$.
Suppose that $\phi$ is Lebesgue integrable, i.e.:
:$\ds \int _\R \cmod {\map \phi t} \rd t < + \infty$
Then $P_X$ is absolutely continuous {{WRT}} the Lebesgue measure.
Moreover, the Radon-Nikodym derivative is given by:
:$\ds \map g x := \dfrac 1 {2 \pi} \int_\R \map \phi t e^{- i t x} \rd t$

Proof:
Let $a < b$ be such that:
:$\map {P_X} {\set {a,b} } = 0$
Then:
{{begin-eqn}}
{{eqn | l = \int_a^b \map g x \rd x
      | r = \dfrac 1 {2 \pi} \int_a^b \paren {\int_\R \map \phi t e^{- i t x} \rd t} \rd x
}}
{{eqn | r = \dfrac 1 {2 \pi} \int_\R \map \phi t \paren {\int_a^b e^{- i t x} \rd x} \rd t
      | c = Fubini's Theorem
}}
{{eqn | r = \dfrac 1 {2 \pi} \int_\R \map \phi t \frac {e^{- i t a} - e^{- i t b} }{i t} \rd t
}}
{{end-eqn}}
Now:
:$\ds \forall t \in \R : \quad \cmod {\map \phi t \frac {e^{- i t a} - e^{- i t b} }{i t} } \le \cmod {\map \phi t} \paren {b - a}$
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {2 \pi} \int_\R \map \phi t \frac {e^{- i t a} - e^{- i t b} }{i t} \rd t
      | r = \lim_{T \mathop \to \infty} \dfrac 1 {2 \pi} \int_{-T}^T \map \phi t \frac {e^{- i t a} - e^{- i t b} }{i t} \rd t
      | c = Lebesgue's Dominated Convergence Theorem
}}
{{eqn | r = \map {P_X} {\hointl a b}
      | c = Lévy's Inversion Formula
}}
{{end-eqn}}
{{ProofWanted|Finish for all $a < b$}}
{{Namedfor|Paul Pierre Lévy|cat = Lévy}}
Category:Lévy's Inversion Formula
gea66lslhmao2vjt6ww58kn0arjxwdq
Theorem: Characterization of Paracompactness in T3 Space/Lemma 6

:$\VV^*$ is an open locally finite cover of $T$

Proof:
==== Lemma 4 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 4}}{{qed|lemma}}
Theorem: Quantifier-Free Formula of Arithmetic is Provable

Let $\phi$ be a sentence in the language of arithmetic.
Suppose $\phi$ contains no quantifiers.
Suppose also that $\N \models \phi$.
:That is, the natural numbers model $\phi$.
Then $\phi$ is a theorem of minimal arithmetic.

Proof:
By Existence of Negation Normal Form of Statement, $\phi$ is logically equivalent to a WFF $\psi$ such that:
:The only logical connectives are $\set {\neg, \land, \lor}$.
:The connective $\neg$ only appears in front of a predicate symbol.
Proceed by induction on the structure of WFFs in the language of arithmetic.
Theorem: Quantifier-Free Formula of Arithmetic is Provable/Corollary

Let $\phi$ be a sentence in the language of arithmetic.
Suppose $\phi$ contains no quantifiers.
Then exactly one of:
:$\phi$
:$\neg \phi$
is a theorem of minimal arithmetic.

Proof:
By Law of Excluded Middle, either $\N \models \phi$, or $\N \models \neg \phi$.
By Quantifier-Free Formula of Arithmetic is Provable, whichever one holds is a theorem of minimal arithmetic.
{{qed|lemma}}
Now, suppose that $\N \models \phi$.
Then, $\N \not\models \phi$ by definition of value of formula.
Thus, by the definition of sound proof system, $\neg \phi$ is not a theorem.
Therefore, $\phi$ and $\neg \phi$ cannot both be theorems.
{{qed}}
6l0m817qcfrsjkp79fknsx58ftigd7h
Theorem: Characteristic Function of Random Variable is Well-Defined

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ be a real-valued random variable on $\struct {\Omega, \Sigma, \Pr}$.
The characteristic function $\phi: \R \to \C$ of $X$ is well-defined.

Proof:
Let $t \in \R$.
Recall:
{{begin-eqn}}
{{eqn | l = \map \phi t
      | r = \expect {e^{i t X} }
      | c = {{Defof|Characteristic Function of Random Variable|Characteristic Function}}
}}
{{eqn | r = \int e^{i t X} \rd \Pr
      | c = {{Defof|Expectation/General Definition|Expectation}}
}}
{{end-eqn}}
Thus we need to show that the last integral exists.
By Modulus of Exponential of Imaginary Number is One:
:$\cmod {e^{i t X } } = 1$
since $t \map X \omega \in \R$ for all $\omega \in \Omega$.
In particular:
:$\ds \int \cmod {e^{i t X} } \rd \Pr = \int 1 \rd \Pr = 1$
{{explain|No seriously, I mean that, a link to the definition of $\d \Pr$ which is understandable in the context of the general measure $\mu$, which in itself is not a trivial concept to grab, so at least thrown a bone to the poor reader of the page, yeah?<br/>I gave it above as {{Defof|Expectation/General Definition|Expectation}}. Or feel free to rename $\Pr$ to $\mu$, if it is somehow helpful.}}
Thus, in view of Characterization of Integrable Functions:
:$\ds \int e^{i t X} \rd \Pr$
exists.
{{qed}}
Category:Probability Theory
7m3m4j8azfche8o7esyfcskpl3ef7xa
Theorem: Existential Quantification of Provable Arithmetic Formula is Provable

Let $\map \phi x$ be a WFF in the language of arithmetic with $1$ free variable.
Let $\sqbrk a$ denote the unary representation of $a$.
Suppose that, for every $n \in \N$ such that $\N \models \map \phi {x \gets \sqbrk n}$:
:$\map \phi {x \gets \sqbrk n}$
is a theorem of minimal arithmetic.
Suppose also that:
:$\N \models \exists x: \map \phi x$
Then:
:$\exists x: \map \phi x$
is a theorem of minimal arithmetic.

Proof:
By definition of value of formula:
:$\exists x \in \N: \map \phi x$
Choose $x_0 \in \N$ that satisfies $\map \phi {x \gets x_0}$.
By Unary Representation of Natural Number:
:$x_0 = \sqbrk {x_0}$
Thus, by Substitution Property of Equality:
:$\map \phi {x \gets \sqbrk {x_0} }$
But then, by hypothesis:
:$\map \phi {x \gets \sqbrk {x_0} }$
is a theorem of minimal arithmetic.
The result follows from Existential Generalisation.
{{qed}}
Category:Natural Numbers
Category:Proof Theory
mq94t3noi0k5jore3o6rvau6rvn4gyd
Theorem: Bounded Universal Quantification of Provable Arithmetic Formula is Provable

Let $\map \phi x$ be a WFF in the language of arithmetic with $1$ free variable.
Let $\tau$ be a term in the language of arithmetic with no variables.
Let $\sqbrk a$ denote the unary representation of $a$.
Suppose that, for every $n \in \N$ such that $\N \models \map \phi {x \gets \sqbrk n}$:
:$\map \phi {x \gets \sqbrk n}$
is a theorem of minimal arithmetic.
Suppose also that:
:$\N \models \forall x < \tau: \map \phi x$
Then:
:$\forall x < \tau: \map \phi x$
is a theorem of minimal arithmetic.

Proof:
Let $t = \map {\operatorname{val}_\N} \tau$ be the value of $\tau$ under the natural numbers.
By definition of value of formula:
:$\N \models \map \phi {x \gets x_0}$
for every $x_0 < t$.
Therefore, {{hypothesis}}:
:$\map \phi {x \gets \sqbrk {x_0} }$
is a theorem, for every $x_0 < t$.
Additionally, by Lower Section of Natural Number is Provable:
:$\forall x: x = 0 \lor x = \map s 0 \lor \dotso \lor x = \sqbrk {t - 1} \lor \neg {x < \sqbrk t}$
is a theorem.
The result follows from False Statement implies Every Statement and Proof by Cases.
{{qed}}
Category:Natural Numbers
Category:Proof Theory
33v7rue85z63vj0n6uw1qjg8l7a391e
Theorem: Characterization of Paracompactness in T3 Space/Statement 3 implies Statement 1

Let $T = \struct{X, \tau}$ be a topological space.
If every open cover of $T$ have a closed locally finite refinement then:
:$T$ is paracompact.

Proof:
Let every open cover of $T$ have a closed locally finite refinement.
Let $\UU$ be an open cover of $T$.
Let $\VV$ be a closed locally finite refinement of $\UU$, which exists by assumption.
Let $\WW = \set{W \in \tau : \set{V \in \VV : V \cap W \ne \O} \text{ is finite}}$.
By definition of locally finite:
:$\forall x \in X: \exists W \in \tau: x \in W$ and $\set{V \in \VV : V \cap W \ne \O}$ is finite. 
Hence $\WW$ is an open cover of $T$, by definition.
Let $\AA$ be a closed locally finite refinement of $\WW$, which exists by assumption.
==== Lemma 4 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 4}}{{qed|lemma}}
For each $V \in \VV$, let:
:$V^* = X \setminus \ds \bigcup \set{A \in \AA : A \cap V = \O}$
==== Lemma 5 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 5}}{{qed|lemma}}
Let $\VV^* = \set{V^* : V \in \VV}$.
==== Lemma 6 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 6}}{{qed|lemma}}
From {{Lemma|Characterization of Paracompactness in T3 Space|5}} and {{Lemma|Characterization of Paracompactness in T3 Space|6}} it follows that $\VV$ is a refinement of $\VV^*$ by definition.
By definition of refinement:
:$\forall V \in \VV : \exists U \in \UU : V \subseteq U$
For each $V \in \VV$, let:
:$U_V \in \UU : V \subseteq U_V$
Let:
:$\UU^* = \set{V^* \cap U_V : V \in \VV}$
==== Lemma 7 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 7}}{{qed|lemma}}
Since $\UU$ was arbitrary, it follows that $T$ is paracompact by definition.
Theorem: Minimal Arithmetic is Sigma 1 Complete

Let $\phi$ be a $\Sigma_1$ sentence in the language of arithmetic.
Suppose $\N \models \phi$.
Then $\phi$ is a theorem in minimal arithmetic.

Proof:
By definition of $\Sigma_1$, $\phi$ is logically equivalent to:
:$Q_1 Q_2 \dotsm Q_k \map \psi {x_1, x_2, \dotsc, x_k}$
where $\psi$ is a WFF with no quantifiers.
Proceed by induction on the number of quantifiers in the formula.
Theorem: Multiples of Factorial Plus One are Coprime

Let $a \in \N$ be a natural number.
Let $\sequence {x_1, x_2, \dotsc, x_n}$ be a sequence of natural numbers such that:
:$\forall i: 1 \le i \le n: x_i = 1 + i \times a!$
where $a!$ denotes the factorial of $a$.
Let $a \ge n - 1$.
Then $\set {x_i}$ are pairwise coprime.

Proof:
Let $p$ be a prime number.
Suppose that $p \divides x_i$.
Then, by definition of $x_i$:
:$p \divides 1 + i \times a!$
Thus, by Consecutive Integers are Coprime:
:$p \nmid i \times a!$
Therefore:
:$p \nmid a!$
{{AimForCont}} $p \divides x_j$, where $j \ne i$.
Then $p \divides 1 + j \times a!$.
By Common Divisor Divides Difference:
:$p \divides \paren {i - j} \times a!$
By Euclid's Lemma, along with $p \nmid a!$ above:
:$p \divides i - j$
But as $0 < \size {i - j} < n$:
:$p \divides \paren {n - 1}!$
Additionally, since $a \ge n - 1$:
:$\paren {n - 1}! \divides a!$
By Divisor Relation is Transitive:
:$p \divides a!$
However, $p \nmid a!$ from above, a contradiction.
Thus, by Proof by Contradiction, there is no such $x_j$.
Hence the result.
{{qed}}
Category:Coprime Integers
Category:Factorials
hjbea2e4ps573am3jctnsvwcvjrbujq
Theorem: Existential Quantifier Distributes over Conjunction

Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.
Then:
:$\exists x: \paren {\map \phi x \land \map \psi x} \vdash \paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}$

Proof:
{{BeginTableau|\exists x: \paren {\map \phi x \land \map \psi x} \vdash \paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x} }}
{{TableauLine|n = 1
             |pool = 1
             |f = \exists x: \paren {\map \phi x \land \map \psi x}
             |rlnk = Rule of Assumption
             |rtxt = Premise
}}
{{TableauLine|n = 2
             |pool = 2
             |f = \map \phi {x \gets x_0} \land \map \psi {x \gets x_0}
             |rlnk = Rule of Assumption
             |rtxt = Assumption
             |c = $x_0$ is arbitrary
}}
{{TableauLine|n = 3
             |pool = 2
             |f = \map \phi {x \gets x_0}
             |rlnk = Rule of Simplification
             |rtxt = Rule of Simplification
             |dep = 2
}}
{{TableauLine|n = 4
             |pool = 2
             |f = \exists x: \map \phi x
             |rlnk = Existential Generalisation
             |rtxt = Existential Generalisation
             |dep = 3
}}
{{TableauLine|n = 5
             |pool = 2
             |f = \map \psi {x \gets x_0}
             |rlnk = Rule of Simplification
             |rtxt = Rule of Simplification
             |dep = 2
}}
{{TableauLine|n = 6
             |pool = 2
             |f = \exists x: \map \psi x
             |rlnk = Existential Generalisation
             |rtxt = Existential Generalisation
             |dep = 5
}}
{{TableauLine|n = 7
             |pool = 2
             |f = \paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}
             |rlnk = Rule of Conjunction
             |rtxt = Rule of Conjunction
             |dep = 4, 6
}}
{{TableauLine|n = 8
             |pool = 1
             |f = \paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}
             |rlnk = Existential Instantiation
             |rtxt = Existential Instantiation
             |dep = 1, 2-7
}}
{{EndTableau|qed}}
Category:Existential Quantifier
fj8sz0ltet5wrlor90cfx6opil014r4
Theorem: Universal Quantifier Distributes over Conjunction

Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.
Then:
:$\forall x: \paren {\map \phi x \land \map \psi x} \dashv \vdash \paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}$

Proof:
=== Forward Implication ===
{{BeginTableau|\forall x: \paren {\map \phi x \land \map \psi x} \vdash \paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x} }}
{{TableauLine|n = 1
             |pool = 1
             |f = \forall x: \paren {\map \phi x \land \map \psi x}
             |rlnk = Rule of Assumption
             |rtxt = Premise
}}
{{TableauLine|n = 2
             |pool = 1
             |f = \map \phi {x \gets x_0} \land \map \psi {x \gets x_0}
             |rlnk = Universal Instantiation
             |rtxt = Universal Instantiation
             |dep = 1
}}
{{TableauLine|n = 3
             |pool = 1
             |f = \map \phi {x \gets x_0}
             |rlnk = Rule of Simplification
             |rtxt = Rule of Simplification
             |dep = 2
}}
{{TableauLine|n = 4
             |pool = 1
             |f = \forall x: \map \phi x
             |rlnk = Universal Generalisation
             |rtxt = Universal Generalisation
             |dep = 3
}}
{{TableauLine|n = 5
             |pool = 1
             |f = \map \psi {x \gets x_0}
             |rlnk = Rule of Simplification
             |rtxt = Rule of Simplification
             |dep = 2
}}
{{TableauLine|n = 6
             |pool = 1
             |f = \forall x: \map \psi x
             |rlnk = Universal Generalisation
             |rtxt = Universal Generalisation
             |dep = 5
}}
{{TableauLine|n = 7
             |pool = 1
             |f = \paren {\forall x: \map \phi x} \land \paren {\forall x: \map \psi x}
             |rlnk = Rule of Conjunction
             |rtxt = Rule of Conjunction
             |dep = 4, 6
}}
{{EndTableau}}{{qed|lemma}}
Theorem: Existential Quantifier Distributes over Disjunction

Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.
Then:
:$\exists x: \paren {\map \phi x \lor \map \psi x} \dashv \vdash \paren {\exists x: \map \phi x} \lor \paren {\exists x: \map \psi x}$

Proof:
=== Forward Implication ===
{{BeginTableau|\exists x: \paren {\map \phi x \lor \map \psi x} \vdash \paren {\exists x: \map \phi x} \lor \paren {\exists x: \map \psi x} }}
{{TableauLine|n = 1
             |pool = 1
             |f = \exists x: \paren {\map \phi x \lor \map \psi x}
             |rlnk = Rule of Assumption
             |rtxt = Premise
}}
{{TableauLine|n = 2
             |pool = 2
             |f = \map \phi {x \gets x_0} \lor \map \psi {x \gets x_0}
             |rlnk = Rule of Assumption
             |rtxt = Assumption
}}
{{TableauLine|n = 3
             |pool = 3
             |f = \map \phi {x \gets x_0}
             |rlnk = Rule of Assumption
             |rtxt = Assumption
}}
{{TableauLine|n = 4
             |pool = 3
             |f = \exists x: \map \phi x
             |rlnk = Existential Generalisation
             |rtxt = Existential Generalisation
             |dep = 3
}}
{{TableauLine|n = 5
             |pool = 3
             |f = \paren {\exists x: \map \phi x} \lor \paren {\exists x: \map \psi x}
             |rlnk = Rule of Addition
             |rtxt = Rule of Addition
             |dep = 4
}}
{{TableauLine|n = 6
             |pool = 6
             |f = \map \psi {x \gets x_0}
             |rlnk = Rule of Assumption
             |rtxt = Assumption
}}
{{TableauLine|n = 7
             |pool = 6
             |f = \exists x: \map \psi x
             |rlnk = Existential Generalisation
             |rtxt = Existential Generalisation
             |dep = 6
}}
{{TableauLine|n = 8
             |pool = 6
             |f = \paren {\exists x: \map \phi x} \lor \paren {\exists x: \map \psi x}
             |rlnk = Rule of Addition
             |rtxt = Rule of Addition
             |dep = 7
}}
{{TableauLine|n = 9
             |pool = 2
             |f = \paren {\exists x: \map \phi x} \lor \paren {\exists x: \map \psi x}
             |rlnk = Proof by Cases
             |rtxt = Proof by Cases
             |dep = 2, 3-5, 6-8
}}
{{TableauLine|n = 10
             |pool = 1
             |f = \paren {\exists x: \map \phi x} \lor \paren {\exists x: \map \psi x}
             |rlnk = Existential Instantiation
             |rtxt = Existential Instantiation
             |dep = 1, 2-9
}}
{{EndTableau|lemma}}
Theorem: Universal Quantifier Distributes over Disjunction

Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.
Then:
:$\paren {\forall x: \map \phi x} \lor \paren {\forall x: \map \psi x} \vdash \forall x: \paren {\map \phi x \lor \map \psi x}$

Proof:
{{BeginTableau | \paren {\forall x: \map \phi x} \lor \paren {\forall x: \map \psi x} \vdash \forall x: \paren {\map \phi x \lor \map \psi x}
}}
{{TableauLine | n = 1
              | pool = 1
              | f = \paren {\forall x: \map \phi x} \lor \paren {\forall x: \map \psi x}
              | rlnk = Rule of Assumption
              | rtxt = Premise
}}
{{TableauLine | n = 2
              | pool = 2
              | f = \forall x: \map \phi x
              | rlnk = Rule of Assumption
              | rtxt = Assumption
}}
{{TableauLine | n = 3
              | pool = 2
              | f = \map \phi {x \gets x_0}
              | rlnk = Universal Instantiation
              | rtxt = Universal Instantiation
              | dep = 2
}}
{{TableauLine | n = 4
              | pool = 2
              | f = \map \phi {x \gets x_0} \lor \map \psi {x \gets x_0}
              | rlnk = Rule of Addition
              | rtxt = Rule of Addition
              | dep = 3
}}
{{TableauLine | n = 5
              | pool = 5
              | f = \forall x: \map \psi x
              | rlnk = Rule of Assumption
              | rtxt = Assumption
}}
{{TableauLine | n = 6
              | pool = 5
              | f = \map \psi {x \gets x_0}
              | rlnk = Universal Instantiation
              | rtxt = Universal Instantiation
              | dep = 5
}}
{{TableauLine | n = 7
              | pool = 5
              | f = \map \phi {x \gets x_0} \lor \map \psi {x \gets x_0}
              | rlnk = Rule of Addition
              | rtxt = Rule of Addition
              | dep = 6
}}
{{TableauLine | n = 8
              | pool = 1
              | f = \map \phi {x \gets x_0} \lor \map \psi {x \gets x_0}
              | rlnk = Proof by Cases
              | rtxt = Proof by Cases
              | dep = 1, 2-4, 5-7
}}
{{TableauLine | n = 9
              | pool = 1
              | f = \forall x: \paren {\map \phi x \lor \map \psi x}
              | rlnk = Universal Generalisation
              | rtxt = Universal Generalisation
              | dep = 8
}}
{{EndTableau|qed}}
Category:Universal Quantifier
2xymy5ef4yf2k7dskp3zjrrq3clx9gr