avewright/proofwiki-math huggingface dataset:
Theorem: Exclusive Or as Disjunction of Conjunctions

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

Proof:
{{begin-eqn}}
{{eqn | l = p \oplus q
      | o = \dashv \vdash
      | r = \neg \left ({p \iff q}\right)
      | c = Exclusive Or is Negation of Biconditional
}}
{{eqn | o = \dashv \vdash
      | r = \left({\neg p \land q}\right) \lor \left({p \land \neg q}\right)
      | c = Non-Equivalence as Disjunction of Conjunctions
}}
{{end-eqn}}
{{qed}}
Theorem: Exclusive Or as Disjunction of Conjunctions

:$p \oplus q \dashv \vdash \paren {\neg p \land q} \lor \paren {p \land \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.
:<nowiki>$\begin {array} {|ccc||ccccccccc|} \hline
p & \oplus & q & (\neg & p & \land & q) & \lor & (p & \land & \neg & q) \\
\hline
\F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \F & \F & \T & \F & \F & \T & \T & \T & \T & \F \\
\T & \F & \T & \F & \T & \F & \T & \F & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Non-Equivalence as Disjunction of Negated Conditionals

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

Proof:
{{BeginTableau|\neg \paren {p \iff q} \vdash \neg \paren {p \implies q} \lor \neg \paren {q \implies p} }}
{{Premise|1|\neg \paren {p \iff q} }}
{{SequentIntro|2|1|\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|1
  |Rule of Material Equivalence}}
{{DeMorgan|3|1|\neg \paren {p \implies q} \lor \neg \paren {q \implies p}|2|Disjunction of Negations}}
{{EndTableau|lemma}}
{{BeginTableau|\neg \paren {p \implies q} \lor \neg \paren {q \implies p} \vdash \neg \paren {p \iff q} }}
{{Premise|1|\neg \paren {p \implies q} \lor \neg \paren {q \implies p} }}
{{DeMorgan|2|1|\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|1|Disjunction of Negations}}
{{SequentIntro|3|1|\neg \paren {p \iff q}|2|Rule of Material Equivalence}}
{{EndTableau}}
{{qed}}
Theorem: Non-Equivalence as Disjunction of Negated Conditionals

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

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}{|cccc||ccccccccc|} \hline
\neg & (p & \iff & q) & \neg & (p & \implies & q) & \lor & \neg & (q & \implies & p) \\
\hline
\F & \F & \T & \F & \F & \F & \T & \F & \F & \F & \F & \T & \F \\
\T & \F & \F & \T & \F & \F & \T & \T & \T & \T & \T & \F & \F  \\
\T & \T & \F & \F & \T & \T & \F & \F & \T & \F & \F & \T & \T  \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F & \T & \T & \T  \\
\hline
\end{array}$
{{qed}}
Theorem: Conjunction of Disjunction with Negation is Conjunction with Negation

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

Proof:
{{BeginTableau|p \land \neg q \vdash \paren {p \lor q} \land \neg q}}
{{Premise|1|p \land \neg q}}
{{Simplification|2|1|p|1|1}}
{{Addition|3|1|p \lor q|2|1}}
{{Simplification|4|1|\neg q|1|2}}
{{Conjunction|5|1|\paren {p \lor q} \land \neg q|3|4}}
{{EndTableau|lemma}}
and its converse:
{{BeginTableau|\paren {p \lor q} \land \neg q \vdash p \land \neg q}}
{{Premise|1|\paren {p \lor q} \land \neg q}}
{{SequentIntro|2|1|\paren {p \land \neg q} \lor \paren {q \land \neg q}|1|Conjunction Distributes over Disjunction}}
{{Assumption|3|q \land \neg q}}
{{NonContradiction|4|3|3|3}}
{{Contradiction|5||\neg \paren {q \land \neg q}|3|4}}
{{SequentIntro|6|1|p \land \neg q|2, 5|Disjunctive Syllogism}}
{{EndTableau|qed}}
Category:Conjunction
Category:Disjunction
Category:Logical Negation
ehpugt1xevdfp43z8vdzl4nga4slu25
Theorem: Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction

