avewright/proofwiki-math huggingface dataset:
Theorem: Biconditional is Transitive/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\paren {p \iff q} \land \paren {q \iff r} } \implies \paren {p \iff r} }}
{{Assumption|1|\paren {p \iff q} \land \paren {q \iff r} }}
{{Simplification|2|1|p \iff q|1|1}}
{{Simplification|3|1|q \iff r|1|2}}
{{SequentIntro|4|1|p \iff r|2, 3|Biconditional is Transitive: Formulation 1}}
{{Implication|5||\paren {\paren {p \iff q} \land \paren {q \iff r} } \implies \paren {p \iff r}|1|4}}
{{EndTableau}}
{{qed}}
Theorem: Biconditional as Disjunction of Conjunctions/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|p \iff q \vdash \paren {p \land q} \lor \paren {\neg p \land \neg q} }}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{BiconditionalElimination|3|1|q \implies p|1|2}}
{{ExcludedMiddle|4|p \lor \neg p}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|2|5}}
{{Conjunction|7|1, 5|p \land q|5|6}}
{{Addition|8|1, 5|\paren {p \land q} \lor \paren {\neg p \land \neg q}|7|1}}
{{Assumption|9|\neg p}}
{{ModusTollens|10|1, 9|\neg q|3|9}}
{{Conjunction|11|1, 9|\neg p \land \neg q|9|10}}
{{Addition|12|1, 9|\paren {p \land q} \lor \paren {\neg p \land \neg q}|11|2}}
{{ProofByCases|13|1|\paren {p \land q} \lor \paren {\neg p \land \neg q}|1|5|8|9|12}}
{{EndTableau}}
{{qed}}
{{LEM}}
Category:Biconditional as Disjunction of Conjunctions
7wl576xv2ies61jb9sytj4wobypi3dk
Theorem: Biconditional as Disjunction of Conjunctions/Formulation 1/Reverse Implication

: $\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right) \vdash p \iff q$

Proof:
{{BeginTableau|\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right) \vdash p \iff q}}
{{Premise|1|\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)}}
{{Assumption|2|p \land q}}
{{Assumption|3|p}}
{{Simplification|4|2|q|2|2}}
{{Implication|5|2|p \implies q|3|4}}
{{Assumption|6|q}}
{{Simplification|7|2|p|2|1}}
{{Implication|8|2|q \implies p|6|7}}
{{BiconditionalIntro|9|2|p \iff q|5|8}}
{{Assumption|10|\neg p \land \neg q}}
{{Assumption|11|\neg p}}
{{Simplification|12|10|\neg q|10|2}}
{{Implication|13|10|\neg p \implies \neg q|11|12}}
{{SequentIntro|14|10|q \implies p|13|Rule of Transposition}}
{{Assumption|15|\neg q}}
{{Simplification|16|10|\neg p|10|1}}
{{Implication|17|10|\neg q \implies \neg p|15|16}}
{{SequentIntro|18|10|p \implies q|17|Rule of Transposition}}
{{BiconditionalIntro|19|10|p \iff q|18|14}}
{{ProofByCases|20|1|p \iff q|1|2|9|10|19}}
{{EndTableau}}
{{qed}}
Category:Biconditional as Disjunction of Conjunctions
kpkzs6086yvdup4ehfnuooz56hz7783
Theorem: Biconditional as Disjunction of Conjunctions/Formulation 1

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, in all cases the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc||ccccccccc|} \hline
p & \iff & q & (p & \land & q) & \lor & (\neg & p & \land & \neg & q) \\
\hline
\F & \T & \F & \F & \F & \F & \T & \T & \F & \T & \T & \F \\
\F & \F & \T & \F & \F & \T & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \T & \F & \F & \F & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Biconditional as Disjunction of Conjunctions/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \iff q} \iff \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} } }}
{{Assumption        |1|p \iff q}}
{{SequentIntro      |2|1|\paren {p \land q} \lor \paren {\neg p \land \neg q}|1|Biconditional as Disjunction of Conjunctions: Formulation 1}}
{{Implication       |3| |\paren {p \iff q} \implies \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} }|1|2}}
{{Assumption        |4|\paren {p \land q} \lor \paren {\neg p \land \neg q} }}
{{SequentIntro      |5|4|p \iff q|4|Biconditional as Disjunction of Conjunctions: Formulation 1}}
{{Implication       |6| |\paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} } \implies \paren {p \iff q}|4|5}}
{{BiconditionalIntro|7| |\paren {p \iff q} \iff \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Biconditional as Disjunction of Conjunctions/Formulation 2

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, in all cases the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccc|c|ccccccccc|} \hline
(p & \iff & q) & \iff & ((p & \land & q) & \lor & (\neg & p & \land & \neg & q)) \\
\hline
\F & \T & \F & \T & \F & \F & \F & \T & \T & \F & \T & \T & \F \\
\F & \F & \T & \T & \F & \F & \T & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \T & \T & \F & \F & \F & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Biconditional Equivalent to Biconditional of Negations/Formulation 1/Forward Implication

:$p \iff q \vdash \neg p \iff \neg q$

Proof:
{{BeginTableau|p \iff q \vdash \neg p \iff \neg q}}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{SequentIntro|3|1|\neg q \implies \neg p|2|Rule of Transposition}}
{{BiconditionalElimination|4|1|q \implies p|1|2}}
{{SequentIntro|5|1|\neg p \implies \neg q|4|Rule of Transposition}}
{{BiconditionalIntro|6|1|\neg p \iff \neg q|5|3}}
{{EndTableau|qed}}
Theorem: Biconditional Equivalent to Biconditional of Negations/Formulation 1/Reverse Implication

