avewright/proofwiki-math huggingface dataset:
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive/Formulation 1

:$\paren {q \lor r} \land p \dashv \vdash \paren {q \land p} \lor \paren {r \land p}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc||ccccccc|} \hline
(q & \lor & r) & \land & p & (q & \land & p) & \lor & (r & \land & p) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F & \F & \T & \F & \F & \F & \T \\
\F & \T & \T & \F & \F & \F & \F & \F & \F & \T & \F & \F \\
\F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T & \T \\
\T & \T & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \T & \T & \F & \F & \T \\
\T & \T & \T & \F & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive/Formulation 2

:$\vdash \paren {\paren {q \lor r} \land p} \iff \paren {\paren {q \land p} \lor \paren {r \land p} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {q \lor r} \land p} \iff \paren {\paren {q \land p} \lor \paren {r \land p} } }}
{{Assumption|1|\paren {q \lor r} \land p}}
{{SequentIntro|2|1|\paren {q \land p} \lor \paren {r \land p}|1|Conjunction is Right Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {\paren {q \lor r} \land p} \implies \paren {\paren {q \land p} \lor \paren {r \land p} }|1|2}}
{{Assumption|4|\paren {q \land p} \lor \paren {r \land p} }}
{{SequentIntro|5|4|\paren {q \lor r} \land p|4|Conjunction is Right Distributive over Disjunction: Formulation 1}}
{{Implication|6||\paren {\paren {q \land p} \lor \paren {r \land p} } \implies \paren {\paren {q \lor r} \land p}|4|5}}
{{BiconditionalIntro|7||\paren {\paren {q \lor r} \land p} \iff \paren {\paren {q \land p} \lor \paren {r \land p} }|3|6}}
{{EndTableau}}
{{qed}
Category:Rule of Distribution
is2g3m0dxduotdabjgasc2fnjc5jfo9
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
p & \lor & (q & \land & r) & (p & \lor & q) & \land & (p & \lor & r) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \F & \F & \T & \T & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \F & \F & \T & \T & \F & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \F & \T & \T & \T & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} } }}
{{Assumption|1|p \lor \paren {q \land r} }}
{{SequentIntro|2|1|\paren {p \lor q} \land \paren {p \lor r}|1|Disjunction is Left Distributive over Conjunction: Formulation 1}}
{{Implication|3||\paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor q} \land \paren {p \lor r} }|1|2}}
{{Assumption|4|\paren {p \lor q} \land \paren {p \lor r} }}
{{SequentIntro|5|4|p \lor \paren {q \land r}|4|Disjunction is Left Distributive over Conjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \lor q} \land \paren {p \lor r} } \implies \paren {p \lor \paren {q \land r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|} \hline
p & \lor & (q & \land & r) & \iff & (p & \lor & q) & \land & (p & \lor & r) \\
\hline
\F & \F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \T & \F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \F & \T & \F & \T & \T & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \F & \F & \T & \T & \T & \F & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \F & \T & \T & \T & \T & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive/Formulation 2}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
(q & \land & r) & \lor & p & (q & \lor & p) & \land & (r & \lor & p) \\
\hline
F & F & F & F & F & F & F & F & F & F & F & F \\
F & F & F & T & T & F & T & T & T & F & T & T \\
F & F & T & F & F & F & F & F & F & T & T & F \\
F & F & T & T & T & F & T & T & T & T & T & T \\
T & F & F & F & F & T & T & F & F & F & F & F \\
T & F & F & T & T & T & T & T & T & F & T & T \\
T & T & T & T & F & T & T & F & T & T & T & F \\
T & T & T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 1/Forward Implication

:$p \lor \paren {q \land r} \vdash \paren {p \lor q} \land \paren {p \lor r}$

Proof:
{{BeginTableau|p \lor \paren {q \land r} \vdash \paren {p \lor q} \land \paren {p \lor r} }}
{{Premise        | 1|p \lor \paren {q \land r} }}
{{Assumption     | 2|p}}
{{Addition       | 3|2|p \lor q|2|1}}
{{Addition       | 4|2|p \lor r|2|1}}
{{Conjunction    | 5|2|\paren {p \lor q} \land \paren {p \lor r}|3|4}}
{{Assumption     | 6|q \land r}}
{{Simplification | 7|6|q|6|1}}
{{Simplification | 8|6|r|6|2}}
{{Addition       | 9|6|p \lor q|7|2}}
{{Addition       |10|6|p \lor r|8|2}}
{{Conjunction    |11|6|\paren {p \lor q} \land \paren {p \lor r}|7|8}}
{{ProofByCases   |12|1|\paren {p \lor q} \land \paren {p \lor r}|1|2|5|6|11}}
{{EndTableau}}
{{qed}}
Category:Rule of Distribution
i25mmyxvwb862jvl4ipx120n568xzpk
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2