:$\neg \paren {p \iff q} \dashv \vdash \paren {p \lor q} \land \neg \paren {p \land q}$
That is, negation of the biconditional means the same thing as '''either-or but not both''', that is, exclusive or.

Proof:
{{BeginTableau|\neg \paren {p \iff q} \vdash \paren {p \lor q} \land \neg \paren {p \land q} }}
{{Premise|1|\neg \paren {p \iff q} }}
{{SequentIntro|2|1|\paren {\neg p \land q} \lor \paren {p \land \neg q}|1
  |Non-Equivalence as Disjunction of Conjunctions: Formulation 1
}}
{{Commutation|3|1|\paren {p \land \neg q} \lor \paren {\neg p \land q}|2|Disjunction}}
{{Commutation|4|1|\paren {p \land \neg q} \lor \paren {q \land \neg p}|3|Conjunction}}
{{SequentIntro|5|1
  |\paren {\paren {p \lor q} \land \neg q} \lor \paren {\paren {q \lor p} \land \neg p}
  |4
  |Conjunction of Disjunction with Negation is Conjunction with Negation
}}
{{Commutation|6|1
  |\paren {\paren {p \lor q} \land \neg q} \lor \paren {\paren {p \lor q} \land \neg p}
  |5|Disjunction}}
{{SequentIntro|7|1|\paren {p \lor q} \land \paren {\neg q \lor \neg p}|6
  |Conjunction Distributes over Disjunction
}}
{{Commutation|8|1|\paren {p \lor q} \land \paren {\neg p \lor \neg q}|7|Disjunction}}
{{DeMorgan|9|1|\paren {p \lor q} \land \neg \paren {\neg \neg p \land \neg \neg q}|8|Disjunction}}
{{DoubleNegElimination|10|1|\paren {p \lor q} \land \neg \paren {p \land q}|9}}
{{EndTableau}}
{{BeginTableau|\paren {p \lor q} \land \neg \paren {p \land q} \vdash \neg \paren {p \iff q} }}
{{Premise|1|\paren {p \lor q} \land \neg \paren {p \land q} }}
{{DeMorgan|2|1|\paren {p \lor q} \land \paren {\neg p \lor \neg q}|1|Disjunction of Negations}}
{{Commutation|3|1|\paren {p \lor q} \land \paren {\neg p \lor \neg q}|2|Disjunction}}
{{SequentIntro|4|1
  |\paren {\paren {p \lor q} \land \neg q} \lor \paren {\paren {p \lor q} \land \neg p}
  |3
  |Conjunction Distributes over Disjunction
}}
{{SequentIntro|5|1|\paren {p \land \neg q} \lor \paren {q \land \neg p}|4|Conjunction of Disjunction with Negation is Conjunction with Negation}}
{{Commutation|6|1|\paren {q \land \neg p} \lor \paren {p \land \neg q}|5|Disjunction}}
{{Commutation|7|1|\paren {\neg p \land q} \lor \paren {p \land \neg q}|6|Conjunction}}
{{SequentIntro|8|1|\neg \paren {p \iff q}|6|Non-Equivalence as Disjunction of Conjunctions: Formulation 1}}
{{EndTableau}}
{{qed}}
Theorem: Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction

:$\neg \paren {p \iff q} \dashv \vdash \paren {p \lor q} \land \neg \paren {p \land q}$
That is, negation of the biconditional means the same thing as '''either-or but not both''', that is, exclusive or.

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}{|cccc||cccccccc|} \hline
\neg & (p & \iff & q) & (p & \lor & q) & \land & \neg & (p & \land & q) \\
\hline
\F & \F & \T & \F & \F & \F & \F & \F & \T & \F & \F & \F \\
\T & \F & \F & \T & \F & \T & \T & \T & \T & \F & \F & \T  \\
\T & \T & \F & \F & \T & \T & \F & \T & \T & \T & \F & \F  \\
\F & \T & \T & \T & \T & \T & \T & \F & \F & \T & \T & \T  \\
\hline
\end{array}$
{{qed}}
Theorem: Non-Equivalence as Conjunction of Disjunction with Disjunction of Negations

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

Proof:
{{BeginTableau|\neg \paren {p \iff q} \vdash \paren {p \lor q} \land \paren {\neg p \lor \neg q} }}
{{Premise     |1|\neg \paren {p \iff q} }}
{{SequentIntro|2|1|\paren {p \lor q} \land \neg \paren {p \land q}|1|Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction}}
{{DeMorgan    |3|1|\paren {p \lor q} \land \paren {\neg p \lor \neg q}|2|Disjunction of Negations}}
{{EndTableau}}
{{BeginTableau|\paren {p \lor q} \land \paren {\neg p \lor \neg q} \vdash \neg \paren {p \iff q} }}
{{Premise     |1|\paren {p \lor q} \land \paren {\neg p \lor \neg q} }}
{{DeMorgan    |2|1|\paren {p \lor q} \land \neg \paren {p \land q}|1|Disjunction of Negations}}
{{SequentIntro|3|1|\neg \paren {p \iff q}|2|Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction}}
{{EndTableau|qed}}
Theorem: Non-Equivalence as Conjunction of Disjunction with Disjunction of Negations

:$\neg \paren {p \iff q} \dashv \vdash \paren {p \lor q} \land \paren {\neg p \lor \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}{|cccc||ccccccccc|} \hline
\neg & (p & \iff & q) & (p & \lor & q) & \land & (\neg & p & \lor & \neg & q) \\
\hline
\F & \F & \T & \F & \F & \F & \F & \F & \T & \F & \T & \T & \F \\
\T & \F & \F & \T & \F & \T & \T & \T & \T & \F & \T & \F & \T \\
\T & \T & \F & \F & \T & \T & \F & \T & \F & \T & \T & \T & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Inversion Mapping is Involution

Let $G$ be a group, and let $\iota: G \to G$ be the inversion mapping.
Then $\iota$ is an involution.
That is:
:$\forall g \in G: \map \iota {\map \iota g} = g$

Proof:
Let $g \in G$.
Then:
{{begin-eqn}}
{{eqn | l = \map \iota {\map \iota g}
      | r = \paren {g^{-1} }^{-1}
      | c = {{Defof|Inversion Mapping}}
}}
{{eqn | r = g
      | c = Inverse of Group Inverse
}}
{{end-eqn}}
which establishes the result.
{{qed}}
Category:Inversion Mappings
scu8viz33uzskvkzuh04emh1ycpbec3
Theorem: Order Isomorphism between Linearly Ordered Spaces is Homeomorphism

Let $\struct {S_1, \le_1, \tau_1}$ and $\struct {S_2, \le_2, \tau_2}$ be linearly ordered spaces.
Let $\phi: S_1 \to S_2$ be an order isomorphism from $\struct {S_1, \le_1}$ to $\struct {S_2, \le_2}$.
Then $\phi$ is a homeomorphism from $\struct {S_1, \tau_1}$ to $\struct {S_2, \tau_2}$.

