avewright/proofwiki-math huggingface dataset:
Theorem: De Morgan's Laws (Boolean Algebras)

:$\neg \paren {a \vee b} = \neg a \wedge \neg b$
:$\neg \paren {a \wedge b} = \neg a \vee \neg b$

Proof:
By virtue of Complement in Boolean Algebra is Unique, it will suffice to verify:
:$\paren {a \vee b} \wedge \paren {\neg a \wedge \neg b} = \bot$
:$\paren {a \vee b} \vee \paren {\neg a \wedge \neg b} = \top$
For the first of these, compute:
{{begin-eqn}}
{{eqn | l = \paren {a \vee b} \wedge \paren {\neg a \wedge \neg b}
      | r = \paren {\paren {a \vee b} \wedge \neg a} \wedge \neg b
      | c = $\wedge$ is associative
}}
{{eqn | r = \paren {\paren {a \wedge \neg a} \vee \paren {b \wedge \neg a} } \wedge \neg b
      | c = $\wedge$ distributes over $\vee$
}}
{{eqn | r = \paren {\bot \vee \paren {b \wedge \neg a} } \wedge \neg b
      | c = Axiom $(\text {BA} \ 4)$ for Boolean algebras
}}
{{eqn | r = \paren {b \wedge \neg a} \wedge \neg b
      | c = $\bot$ is the identity for $\vee$
}}
{{eqn | r = \neg a \wedge \paren {b \wedge \neg b}
      | c = $\wedge$ is commutative and associative
}}
{{eqn | r = \neg a \wedge \bot
      | c = Axiom $(\text {BA} \ 4)$
}}
{{eqn | r = \bot
      | c = Identities of Boolean Algebra are also Zeroes
}}
{{end-eqn}}
By the Duality Principle, we also conclude:
:$\paren {a \wedge b} \vee \paren {\neg a \vee \neg b} = \top$
Substituting $\neg a$ and $\neg b$ for $a$ and $b$, respectively, this becomes:
:$\paren {\neg a \wedge \neg b} \vee \paren {a \vee b} = \top$
where Complement of Complement (Boolean Algebras) was applied.
Since $\vee$ is commutative, we have also derived the second of the two equations above.
Hence:
:$\neg \paren {a \vee b} = \neg a \wedge \neg b$
{{qed|lemma}}
Now by again the Duality Principle:
:$\neg \paren {a \wedge b} = \neg a \vee \neg b$
follows immediately.
{{qed}}
Theorem: Complement in Boolean Algebra is Unique

Let $\left({S, \vee, \wedge}\right)$ be a Boolean algebra.
Then for all $a \in S$, there is a unique $b \in S$ such that:
:$a \wedge b = \bot, a \vee b = \top$
i.e., a valid choice for $\neg a$ as in axiom $(BA \ 4)$ for Boolean algebras.

Proof:
Suppose $b, c \in S$ both satisfy the identities.
Then:
{{begin-eqn}}
{{eqn | l = b
      | r = b \wedge \top
      | c = $\top$ is the identity for $\wedge$
}}
{{eqn | r = b \wedge \left({a \vee c}\right)
      | c = by hypothesis
}}
{{eqn | r = \left({b \wedge a}\right) \vee \left({b \wedge c}\right)
      | c = $\wedge$ distributes over $\vee$
}}
{{eqn | r = \bot \vee \left({b \wedge c}\right)
      | c = by hypothesis
}}
{{eqn | r = \left({a \wedge c}\right) \vee \left({b \wedge c}\right)
      | c = Axiom $(BA \ 4)$
}}
{{eqn | r = \left({a \vee b}\right) \wedge c
      | c = $\wedge$ distributes over $\vee$
}}
{{eqn | r = \top \wedge c
      | c = by hypothesis
}}
{{eqn | r = c
      | c = $\top$ is the identity for $\wedge$
}}
{{end-eqn}}
That is, $b = c$.
The result follows.
{{qed}}
Category:Boolean Algebras
4vs574sm211kodsk7csg2129n0tmgmh
Theorem: Cancellation of Join in Boolean Algebra

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra.
Let $a, b, c \in S$, and suppose that:
{{begin-eqn}}
{{eqn | l = a \vee c
      | r = b \vee c
}}
{{eqn | l = a \vee \neg c
      | r = b \vee \neg c
}}
{{end-eqn}}
Then $a = b$.