:$\vdash \paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} }$

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} } }}
{{Assumption|1|p \lor \paren {q \land r} }}
{{SequentIntro|2|1|\paren {p \lor q} \land \paren {p \lor r}|1|Disjunction is Left Distributive over Conjunction: Formulation 1}}
{{Implication|3||\paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor q} \land \paren {p \lor r} }|1|2}}
{{Assumption|4|\paren {p \lor q} \land \paren {p \lor r} }}
{{SequentIntro|5|4|p \lor \paren {q \land r}|4|Disjunction is Left Distributive over Conjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \lor q} \land \paren {p \lor r} } \implies \paren {p \lor \paren {q \land r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2

:$\vdash \paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} }$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|} \hline
p & \lor & (q & \land & r) & \iff & (p & \lor & q) & \land & (p & \lor & r) \\
\hline
\F & \F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \T & \F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \F & \T & \F & \T & \T & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \F & \F & \T & \T & \T & \F & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \F & \T & \T & \T & \T & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive/Formulation 1

:$\paren {q \land r} \lor p \dashv \vdash \paren {q \lor p} \land \paren {r \lor p}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
(q & \land & r) & \lor & p & (q & \lor & p) & \land & (r & \lor & p) \\
\hline
F & F & F & F & F & F & F & F & F & F & F & F \\
F & F & F & T & T & F & T & T & T & F & T & T \\
F & F & T & F & F & F & F & F & F & T & T & F \\
F & F & T & T & T & F & T & T & T & T & T & T \\
T & F & F & F & F & T & T & F & F & F & F & F \\
T & F & F & T & T & T & T & T & T & F & T & T \\
T & T & T & T & F & T & T & F & T & T & T & F \\
T & T & T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive/Formulation 2

:$\vdash \paren {\paren {q \land r} \lor p} \iff \paren {\paren {q \lor p} \land \paren {r \lor p} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {q \land r} \lor p} \iff \paren {\paren {q \lor p} \land \paren {r \lor p} } }}
{{Assumption|1|\paren {q \land r} \lor p}}
{{SequentIntro|2|1|\paren {q \lor p} \land \paren {r \lor p}|1|Conjunction is Right Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {\paren {q \land r} \lor p} \implies \paren {\paren {q \lor p} \land \paren {r \lor p} }|1|2}}
{{Assumption|4|\paren {q \lor p} \land \paren {r \lor p} }}
{{SequentIntro|5|4|\paren {q \land r} \lor p|4|Conjunction is Right Distributive over Disjunction: Formulation 1}}
{{Implication|6||\paren {\paren {q \lor p} \land \paren {r \lor p} } \implies \paren {\paren {q \land r} \lor p}|4|5}}
{{BiconditionalIntro|7||\paren {\paren {q \land r} \lor p} \iff \paren {\paren {q \lor p} \land \paren {r \lor p} }|3|6}}
{{EndTableau|qed}}
Category:Rule of Distribution
7z7uuzjoo8r26oav447crim4y4t7oxm
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive/Formulation 1/Proof

:$\left({q \land r}\right) \lor p \dashv \vdash \left({q \lor p}\right) \land \left({r \lor p}\right)$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
(q & \land & r) & \lor & p & (q & \lor & p) & \land & (r & \lor & p) \\
\hline
F & F & F & F & F & F & F & F & F & F & F & F \\
F & F & F & T & T & F & T & T & T & F & T & T \\
F & F & T & F & F & F & F & F & F & T & T & F \\
F & F & T & T & T & F & T & T & T & T & T & T \\
T & F & F & F & F & T & T & F & F & F & F & F \\
T & F & F & T & T & T & T & T & T & F & T & T \\
T & T & T & T & F & T & T & F & T & T & T & F \\
T & T & T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Union of Subsets is Subset/Set of Sets