Proof:
By the definition of order isomorphism, $\phi$ is a bijection.
Thus to show $\phi$ is a homeomorphism it remains to be shown that:
:$\phi$ is continuous
and:
:$\phi^{-1}$ is continuous.
First it is shown that $\phi^{-1}$ is continuous.
By Order Isomorphism Preserves Initial Segments and its dual, $\phi$ maps open rays in $\struct {S_1, \le_1}$ to open rays in $\struct {S_2, \le_2}$.
By Continuity Test using Sub-Basis, $\phi^{-1}$ is continuous.
Next it is shown that $\phi^{-1}$ is continuous.
By Inverse of Order Isomorphism is Order Isomorphism, $\phi^{-1}$ is an order isomorphism.
Applying the above shows that $\phi = \paren {\phi^{-1} }^{-1}$ is continuous.
Both $\phi$ and $\phi^{-1}$ have been shown to be continuous.
Thus, by definition, $\phi$ is a homeomorphism.
{{qed}}
Category:Linearly Ordered Spaces
dnyofjqvk2qgg6aiwah84iv1pyw9vl2
Theorem: Rule of Association/Conjunction

Conjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Conjunction/Formulation 2}}

Proof:
{{BeginTableau|p \land \paren {q \land r} \vdash \paren {p \land q} \land r}}
{{Premise|1|p \land \paren {q \land r} }}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|q \land r|1|2}}
{{Simplification|4|1|q|3|1}}
{{Simplification|5|1|r|3|2}}
{{Conjunction|6|1|p \land q|2|4}}
{{Conjunction|7|1|\paren {p \land q} \land r|6|5}}
{{EndTableau}}
{{BeginTableau|\paren {p \land q} \land r \vdash p \land \paren {q \land r} }}
{{Premise|1|\paren {p \land q} \land r}}
{{Simplification|2|1|p \land q|1|1}}
{{Simplification|3|1|r|1|2}}
{{Simplification|4|1|p|2|1}}
{{Simplification|5|1|q|2|2}}
{{Conjunction|6|1|q \land r|5|3}}
{{Conjunction|7|1|p \land \paren {q \land r}|4|6}}
{{EndTableau|qed}}
Theorem: Rule of Association/Conjunction

Conjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Conjunction/Formulation 2}}

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}{|ccccc||ccccc|} \hline
p & \land & (q & \land & r) & (p & \land & q) & \land & r \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F & \F & \F & \F & \T \\
\F & \F & \T & \F & \F & \F & \F & \T & \F & \F \\
\F & \F & \T & \T & \T & \F & \F & \T & \F & \T \\
\T & \F & \F & \F & \F & \T & \F & \F & \F & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Association/Conjunction

Conjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Conjunction/Formulation 2}}

Proof:
=== Forward Implication ===
{{:Rule of Association/Conjunction/Formulation 2/Proof 1/Forward Implication}}
=== Reverse Implication ===
{{:Rule of Association/Conjunction/Formulation 2/Proof 1/Reverse Implication}}
{{BeginTableau|\vdash \paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r} }}
{{TheoremIntro|1|\paren {p \land \paren {q \land r} } \implies \paren {\paren {p \land q} \land r}|Forward Implication}}
{{TheoremIntro|2|\paren {p \land \paren {q \land r} } \impliedby \paren {\paren {p \land q} \land r}|Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r}|1|2}}
{{EndTableau|qed}}
Theorem: Rule of Association/Conjunction

Conjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Conjunction/Formulation 2}}

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

Disjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Disjunction/Formulation 2}}