:$\neg p \iff \neg q \vdash p \iff q$

Proof:
{{BeginTableau|\neg p \iff \neg q \vdash p \iff q}}
{{Premise|1|\neg p \iff \neg q}}
{{BiconditionalElimination|2|1|\neg p \implies \neg q|1|1}}
{{SequentIntro|3|1|\neg \neg q \implies \neg \neg p|2|Rule of Transposition}}
{{DoubleNegElimination|4|1|q \implies p|3|(twice)}}
{{BiconditionalElimination|5|1|\neg q \implies \neg p|1|2}}
{{SequentIntro|6|1|\neg \neg p \implies \neg \neg q|5|Rule of Transposition}}
{{DoubleNegElimination|7|1|p \implies q|3|(twice)}}
{{BiconditionalIntro|8|1|p \iff q|7|4}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Biconditional iff Disjunction implies Conjunction/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|p \iff q \vdash \paren {p \lor q} \implies \paren {p \land q} }}
{{Premise     |1|p \iff q}}
{{SequentIntro|2|1|\paren {p \land q} \lor \paren {\neg p \land \neg q}|1|Biconditional as Disjunction of Conjunctions}}
{{DeMorgan    |3|1|\paren {p \land q} \lor \neg \paren {p \lor q}|2|Conjunction of Negations}}
{{Commutation |4|1|\neg \paren {p \lor q} \lor \paren {p \land q}|3|Disjunction}}
{{SequentIntro|5|1|\paren {p \lor q} \implies \paren {p \land q}|4|Rule of Material Implication}}
{{EndTableau|qed}}
Category:Biconditional iff Disjunction implies Conjunction
gwmmdt1jjyuu9o5wjmzqeyy18ryvijl
Theorem: Biconditional iff Disjunction implies Conjunction/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau|\paren {p \lor q} \implies \paren {p \land q} \vdash p \iff q}}
{{Premise|1|\paren {p \lor q} \implies \paren {p \land q} }}
{{SequentIntro|2|1|\neg \paren {p \lor q} \lor \paren {p \land q}|1|Rule of Material Implication}}
{{Commutation|3|1|\paren {p \land q} \lor \neg \paren {p \lor q}|2|Disjunction}}
{{DeMorgan|4|1|\paren {p \land q} \lor \paren {\neg p \land \neg q}|3|Conjunction of Negations}}
{{SequentIntro|5|1|\paren {p \implies q} \land \paren {q \implies p}|4
  |Biconditional as Disjunction of Conjunctions}}
{{SequentIntro|6|1|p \iff q|5|Rule of Material Equivalence}}
{{EndTableau}}
{{qed}}
{{LEM|Rule of Material Implication}}
Category:Biconditional iff Disjunction implies Conjunction
jqdy658aw8hc3lliet88riceo86768k
Theorem: Biconditional iff Disjunction implies Conjunction/Formulation 1

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, in all cases the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc||ccccccc|} \hline
p & \iff & q & (p & \lor & q) & \implies & (p & \land & q) \\
\hline
\F & \T & \F & \F & \F & \F & \T & \F & \F & \F \\
\F & \F & \T & \F & \T & \T & \F & \F & \F & \T \\
\T & \F & \F & \T & \T & \F & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Biconditional iff Disjunction implies Conjunction/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \iff q} \iff \paren {\paren {p \lor q} \implies \paren {p \land q} } }}
{{Assumption|1|p \iff q}}
{{SequentIntro|2|1|\paren {p \lor q} \implies \paren {p \land q}|1|Biconditional iff Disjunction implies Conjunction: Formulation 1}}
{{Implication|3||\paren {p \iff q} \implies \paren {\paren {p \lor q} \implies \paren {p \land q} }|1|2}}
{{Assumption|4|\paren {p \lor q} \implies \paren {p \land q} }}
{{SequentIntro|5|4|p \iff q|4|Biconditional iff Disjunction implies Conjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \lor q} \implies \paren {p \land q} } \implies \paren {p \iff q}|4|5}}
{{BiconditionalIntro|7||\paren {p \iff q} \iff \paren {\paren {p \lor q} \implies \paren {p \land q} }|3|6}}
{{EndTableau|qed}}
Category:Biconditional iff Disjunction implies Conjunction
ped3t1i3j2njrik98s3s2wh0of6qnrx
Theorem: Order of Squares in Totally Ordered Ring without Proper Zero Divisors