Let $T$ be a set.
Let $\mathbb S$ be a set of sets.
Suppose that for each $S \in \mathbb S$, $S \subseteq T$.
Then:
:$\ds \bigcup \mathbb S \subseteq T$

Proof:
Let $x \in \ds \bigcup \mathbb S$.
By the definition of union, there exists an $S \in \mathbb S$ such that $x \in S$.
By premise, $S \subseteq T$.
By the definition of subset, $x \in T$.
Since this result holds for each $x \in \ds \bigcup \mathbb S$:
:$\ds \bigcup \mathbb S \subseteq T$
{{qed}}
Category:Union of Subsets is Subset
epzeghl0l5u1bxl4pdjrq7gj0c1a0jt
Theorem: Union is Smallest Superset/Set of Sets

Let $T$ be a set.
Let $\mathbb S$ be a set of sets.
Then:
:$\paren {\forall X \in \mathbb S: X \subseteq T} \iff \bigcup \mathbb S \subseteq T$

Proof:
By Union of Subsets is Subset: Set of Sets:
:$\paren {\forall X \in \mathbb S: X \subseteq T} \implies \bigcup \mathbb S \subseteq T$
{{qed|lemma}}
For the converse implication, suppose that $\bigcup \mathbb S \subseteq T$.
Consider any $X \in \mathbb S$ and take any $x \in X$.
From Set is Subset of Union: Set of Sets we have that $X \subseteq \bigcup \mathbb S$.
Thus $x \in \bigcup \mathbb S$.
But $\bigcup \mathbb S \subseteq T$.
So it follows that $X \subseteq T$.
So:
:$\bigcup \mathbb S \subseteq T \implies \paren {\forall X \in \mathbb S: X \subseteq T}$
{{qed|lemma}}
Hence:
:$\paren {\forall X \in \mathbb S: X \subseteq T} \iff \bigcup \mathbb S \subseteq T$
{{Qed}}
Theorem: Intersection of Relations is Relation

Let $S$ and $T$ be sets.
Let $\FF$ be a family of relations from $S$ to $T$.
Let $\ds \RR = \bigcap \FF$, the intersection of all the elements of $\FF$.
Then $\RR$ is a relation from $S$ to $T$.
{{Expand|Binary case}}

Proof:
By the definition of a relation from $S$ to $T$, each element of $\FF$ is a subset of $S \times T$.
By Intersection of Subsets is Subset: Set of Sets:
:$\RR \subseteq S \times T$
Therefore, by the definition of a relation from $S$ to $T$, $\RR$ is a relation from $S$ to $T$.
{{qed}}
Category:Relation Theory
fgpu3jpko1f2tytpylqjet8xv04o2yz
Theorem: Intersection of Subsets is Subset/Set of Sets

Let $T$ be a set.
Let $\mathbb S$ be a non-empty set of sets.
Suppose that for each $S \in \mathbb S$:
:$S \subseteq T$
Then:
:$\bigcap \mathbb S \subseteq T$

Proof:
Let $x \in \bigcap \mathbb S$.
Then by the definition of intersection:
:$\forall S \in \mathbb S: x \in S$.
Since $\mathbb S$ is non-empty by the premise, it has some element $S$.
Then $x \in S$.
Since $S \in \mathbb S$, the premise shows that $S \subseteq T$.
By the definition of subset, $x \in T$.
Since this holds for each $x \in \bigcap \mathbb S$:
:$\bigcap \mathbb S \subseteq T$
{{qed}}
Category:Set Intersection
Category:Subsets
nvi46jila9jjopv6mlvzhcmdtcs3ngx
Theorem: Equivalence of Definitions of Initial Topology

Let $X$ be a set.
Let $I$ be an indexing set.
Let $\family {\struct{Y_i, \tau_i}}_{i \mathop \in I}$ be an indexed family of topological spaces indexed by $I$.
Let $\family {f_i: X \to Y_i}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
{{TFAE|def = Initial Topology}}

Proof:
=== Definition 1 Implies Definition 2 ===
{{:Equivalence of Definitions of Initial Topology/Definition 1 Implies Definition 2}}{{qed|lemma}}
Theorem: Radius of Convergence from Limit of Sequence/Complex Case