Proof:
{{BeginTableau|p \lor \paren {q \lor r} \vdash \paren {p \lor q} \lor r}}
{{Premise|1|p \lor \paren {q \lor r} }}
{{Assumption|2|p|By assuming the first main disjunct ...}}
{{Addition|3|2|p \lor q|2|1}}
{{Addition|4|2|\paren {p \lor q} \lor r|3|1|... the conclusion is derived}}
{{Assumption|5|q \lor r|Then assume the second main disjunct ...}}
{{Assumption|6|q|... and by assuming the first disjunct of that second main disjunct ...}}
{{Addition|7|6|p \lor q|6|2}}
{{Addition|8|6|\paren {p \lor q} \lor r|7|1|... the conclusion is derived}}
{{Assumption|9|r|Then assume the second disjunct of that second main disjunct ...}}
{{Addition|10|9|\paren {p \lor q} \lor r|9|2|... and likewise the same conclusion is derived}}
{{ProofByCases|11|5|\paren {p \lor q} \lor r|5|6|8|9|10}}
{{ProofByCases|12|1|\paren {p \lor q} \lor r|1|2|4|5|11}}
{{EndTableau|lemma}}
{{BeginTableau|\paren {p \lor q} \lor r \vdash p \lor \paren {q \lor r} }}
{{Premise|1|\paren {p \lor q} \lor r}}
{{Assumption|2|p \lor q}}
{{Assumption|3|p}}
{{Addition|4|3|p \lor \paren {q \lor r}|3|1}}
{{Assumption|5|q}}
{{Addition|6|5|q \lor r|5|1}}
{{Addition|7|5|p \lor \paren {q \lor r}|6|2}}
{{ProofByCases|8|2|p \lor \paren {q \lor r}|2|3|4|5|7}}
{{Assumption|9|r}}
{{Addition|10|9|q \lor r|9|2}}
{{Addition|11|9|p \lor \paren {q \lor r}|10|2}}
{{ProofByCases|12|1|p \lor \paren {q \lor r}|1|2|8|9|11}}
{{EndTableau|qed}}
Theorem: Rule of Association/Disjunction

Disjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Disjunction/Formulation 2}}

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}{|ccccc||ccccc|} \hline
p & \lor & (q & \lor & r) & (p & \lor & q) & \lor & r \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \T & \F & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \T & \T & \F & \F & \T & \T & \T & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \F & \F & \F & \T & \T & \F & \T & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Association/Disjunction

Disjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Disjunction/Formulation 2}}

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

Disjunction is associative:
=== Formulation 1 ===
{{:Rule of Association/Disjunction/Formulation 1}}
=== Formulation 2 ===
{{:Rule of Association/Disjunction/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = \paren {p \lor \paren {q \lor r} } \implies \paren {\paren {p \lor q} \lor r}
 | rlnk = Rule of Association/Disjunction/Formulation 2/Forward Implication
 | rtxt = Rule of Association: Forward Implication
}}
{{TableauLine
 | n = 2
 | f = \paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} }
 | rlnk = Rule of Association/Disjunction/Formulation 2/Reverse Implication
 | rtxt = Rule of Association: Reverse Implication
}}
{{TableauLine
 | n = 3
 | f = \paren {\paren {p \lor \paren {q \lor r} } \implies \paren {\paren {p \lor q} \lor r} } \land \paren {\paren {\paren {p \lor q} \lor r} \implies \paren {p \lor \paren {q \lor r} } }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 4$
 | dep  = 1, 2
}}
{{TableauLine
 | n = 4
 | f = \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 2 (3)$
 | dep  = 3
}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Association/Conjunction/Formulation 1

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

Proof:
{{BeginTableau|p \land \paren {q \land r} \vdash \paren {p \land q} \land r}}
{{Premise|1|p \land \paren {q \land r} }}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|q \land r|1|2}}
{{Simplification|4|1|q|3|1}}
{{Simplification|5|1|r|3|2}}
{{Conjunction|6|1|p \land q|2|4}}
{{Conjunction|7|1|\paren {p \land q} \land r|6|5}}
{{EndTableau}}
{{BeginTableau|\paren {p \land q} \land r \vdash p \land \paren {q \land r} }}
{{Premise|1|\paren {p \land q} \land r}}
{{Simplification|2|1|p \land q|1|1}}
{{Simplification|3|1|r|1|2}}
{{Simplification|4|1|p|2|1}}
{{Simplification|5|1|q|2|2}}
{{Conjunction|6|1|q \land r|5|3}}
{{Conjunction|7|1|p \land \paren {q \land r}|4|6}}
{{EndTableau|qed}}
Theorem: Rule of Association/Conjunction/Formulation 1

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

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}{|ccccc||ccccc|} \hline
p & \land & (q & \land & r) & (p & \land & q) & \land & r \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F & \F & \F & \F & \T \\
\F & \F & \T & \F & \F & \F & \F & \T & \F & \F \\
\F & \F & \T & \T & \T & \F & \F & \T & \F & \T \\
\T & \F & \F & \F & \F & \T & \F & \F & \F & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Association/Disjunction/Formulation 1

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