Let $\struct {R, +, \circ, \le}$ be a totally ordered ring without proper zero divisors whose zero is $0_R$.
Let $x, y \in R$ be positive, that is, $0_R \le x, y$.
Then $x \le y \iff x \circ x \le y \circ y$.
That is, the square mapping is an order embedding of $\struct {R_{\ge 0}, \le}$ into itself.
When $R$ is one of the standard sets of numbers $\Z, \Q, \R$, then this translates into:
:If $x, y$ are positive, then $x \le y \iff x^2 \le y^2$.

Proof:
From Order of Squares in Ordered Ring, we have:
:$x \le y \implies x \circ x \le y \circ y$
To prove the opposite implication, we use a Proof by Contradiction.
{{AimForCont}} $x \circ x \le y \circ y$ but $x \not\le y$.
Since $\le$ is a total ordering, this means $y < x$.
Since $0_R \le y$, Extended Transitivity shows that $0_R < x$, so in particular $x ≠ 0_R$.
As $\le$ is compatible with the ring structure $\struct {R, +, \circ}$ and $x$ and $y$ are both positive, we have:
:$y \circ y \le y \circ x \le x \circ x$
Since we assume $x \circ x \le y \circ y$, Ordering Cycle implies Equality shows that:
:$y \circ y = x \circ x = y \circ x$
Therefore:
{{begin-eqn}}
{{eqn | l = 0_R
      | r = x \circ x + \paren {-\paren {y \circ x} }
      | c = {{Defof|Ring Negative}}
}}
{{eqn | r = x \circ x + \paren {-y} \circ x
      | c = Product with Ring Negative
}}
{{eqn | r = \paren {x + \paren {-y} } \circ x
      | c = {{Ring-axiom|D}}
}}
{{end-eqn}}
Since $x \ne y$, we have that $x + \paren {-y} \ne 0_R$; otherwise, by {{Ring-axiom|A1}}, we would have $x = \paren {x + \paren {-y} } + y = y$.
We have already shown that $x \ne 0_R$.
But then $x$ and $x + \paren {-y}$ are proper zero divisors of $R$, contradicting the hypothesis that $R$ has no proper zero divisors.
{{qed}}
Theorem: Order of Squares in Ordered Field