Proof:
{{begin-eqn}}
{{eqn | l = a
      | r = a \vee \bot
      | c = {{Boolean-algebra-axiom|1|3}}: $\bot$ is the identity for $\vee$
}}
{{eqn | r = a \vee \paren {c \wedge \neg c}
      | c = {{Boolean-algebra-axiom|1|4}}
}}
{{eqn | r = \paren {a \vee c} \wedge \paren {a \vee \neg c}
      | c = {{Boolean-algebra-axiom|1|2}}: $\vee$ distributes over $\wedge$
}}
{{eqn | r = \paren {b \vee c} \wedge \paren {b \vee \neg c}
      | c = {{hypothesis}}
}}
{{eqn | r = b \vee \paren {c \wedge \neg c}
      | c = {{Boolean-algebra-axiom|1|2}}: $\vee$ distributes over $\wedge$
}}
{{eqn | r = b \vee \bot
      | c = {{Boolean-algebra-axiom|1|4}}
}}
{{eqn | r = b
      | c = {{Boolean-algebra-axiom|1|3}}: $\bot$ is the identity for $\vee$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Cancellation of Meet in Boolean Algebra

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra.
Let $a, b, c \in S$.
Let:
{{begin-eqn}}
{{eqn | l = a \wedge c
      | r = b \wedge c
}}
{{eqn | l = a \wedge \neg c
      | r = b \wedge \neg c
}}
{{end-eqn}}
Then:
: $a = b$

Proof:
Follows from Cancellation of Join in Boolean Algebra through the Duality Principle
{{qed}}
Theorem: Absorption Laws (Boolean Algebras)

Let $\struct {S, \vee, \wedge}$ be a Boolean algebra, defined as in Definition 1.
Then:
{{begin-eqn}}
{{eqn | q = \forall a, b \in S
      | l = a
      | r = a \vee \paren {a \wedge b}
}}
{{eqn | l = a
      | r = a \wedge \paren {a \vee b}
}}
{{end-eqn}}
That is, $\vee$ absorbs $\wedge$, and $\wedge$ absorbs $\vee$.

Proof:
Let $a, b \in S$.
Then:
{{begin-eqn}}
{{eqn | l = a \vee \paren {a \wedge b}
      | r = \paren {a \wedge \top} \vee \paren {a \wedge b}
      | c = {{Boolean-algebra-axiom|1|3}}: $\top$ is the identity for $\wedge$
}}
{{eqn | r = a \wedge \paren {\top \vee b}
      | c = {{Boolean-algebra-axiom|1|2}}: $\wedge$ distributes over $\vee$
}}
{{eqn | r = a \wedge \top
      | c = Identities of Boolean Algebra are also Zeroes
}}
{{eqn | r = a
      | c = {{Boolean-algebra-axiom|1|3}}: $\top$ is the identity for $\wedge$
}}
{{end-eqn}}
as desired.
{{qed|lemma}}
The result:
:$a = a \wedge \paren {a \vee b}$
follows from the Duality Principle.
{{qed}}
Theorem: Difference of Absolutely Convergent Series

Let $\ds \sum_{n \mathop = 1}^\infty a_n$ and $\ds \sum_{n \mathop = 1}^\infty b_n$ be two real or complex series that are absolutely convergent.
Then the series $\ds \sum_{n \mathop = 1}^\infty \paren {a_n - b_n}$ is absolutely convergent, and:
:$\ds \sum_{n \mathop = 1}^\infty \paren {a_n - b_n} = \sum_{n \mathop = 1}^\infty a_n - \sum_{n \mathop = 1}^\infty b_n$

Proof:
The series $\ds \sum_{n \mathop = 1}^\infty \paren {-b_n}$ is absolutely convergent, as $\cmod {-b_n} = \cmod {b_n}$ for all $n \in \N$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty a_n - \sum_{n \mathop = 1}^\infty b_n
      | r = \sum_{n \mathop = 1}^\infty a_n + \paren {-1} \sum_{n \mathop = 1}^\infty b_n
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty a_n + \sum_{n \mathop = 1}^\infty \paren {-1} b_n
      | c = Manipulation of Absolutely Convergent Series: Scale Factor
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {a_n - b_n}
      | c = Sum of Absolutely Convergent Series
}}
{{end-eqn}}
{{qed}}
Theorem: True Statement is implied by Every Statement/Formulation 2

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