Proof:
{{BeginTableau|p \lor \paren {q \lor r} \vdash \paren {p \lor q} \lor r}}
{{Premise|1|p \lor \paren {q \lor r} }}
{{Assumption|2|p|By assuming the first main disjunct ...}}
{{Addition|3|2|p \lor q|2|1}}
{{Addition|4|2|\paren {p \lor q} \lor r|3|1|... the conclusion is derived}}
{{Assumption|5|q \lor r|Then assume the second main disjunct ...}}
{{Assumption|6|q|... and by assuming the first disjunct of that second main disjunct ...}}
{{Addition|7|6|p \lor q|6|2}}
{{Addition|8|6|\paren {p \lor q} \lor r|7|1|... the conclusion is derived}}
{{Assumption|9|r|Then assume the second disjunct of that second main disjunct ...}}
{{Addition|10|9|\paren {p \lor q} \lor r|9|2|... and likewise the same conclusion is derived}}
{{ProofByCases|11|5|\paren {p \lor q} \lor r|5|6|8|9|10}}
{{ProofByCases|12|1|\paren {p \lor q} \lor r|1|2|4|5|11}}
{{EndTableau|lemma}}
{{BeginTableau|\paren {p \lor q} \lor r \vdash p \lor \paren {q \lor r} }}
{{Premise|1|\paren {p \lor q} \lor r}}
{{Assumption|2|p \lor q}}
{{Assumption|3|p}}
{{Addition|4|3|p \lor \paren {q \lor r}|3|1}}
{{Assumption|5|q}}
{{Addition|6|5|q \lor r|5|1}}
{{Addition|7|5|p \lor \paren {q \lor r}|6|2}}
{{ProofByCases|8|2|p \lor \paren {q \lor r}|2|3|4|5|7}}
{{Assumption|9|r}}
{{Addition|10|9|q \lor r|9|2}}
{{Addition|11|9|p \lor \paren {q \lor r}|10|2}}
{{ProofByCases|12|1|p \lor \paren {q \lor r}|1|2|8|9|11}}
{{EndTableau|qed}}
Theorem: Rule of Association/Disjunction/Formulation 1

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

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}{|ccccc||ccccc|} \hline
p & \lor & (q & \lor & r) & (p & \lor & q) & \lor & r \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \T & \F & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \T & \T & \F & \F & \T & \T & \T & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \F & \F & \F & \T & \T & \F & \T & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Association/Conjunction/Formulation 1/Proof 1

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

Proof:
{{BeginTableau|p \land \paren {q \land r} \vdash \paren {p \land q} \land r}}
{{Premise|1|p \land \paren {q \land r} }}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|q \land r|1|2}}
{{Simplification|4|1|q|3|1}}
{{Simplification|5|1|r|3|2}}
{{Conjunction|6|1|p \land q|2|4}}
{{Conjunction|7|1|\paren {p \land q} \land r|6|5}}
{{EndTableau}}
{{BeginTableau|\paren {p \land q} \land r \vdash p \land \paren {q \land r} }}
{{Premise|1|\paren {p \land q} \land r}}
{{Simplification|2|1|p \land q|1|1}}
{{Simplification|3|1|r|1|2}}
{{Simplification|4|1|p|2|1}}
{{Simplification|5|1|q|2|2}}
{{Conjunction|6|1|q \land r|5|3}}
{{Conjunction|7|1|p \land \paren {q \land r}|4|6}}
{{EndTableau|qed}}