Let $\struct {R, +, \circ, \le}$ be an ordered field whose zero is $0_R$ and whose unity is $1_R$.
Suppose that $\forall a \in R: 0 < a \implies 0 < a^{-1}$.
Let $x, y \in \struct {R, +, \circ, \le}$ such that $0_R \le x, y$.
Then $x \le y \iff x \circ x \le y \circ y$.
That is, the square function is an order embedding of $\struct {R_{\ge 0}, \le}$ into itself.
When $R$ is one of the standard fields of numbers $\Q$ and $\R$, then this translates into:
:If $x, y$ are positive then $x \le y \iff x^2 \le y^2$.

Proof:
From Order of Squares in Ordered Ring, we have:
:$x \le y \implies x \circ x \le y \circ y$
To prove the reverse implication, suppose that $x \circ x \le y \circ y$.
Thus:
{{begin-eqn}}
{{eqn | l = x \circ x
      | o = \le
      | r = y \circ y
      | c = 
}}
{{eqn | ll=\leadsto
      | l = x \circ x + \paren {-\paren {x \circ x} }
      | o = \le
      | r = y \circ y + \paren {-\paren {x \circ x} }
      | c = 
}}
{{eqn | ll=\leadsto
      | l = 0_R
      | o = \le
      | r = y \circ y + \paren {-\paren {x \circ x} }
      | c = 
}}
{{eqn | ll=\leadsto
      | l = 0_R
      | o = \le
      | r = \paren {y + \paren {-x} } \circ \paren {y + x}
      | c = Difference of Two Squares, which applies because a field is a commutative ring.
}}
{{end-eqn}}
As $0_R \le x, y$ we have $0_R \le x + y$.
Hence by the premise we have $0_R \le \paren {x + y}^{-1}$.
So as $0_R \le \paren {y + \paren {-x} } \circ \paren {y + x}$ we can multiply both sides by $\paren {x + y}^{-1}$ and get $0_R \le \paren {y + \paren {-x} }$.
Adding $-x$ to both sides gives us $x \le y$.
{{qed}}
Theorem: Law of Identity/Formulation 1

:$p \vdash p$

Proof:
{{BeginTableau|p \vdash p}}
{{Premise|1|p}}
{{EndTableau|qed}}
This is the shortest tableau proof possible.
Theorem: Law of Identity/Formulation 1

:$p \vdash p$

Proof:
We apply the Method of Truth Tables (trivially) to the proposition.
:<nowiki>$\begin{array}{|c|c|} \hline
p & p \\
\hline
\F & \F \\
\T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Law of Identity/Formulation 2

Every proposition entails itself:
:$\vdash p \implies p$

Proof:
{{BeginTableau|\vdash p \implies p}}
{{Premise|1|p}}
{{Implication|2||p \implies p|1|1}}
{{EndTableau|qed}}
Theorem: Law of Identity/Formulation 2

Every proposition entails itself:
:$\vdash p \implies p$