Proof:
{{BeginTableau|\vdash q \implies \paren {p \implies q} }}
{{Assumption|1|q}}
{{SequentIntro|2|1|p \implies q|1|True Statement is implied by Every Statement: Formulation 1}}
{{Implication|3||q \implies \paren {p \implies q}|1|2}}
{{EndTableau}}
{{qed}}
Theorem: True Statement is implied by Every Statement/Formulation 2

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

Proof:
{{BeginTableau|\vdash q \implies \paren {p \implies q} }}
{{Assumption|1|p}}
{{Assumption|2|q}}
{{Implication|3|1|p \implies q|1|2}}
{{Implication|4||q \implies \paren {p \implies q}|2|3}}
{{EndTableau}}
{{qed}}
Theorem: True Statement is implied by Every Statement/Formulation 2

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth value under the main connective, the first instance of $\implies$, is $\T$ for each boolean interpretation.
$\begin{array}{|ccccc|} \hline
q & \implies & ( p & \implies & q ) \\
\hline
\F & \T & \T & \F & \F \\
\F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T \\
\T & \T & \F & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: True Statement is implied by Every Statement

==== Formulation 1 ====
{{:True Statement is implied by Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:True Statement is implied by Every Statement/Formulation 2}}

Proof:
{{BeginTableau|p \vdash q \implies p}}
{{Premise|1|p}}
{{Addition|2|1|\neg q \lor p|1|2}}
{{SequentIntro|3|1|q \implies p|1|Rule of Material Implication}}
{{EndTableau}}
{{qed}}
Theorem: True Statement is implied by Every Statement