Let $\xi \in \C$ be a complex number.
Let $\ds \map S z = \sum_{n \mathop = 0}^\infty a_n \paren {z - \xi}^n$ be a (complex) power series about $\xi$.
Let the sequence $\sequence {\cmod {\dfrac {a_{n + 1} } {a_n} } }_{n \mathop \in \N}$ converge.
Then $R$ is given by:
:$\ds \dfrac 1 R = \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} }$
If:
:$\ds \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} } = 0$
then the radius of convergence is infinite, and $\map S z$ is absolutely convergent for all $z \in \C$.

Proof:
Let the sequence $\sequence {\cmod {\dfrac {a_{n+1} } {a_n} } }_{n \mathop \in \N}$ converge.
Let $\epsilon \in \R_{>0}$, and let $z \in \C$.
Let $\cmod {z - \xi} = R - \epsilon$.
By definition of radius of convergence, it follows that $\map S z$ is absolutely convergent.
Then from the Ratio Test:
:$\lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} \paren {z - \xi}^{n + 1} } {a_n \paren {z - \xi}^n} } \le 1$
By Multiple Rule for Complex Sequences, this inequality can be rearranged to obtain:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} } 
      | o = \le
      | r = \cmod {\dfrac {\paren {z - \xi}^{n + 1} } {\paren {z - \xi}^n } }^{-1}
}}
{{eqn | r = \dfrac 1 {\cmod {x - \xi} }
}}
{{eqn | r = \dfrac 1 {R - \epsilon}
}}
{{end-eqn}}
{{qed|lemma}}
Let $\cmod {z - \xi} = R + \epsilon$.
Then $\map S z$ is divergent, so the Ratio Test shows that:
:$\ds \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} \paren {z - \xi}^{n + 1} } {a_n \paren {z - \xi}^n} } \ge 1$
Similarly, this inequality can be rearranged as:
:$\ds \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} } \ge \dfrac 1 {R + \epsilon}$
{{qed|lemma}}
As $\epsilon > 0$ was arbitrary, it follows that:
:$\ds \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} } = \dfrac 1 R$
Hence the result.
{{qed}}
Theorem: Radius of Convergence from Limit of Sequence/Real Case

Let $\xi \in \R$ be a real number.
Let $\ds S \paren x = \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ be a power series about $\xi$.
Then the radius of convergence $R$ of $S \paren x$ is given by:
:$\ds \frac 1 R = \lim_{n \mathop \to \infty} \size {\frac {a_{n + 1} } {a_n} }$
if this limit exists and is nonzero.
If
:$\ds \lim_{n \mathop \to \infty} \size {\frac {a_{n + 1} } {a_n} } = 0$
then the radius of convergence is infinite and therefore the interval of convergence is $\R$.

Proof:
From the ratio test, $S \paren x$ is convergent if:
:$\ds \lim_{n \mathop \to \infty} \size {\frac {a_{n + 1} \paren {x - \xi}^{n + 1} } {a_n \paren {x - \xi}^n} } < 1$
Thus:
{{begin-eqn}}
{{eqn | l = \size {\frac {a_{n + 1} \paren {x - \xi}^{n + 1} } {a_n \paren {x - \xi}^n} }
      | o = <
      | r = 1
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \size {\frac {a_{n + 1} } {a_n} } \size {x - \xi}
      | o = <
      | r = 1
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \size {\frac {a_{n + 1} } {a_n} }
      | o = <
      | r = \frac 1 {\size {x - \xi} }
      | c = 
}}
{{end-eqn}}
The result follows from the definition of radius of convergence.
{{qed}}
Theorem: Conjunction is Equivalent to Negation of Conditional of Negative/Formulation 1

:$p \land q \dashv \vdash \neg \paren {p \implies \neg q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccc||ccccc|} \hline
p & \land & q & \neg & (p & \implies & \neg & q) \\
\hline
\F & \F & \F & \F & \F & \T & \T & \F \\
\F & \F & \T & \F & \F & \T & \F & \T \\
\T & \F & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Conjunction is Equivalent to Negation of Conditional of Negative/Formulation 2

:$\vdash \paren {p \land q} \iff \paren {\neg \paren {p \implies \neg q} }$