Proof:
Using a tableau proof for instance 1 of a Hilbert proof system:
{{BeginTableau|p \implies p|nohead = 1}}
{{TableauLine|n = 1
  | f = \paren {p \implies \paren {\paren {p \implies p} \implies p} } \implies \paren {\paren {p \implies \paren {p \implies p} } \implies \paren {p \implies p} }
  | rtxt = Axiom 2
  | c = $\mathbf A = p, \mathbf B = p \implies p, \mathbf C = p$
}}
{{TableauLine|n = 2
  | f = p \implies \paren {\paren {p \implies p} \implies p}
  | rtxt = Axiom 1
  | c = $\mathbf A = p, \mathbf B = p \implies p$
}}
{{ModusPonens|3||\paren {p \implies \paren {p \implies p} } \implies \paren {p \implies p}|1|2}}
{{TableauLine|n = 4
  | f = p \implies \paren {p \implies p}
  | rtxt = Axiom 1
  | c = $\mathbf A = p, \mathbf B = p$
}}
{{ModusPonens|5||p \implies p|3|4}}
{{EndTableau}}
{{qed}}
Theorem: Law of Identity/Formulation 2

Every proposition entails itself:
:$\vdash p \implies p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth value under the main connective is $\T$ throughout.
:<nowiki>$\begin{array}{|ccc|} \hline
p & \implies & p \\
\hline
\F & \T & \F \\
\T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Neighborhood Condition for Coarser Topology

Let $S$ be a set.
Let $\tau_1$ and $\tau_2$ be two topologies on $S$.
Suppose that for all $z \in S$ and for all open neighborhoods $N_z$ of $z$ with respect to $\tau_1$, there exists $U \in \tau_2$ such that $U \subseteq N_z$.
Then $\tau_1$ is coarser than $\tau_2$.

Proof:
Let $V \in \tau_1$.
For all $z \in V$, we have that $V$ is an open neighborhood of $z$ with respect to $\tau_1$.
Then for all $z \in V$, we can find $U_z \in \tau_2$ such that $z \in U_z \subseteq V$.
Then:
:$\ds V = \bigcup_{z \mathop \in V } \set z \subseteq \bigcup_{z \mathop \in V } U_z \subseteq V$
By definition of set equality, it follows that:
:$\ds V = \bigcup_{z \mathop \in V} U_z \in \tau_2$
Hence:
:$\tau_1 \subseteq \tau_2$
which by definition means that $\tau_1$ is coarser than $\tau_2$.
{{qed}}
Category:Topology
pygg2k7jfc9t7mddzow4iv48k2evff4
Theorem: Absorption Laws (Logic)/Conjunction Absorbs Disjunction/Proof 2

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

Proof:
By calculation:
{{begin-eqn}}
{{eqn | l = p \land \paren {p \lor q}
      | r = \paren {p \lor \bot} \land \paren {p \lor q}
      | c = Disjunction with Contradiction
}}
{{eqn | r = p \lor \paren {\bot \land q}
      | c = Disjunction is Left Distributive over Conjunction
}}
{{eqn | r = p \lor \bot
      | c = Conjunction with Contradiction
}}
{{eqn | r = p
      | c = Disjunction with Contradiction
}}
{{end-eqn}}
{{qed}}
Theorem: Absorption Laws (Logic)/Conjunction Absorbs Disjunction/Forward Implication

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

Proof:
{{BeginTableau|p \land \paren {p \lor q} \vdash p}}
{{Premise|1|p \land \paren {p \lor q} }}
{{Simplification|2|1|p|1|1}}
{{EndTableau|qed}}
Theorem: Absorption Laws (Logic)/Conjunction Absorbs Disjunction/Reverse Implication

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

Proof:
{{BeginTableau|p \vdash p \land \paren {p \lor q} }}
{{Premise|1|p}}
{{Addition|2|1|p \lor q|1|1}}
{{Conjunction|3|1|p \land \paren {p \lor q}|1|2}}
{{EndTableau|qed}}
Theorem: Absorption Laws (Logic)/Conjunction Absorbs Disjunction

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