==== Formulation 1 ====
{{:True Statement is implied by Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:True Statement is implied by Every Statement/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, where the truth value in the relevant column on the {{LHS}} is $\T$, that under the one on the {{RHS}} is also $\T$:
:<nowiki>$\begin{array}{|c||ccc|} \hline
p & q & \implies & p \\
\hline
\F & \F & \T & \F \\
\F & \T & \F & \F \\
\T & \F & \T & \T \\
\T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: True Statement is implied by Every Statement

==== Formulation 1 ====
{{:True Statement is implied by Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:True Statement is implied by Every Statement/Formulation 2}}

Proof:
{{BeginTableau|\vdash q \implies \paren {p \implies q} }}
{{Assumption|1|q}}
{{SequentIntro|2|1|p \implies q|1|True Statement is implied by Every Statement: Formulation 1}}
{{Implication|3||q \implies \paren {p \implies q}|1|2}}
{{EndTableau}}
{{qed}}
Theorem: True Statement is implied by Every Statement

==== Formulation 1 ====
{{:True Statement is implied by Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:True Statement is implied by Every Statement/Formulation 2}}

Proof:
{{BeginTableau|\vdash q \implies \paren {p \implies q} }}
{{Assumption|1|p}}
{{Assumption|2|q}}
{{Implication|3|1|p \implies q|1|2}}
{{Implication|4||q \implies \paren {p \implies q}|2|3}}
{{EndTableau}}
{{qed}}
Theorem: True Statement is implied by Every Statement

==== Formulation 1 ====
{{:True Statement is implied by Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:True Statement is implied by Every Statement/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth value under the main connective, the first instance of $\implies$, is $\T$ for each boolean interpretation.
$\begin{array}{|ccccc|} \hline
q & \implies & ( p & \implies & q ) \\
\hline
\F & \T & \T & \F & \F \\
\F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T \\
\T & \T & \F & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: False Statement implies Every Statement

==== Formulation 1 ====
{{:False Statement implies Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:False Statement implies Every Statement/Formulation 2}}

Proof:
{{BeginTableau|\neg p \vdash p \implies q}}
{{Premise|1|\neg p}}
{{Addition|2|1|\neg p \lor q|1|1}}
{{SequentIntro|3|1|p \implies q|2|Rule of Material Implication}}
{{EndTableau|qed}}
Theorem: False Statement implies Every Statement

==== Formulation 1 ====
{{:False Statement implies Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:False Statement implies Every Statement/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, where the truth value in the relevant column on the {{LHS}} is $\T$, that under the one on the {{RHS}} is also $\T$:
:<nowiki>$\begin{array}{|cc||ccc|} \hline
\neg & p & p & \implies & q \\
\hline
\T & \F & \F & \T & \F \\
\T & \F & \F & \T & \T \\
\F & \F & \T & \F & \F \\
\F & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: False Statement implies Every Statement

==== Formulation 1 ====
{{:False Statement implies Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:False Statement implies Every Statement/Formulation 2}}

Proof:
{{BeginTableau|\vdash \neg p \implies \left({p \implies q}\right)}}
{{Assumption|1|\neg p}}
{{Assumption|2|p}}
{{NonContradiction|3|1, 2|2|1}}
{{Explosion|4|1, 2|q|3}}
{{Implication|5|1|p \implies q|2|4}}
{{Implication|6||\neg p \implies \left({p \implies q}\right)|1|5}}
{{EndTableau}}
{{qed}}
Theorem: False Statement implies Every Statement

==== Formulation 1 ====
{{:False Statement implies Every Statement/Formulation 1}}
==== Formulation 2 ====
{{:False Statement implies Every Statement/Formulation 2}}

Proof:
{{BeginTableau|\vdash \neg p \implies \left({p \implies q}\right)}}
{{Assumption|1|\neg p}}
{{SequentIntro|2|1|p \implies q|1|False Statement implies Every Statement: Formulation 1}}
{{Implication|3||\neg p \implies \left({p \implies q}\right)|1|2}}
{{EndTableau}}
{{qed}}
Theorem: False Statement implies Every Statement/Formulation 2

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

Proof:
{{BeginTableau|\vdash \neg p \implies \left({p \implies q}\right)}}
{{Assumption|1|\neg p}}
{{Assumption|2|p}}
{{NonContradiction|3|1, 2|2|1}}
{{Explosion|4|1, 2|q|3}}
{{Implication|5|1|p \implies q|2|4}}
{{Implication|6||\neg p \implies \left({p \implies q}\right)|1|5}}
{{EndTableau}}
{{qed}}
Theorem: False Statement implies Every Statement/Formulation 2

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

Proof:
{{BeginTableau|\vdash \neg p \implies \left({p \implies q}\right)}}
{{Assumption|1|\neg p}}
{{SequentIntro|2|1|p \implies q|1|False Statement implies Every Statement: Formulation 1}}
{{Implication|3||\neg p \implies \left({p \implies q}\right)|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Smullyan's Drinking Principle

Suppose that there is at least one person in the pub.
Then there is a person $x$ in the pub such that if $x$ is drinking, then everyone in the pub is drinking.

Proof:
We have two choices:
:$\forall y : \map D y$
and
:$\neg \forall y : \map D y$
Suppose $\forall y : \map D y$.
By True Statement is implied by Every Statement:
:$\map D x \implies \forall y : \map D y$
By Existential Generalisation:
:$\exists x : \paren {\map D x \implies \forall y : \map D y}$
Now suppose:
:$\neg \forall y : \map D y$
By De Morgan's Laws (Predicate Logic)/Denial of Universality:
:$\exists y : \neg \map D y$
Switch the variable $y$ with $x$.
Thus, for some $x$:
:$\neg \map D x$
By False Statement implies Every Statement, we have:
:$\map D x \implies \forall y : \map D y$
By Existential Generalisation:
:$\exists x : \paren {\map D x \implies \forall y : \map D y}$
Thus, $\exists x : \paren {\map D x \implies \forall y : \map D y}$ holds both when:
:$\forall y : \map D y$
and when:
:$\neg \forall y : \map D y$
concluding the proof.
{{qed}}
Theorem: Smullyan's Drinking Principle

Suppose that there is at least one person in the pub.
Then there is a person $x$ in the pub such that if $x$ is drinking, then everyone in the pub is drinking.

Proof:
Either everyone in the pub is drinking or someone in the pub is not drinking.
Suppose that everyone in the pub is drinking.
By True Statement is implied by Every Statement, the statement:
:''everyone in the pub is drinking''
is implied by the statement:
:''$x$ is drinking''
for any $x$ in the pub.
Since the pub is by assumption non-empty, there exists some $x$ in the pub.
Thus, there is some $x$ in the pub such that, if $x$ is drinking, then everyone in the pub is drinking.
Now suppose that there is some $x$ in the pub who is not drinking.
By False Statement implies Every Statement, if $x$ is drinking then everyone in the pub is drinking.
Thus, there is some $x$ in the pub such that, if $x$ is drinking, then everyone in the pub is drinking.
{{qed}}
Theorem: Two is Boolean Algebra

Let $\mathbf 2$ denote two.
Then $\mathbf 2$ is a Boolean algebra.

Proof:
It is useful to first state the Cayley tables for the three logical operations $\lor$, $\land$ and $\neg$:
:<nowiki>$\begin{array}{c|cc}
 \lor & \bot & \top \\ \hline
 \bot & \bot & \top \\
 \top & \top & \top
\end{array} \qquad \begin{array}{c|cc}
 \land & \bot & \top \\ \hline
 \bot  & \bot & \bot \\
 \top  & \bot & \top
\end{array} \qquad \begin{array}{c|cc}
      & \bot & \top \\ \hline
 \neg & \top & \bot
\end{array}$
</nowiki>
Let us now verify the axioms for a Boolean algebra in turn.
Theorem: Two-Valued Functions form Boolean Algebra

Let $\mathbf 2$ be the Boolean algebra two, and let $X$ be a set.
Let $\mathbf 2^X$ be the set of all mappings $p: X \to \mathbf 2$.
Define the operations $\vee$, $\wedge$ and $\neg$ on $\mathbf 2^X$ in pointwise fashion thus:
:$\vee: \mathbf 2^X \times \mathbf 2^X \to \mathbf 2^X, \left({p \vee q}\right) (x) := p (x) \vee q (x)$
:$\wedge: \mathbf 2^X \times \mathbf 2^X \to \mathbf 2^X, \left({p \wedge q}\right) (x) := p (x) \wedge q (x)$
:$\neg: \mathbf 2^X \to \mathbf 2^X, \left({\neg p}\right) (x) := \neg p (x)$
Furthermore, write $\bot$ and $\top$ for the constant mappings with these values, viz:
:$\bot: X \to \mathbf 2, \bot (x) := \bot$
:$\top: X \to \mathbf 2, \top (x) := \top$
Then $\left({\mathbf 2^X, \vee, \wedge, \neg}\right)$ is a Boolean algebra, with $\bot$ and $\top$ as identities for $\vee$ and $\wedge$, respectively.

Proof:
Let us verify the axioms for a Boolean algebra in turn.
Theorem: Power Set and Two-Valued Functions are Isomorphic Boolean Rings

Let $S$ be a set.
Let $\mathbf 2$ be the Boolean ring two.
Let $\powerset S$ be the power set of $S$; by Symmetric Difference with Intersection forms Boolean Ring, it is a Boolean ring.
Let $\mathbf 2^S$ be the set of all mappings $f: S \to \mathbf 2$; by Two-Valued Functions form Boolean Ring, it is also a Boolean ring
Let $\chi_{\paren \cdot}: \powerset S \to \mathbf 2^S$ be the characteristic function operation.
Then $\chi_{\paren \cdot}$ is a ring isomorphism.

Proof:
From Support Operation Inverse to Characteristic Function Operation, $\chi_{\paren \cdot}$ is a bijection.
It therefore suffices to establish it is a ring homomorphism.
By Characteristic Function of Symmetric Difference:
:$\chi_{A * B} = \chi_A + \chi_B - 2 \chi_A \chi_B$
Since $\mathbf 2^S$ is a Boolean ring, by Idempotent Ring has Characteristic Two, the {{RHS}} reduces to:
:$\chi_{A * B} = \chi_A + \chi_B$
showing that $\chi_{\paren \cdot}$ preserves ring addition.
By Characteristic Function of Intersection: Variant 1:
:$\chi_{A \cap B} = \chi_A \cdot \chi_B$
showing that $\chi_{\paren \cdot}$ preserves the ring product.
Hence $\chi_{\paren \cdot}$ is a ring homomorphism.
The result follows.
{{qed}}
Theorem: Peirce's Law/Formulation 1

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

Proof:
{{BeginTableau|\paren {p \implies q} \implies p \vdash p}}
{{Premise|1|\paren {p \implies q} \implies p}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|\neg p}}
{{SequentIntro|4|3|p \implies q|3|False Statement implies Every Statement}}
{{ModusPonens|5|1, 3|p|1|4}}
{{Assumption|6|p}}
{{ProofByCases|7|1|p|2|3|5|6|6}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Peirce's Law/Formulation 1

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

Proof:
{{BeginTableau|\paren {p \implies q} \implies p \vdash p}}
{{Premise|1|\paren {p \implies q} \implies p}}
{{Assumption|2|\neg p}}
{{SequentIntro|3|2|p \implies q|2|False Statement implies Every Statement}}
{{ModusPonens|4|1,2|p|1|3}}
{{NonContradiction|5|1,2|2|4}}
{{Reductio|6|1|p|2|5}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum|3}}
Theorem: Peirce's Law/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies q} \implies p} \implies p}}
{{Assumption|1|\paren {p \implies q} \implies p}}
{{SequentIntro|2|1|p|1|Peirce's Law: Formulation 1: $\paren {p \implies q} \implies p \vdash p$}}
{{Implication|3||\paren {\paren {p \implies q} \implies p} \implies p|1|2}}
{{EndTableau}}
{{qed}}
{{LEM|Peirce's Law/Formulation 1|3}}
Theorem: Peirce's Law/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies q} \implies p} \implies p}}
{{Premise|1|\paren {p \implies q} \implies p}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|\neg p}}
{{SequentIntro|4|3|p \implies q|3|False Statement implies Every Statement}}
{{ModusPonens|5|1, 3|p|1|4}}
{{Assumption|6|p}}
{{ProofByCases|7|1|p|2|3|5|6|6}}
{{Implication|8||\paren {\paren {p \implies q} \implies p} \implies p|1|7}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Peirce's Law/Formulation 2

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

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective are $\T$ for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|c|}\hline
((p & \implies & q) & \implies & p) & \implies & p \\
\hline
\F & \T & \F & \F & \F & \T & \F \\
\F & \T & \T & \F & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Peirce's Law/Strong Form/Formulation 2

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

Proof:
=== $(1):$ $\vdash$ Direction ===
{{:Peirce's Law/Strong Form/Formulation 2/Forward Direction}}
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 1

:$p \land \neg q \dashv \vdash \neg \paren {p \implies 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}{|cccc||cccc|} \hline
p & \land & \neg & q & \neg & (p & \implies & q) \\
\hline
\F & \F & \T & \F & \F & \F & \T & \F \\
\F & \F & \F & \T & \F & \F & \T & \T \\
\T & \T & \T & \F & \T & \T & \F & \F \\
\T & \F & \F & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 1/Forward Implication

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

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

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

Proof:
{{BeginTableau|\neg \paren {p \implies q} \vdash p \land \neg q}}
{{Premise|1|\neg \paren {p \implies q} }}
{{Assumption|2|\neg \paren {p \land \neg q} }}
{{SequentIntro|3|2|p \implies q|2|Conditional is Equivalent to Negation of Conjunction with Negative}}
{{NonContradiction|4|1, 2|3|1}}
{{Reductio|5|1|p \land \neg q|2|4}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum|3}}
Category:Conjunction with Negative is Equivalent to Negation of Conditional
6mc59y7ttqepgzomz211lrh1hxpli11
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 2

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

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

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

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