Proof:
{{BeginTableau|\vdash \paren {p \land q} \iff \paren {\neg \paren {p \implies \neg q} } }}
{{Assumption|1|p \land q}}
{{SequentIntro|2|1|\neg \paren {p \implies \neg q}|1|Conjunction is Equivalent to Negation of Conditional of Negative: Formulation 1: Forward Implication}}
{{Implication|3||\paren {p \land q} \implies \paren {\neg \paren {p \implies \neg q} }|1|2}}
{{Assumption|4|\neg \paren {p \implies \neg q} }}
{{SequentIntro|5|4|p \land q|4|Conjunction is Equivalent to Negation of Conditional of Negative: Formulation 1: Reverse Implication}}
{{Implication|6||\paren {\neg \paren {p \implies \neg q} \implies \paren {p \land q} }|4|5}}
{{BiconditionalIntro|7||\paren {p \land q} \iff \paren {\neg \paren {p \implies \neg q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Conjunction is Equivalent to Negation of Conditional of Negative/Formulation 2

:$\vdash \paren {p \land q} \iff \paren {\neg \paren {p \implies \neg q} }$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|ccccc|} \hline
(p & \land & q) & \iff & (\neg & (p & \implies & \neg & q)) \\
\hline
\F & \F & \F & \T & \F & \F & \T & \T & \F \\
\F & \F & \T & \T & \F & \F & \T & \F & \T \\
\T & \F & \F & \T & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \F & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Conjunction is Equivalent to Negation of Conditional of Negative/Formulation 1/Forward Implication

:$p \land q \vdash \neg \paren {p \implies \neg q}$

Proof:
{{BeginTableau|p \land q \vdash \neg \paren {p \implies \neg q} }}
{{Premise|1|p \land q}}
{{Assumption|2|p \implies \neg q|Assume the opposite of what is to be proved ...}}
{{Simplification|3|1|p|1|1}}
{{Simplification|4|1|q|1|2}}
{{ModusPonens|5|1, 2|\neg q|2|3}}
{{NonContradiction|6|1, 2|4|5| ... and demonstrate a contradiction}}
{{Contradiction|7|1|\neg \paren {p \implies \neg q}|2|6}}
{{EndTableau|qed}}
Category:Conjunction is Equivalent to Negation of Conditional of Negative
bhx954r8v2k43wijh0aj8z7svkde8pc
Theorem: Rule of Material Implication/Formulation 1/Forward Implication

:$p \implies q \vdash \neg p \lor q$

Proof:
{{BeginTableau|p \implies q \vdash \neg p \lor q}}
{{Premise|1|p \implies q}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|\neg p}}
{{Addition|4|3|\neg p \lor q|3|1}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|1|5}}
{{Addition|7|1, 5|\neg p \lor q|6|2}}
{{ProofByCases|8|1|\neg p \lor q|2|3|4|5|7}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Implication/Formulation 1

:$p \implies q \dashv \vdash \neg p \lor q$

Proof:
{{BeginTableau|p \implies q \vdash \neg p \lor q}}
{{Premise|1|p \implies q}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|\neg p}}
{{Addition|4|3|\neg p \lor q|3|1}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|1|5}}
{{Addition|7|1, 5|\neg p \lor q|6|2}}
{{ProofByCases|8|1|\neg p \lor q|2|3|4|5|7}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Implication/Formulation 1

:$p \implies q \dashv \vdash \neg p \lor q$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc||cccc|} \hline
p & \implies & q & \neg & p & \lor & q \\
\hline
\F & \T & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Material Implication/Formulation 1

:$p \implies q \dashv \vdash \neg p \lor q$

Proof:
{{BeginTableau|\neg p \lor q \vdash p \implies q}}
{{Premise|1|\neg p \lor q}}
{{Assumption|2|\neg p|Pick the first of the disjuncts ...}}
{{Assumption|3|p|Assume its negation ...}}
{{NonContradiction|4|2, 3|3|2| ... and demonstrate a contradiction}}
{{Explosion|5|2, 3|q|4| ... from a falsehood, ''any'' statement can be derived - pick $q$}}
{{Implication|6|2|p \implies q|3|5}}
{{Assumption|7|q|Pick the second of the disjuncts ...}}
{{Assumption|8|p|... again assume $p$ ...}}
{{IdentityLaw|9|7|q|7|The truth of $q$ still holds}}
{{Implication|10|7|p \implies q|8|9}}
{{ProofByCases|11|1|p \implies q|1|2|6|7|10}}
{{EndTableau}}
{{qed}}