Proof:
By calculation:
{{begin-eqn}}
{{eqn | l = p \land \paren {p \lor q}
      | r = \paren {p \lor \bot} \land \paren {p \lor q}
      | c = Disjunction with Contradiction
}}
{{eqn | r = p \lor \paren {\bot \land q}
      | c = Disjunction is Left Distributive over Conjunction
}}
{{eqn | r = p \lor \bot
      | c = Conjunction with Contradiction
}}
{{eqn | r = p
      | c = Disjunction with Contradiction
}}
{{end-eqn}}
{{qed}}
Theorem: Absorption Laws (Logic)/Conjunction Absorbs Disjunction

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the appropriate truth values match for all boolean interpretations.
$\begin{array}{|ccccc||c|} \hline
p & \land & (p & \lor & q) & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \F & \F & \T & \T & \F \\
\T & \T & \T & \T & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Absorption Laws (Logic)/Disjunction Absorbs Conjunction/Forward Implication

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

Proof:
{{BeginTableau|p \lor \paren {p \land q} \vdash p}}
{{Premise|1|p \lor \paren {p \land q} }}
{{Assumption|2|p}}
{{Assumption|3|p \land q}}
{{Simplification|4|3|p|3|1}}
{{ProofByCases|5|1|p|1|2|2|3|4}}
{{EndTableau|qed}}
Theorem: Absorption Laws (Logic)/Disjunction Absorbs Conjunction/Reverse Implication

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

Proof:
{{BeginTableau|p \vdash p \lor \paren {p \land q} }}
{{Premise|1|p}}
{{Addition|2|1|p \lor \paren {p \land q}|1|1}}
{{EndTableau|qed}}
Theorem: Absorption Laws (Logic)/Disjunction Absorbs Conjunction

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

Proof:
{{begin-eqn}}
{{eqn | l = p \lor \paren {p \land q}
      | r = \paren {p \land \top} \lor \paren {p \land q}
      | c = Conjunction with Tautology
}}
{{eqn | r = p \land \paren {\top \lor q}
      | c = Conjunction is Left Distributive over Disjunction
}}
{{eqn | r = p \land \top
      | c = Disjunction with Tautology
}}
{{eqn | r = p
      | c = Conjunction with Tautology
}}
{{end-eqn}}
{{qed}}
Theorem: Absorption Laws (Logic)/Disjunction Absorbs Conjunction

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the appropriate truth values match for all boolean interpretations.
$\begin{array}{|ccccc||c|} \hline
p & \lor & (p & \land & q) & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F \\
\T & \T & \T & \F & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Extended Transitivity

Let $S$ be a set.
Let $\RR$ be a transitive relation on $S$.
Let $\RR^=$ be the reflexive closure of $\RR$.
Let $a, b, c \in S$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = \paren {a \mathrel \RR b} \land \paren {b \mathrel \RR c}
      | o = \implies
      | r = a \mathrel \RR c
}}
{{eqn | n = 2
      | l = \paren {a \mathrel \RR b} \land \paren {b \mathrel {\RR^=} c}
      | o = \implies
      | r = a \mathrel \RR c
}}
{{eqn | n = 3
      | l = \paren {a \mathrel {\RR^=} b} \land \paren {b \mathrel \RR c}
      | o = \implies
      | r = a \mathrel \RR c
}}
{{eqn | n = 4
      | l = \paren {a \mathrel {\RR^=} b} \land \paren {b \mathrel {\RR^=} c}
      | o = \implies
      | r = a \mathrel {\RR^=} c
}}
{{end-eqn}}

Proof:
$(1)$ follows from the definition of a transitive relation.
$(4)$ follows from Reflexive Closure of Transitive Relation is Transitive.
Suppose that:
:$\paren {a \mathrel \RR b} \land \paren {b \mathrel {\RR^=} c}$
By the definition of reflexive closure:
:$b \mathrel \RR c$ or $b = c$
If $b = c$, then since $a \mathrel \RR b$:
:$a \mathrel \RR c$
If $b \mathrel \RR c$ then by transitivity of $\RR$:
:$a \mathrel \RR c$
Thus $(2)$ holds.
A similar argument proves that $(3)$ holds as well:
Suppose that:
:$\paren {a \mathrel {\RR^=} b} \land \paren {b \mathrel \RR c}$
By the definition of reflexive closure:
:$a \mathrel \RR b$ or $a = b$
If $a = b$, then since $b \mathrel \RR c$:
:$a \mathrel \RR c$
If $a \mathrel \RR b$ then by transitivity of $\RR$:
:$a \mathrel \RR c$
Thus $(3)$ holds.
{{qed}}
Category:Transitive Relations
Category:Reflexive Closures
grgr98m0zamvw910geicyuj15dm47uy
Theorem: Rule of Idempotence/Conjunction

{{:Rule of Idempotence/Conjunction/Formulation 1}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for each boolean interpretations.
$\begin{array} {|c||ccc|} \hline
p & p & \land & p \\
\hline
\T & \T & \T & \T \\
\F & \F & \F & \F \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Idempotence/Disjunction

{{:Rule of Idempotence/Disjunction/Formulation 1}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for each boolean interpretations.
$\begin{array}{|c||ccc|} \hline
p & p & \lor & p \\
\hline
\T & \T & \T & \T \\
\F & \F & \F & \F \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Idempotence/Disjunction/Formulation 1/Forward Implication

:$p \vdash p \lor p$

Proof:
{{BeginTableau|p \vdash p \lor p}}
{{Premise|1|p}}
{{Addition|2|1|p \lor p|1|1}}
{{EndTableau|qed}}
Theorem: Rule of Idempotence/Disjunction/Formulation 1/Reverse Implication

:$p \lor p \vdash p$

Proof:
{{BeginTableau|p \lor p \vdash p}}
{{Premise|1|p \lor p}}
{{Assumption|2|p}}
{{ProofByCases|3|1|p|1|2|2|2|2}}
{{EndTableau|qed}}
Theorem: Rule of Idempotence/Disjunction/Formulation 1

:$p \dashv \vdash p \lor p$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for each boolean interpretations.
$\begin{array}{|c||ccc|} \hline
p & p & \lor & p \\
\hline
\T & \T & \T & \T \\
\F & \F & \F & \F \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Idempotence/Disjunction/Formulation 2

:$\vdash p \iff \paren {p \lor p}$

Proof:
{{BeginTableau       |p \iff \paren {p \lor p} }}
{{Assumption         | 1|     p}}
{{Addition           | 2|   1|p \lor p                    |1|1}}
{{Implication        | 3|    |p \implies \paren {p \lor p}|1|2}}
{{Assumption         | 4|     p \lor p}}
{{Assumption         | 5|     \neg p}}
{{ModusTollendoPonens| 6|4, 5|p                           |4|5|1}}
{{NonContradiction   | 7|4, 5|                             6|5}}
{{Contradiction      | 8|   5|p                           |5|7}}
{{Implication        | 9|    |\paren {p \lor p} \implies p|4|8}}
{{BiconditionalIntro |10|    |p \iff \paren {p \lor p}    |3|9}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Idempotence/Conjunction/Formulation 1/Forward Implication

:$p \vdash p \land p$

Proof:
{{BeginTableau|p \vdash p \land p}}
{{Premise|1|p}}
{{Conjunction|2|1|p \land q|1|1}}
{{EndTableau|qed}}
Category:Rule of Idempotence
dpjnyjtco9tniusxt10j76s1lzcf52l
Theorem: Rule of Idempotence/Conjunction/Formulation 1/Reverse Implication

:$p \land p \vdash p$

Proof:
{{BeginTableau|p \land p \vdash p}}
{{Premise|1|p \land p}}
{{Simplification|2|1|p|1|1}}
{{EndTableau|qed}}
Category:Rule of Idempotence
6ejt9d025qxqrds4cn8tiwy441h4fcc