avewright/proofwiki-math huggingface dataset:
Theorem: Existence of Rational Powers of Irrational Numbers

There exist irrational numbers $a$ and $b$ such that $a^b$ is rational.

Proof:
Given that $2$ is rational and $\sqrt 2$ is irrational, consider the number $q = \sqrt 2^{\sqrt 2}$.
We consider the two cases.
:$(1): \quad$ If $q$ is rational then $a = \sqrt 2$ and $b = \sqrt 2$ are the desired irrational numbers.
:$(2): \quad$ If $q$ is irrational then $q^{\sqrt 2} = \paren {\sqrt 2^{\sqrt 2} }^{\sqrt 2} = \sqrt 2^{\paren {\sqrt 2} \paren {\sqrt 2} } = \sqrt 2^2 = 2$ is rational, so $a = q = \sqrt 2^{\sqrt 2}$ and $b = \sqrt 2$ are the desired irrational numbers.
{{qed}}
Theorem: Existence of Rational Powers of Irrational Numbers

There exist irrational numbers $a$ and $b$ such that $a^b$ is rational.

Proof:
Consider the equation:
:$\paren {\sqrt 2}^{\log_{\sqrt 2} 3} = 3$
We have that $\sqrt 2$ is irrational and $3$ is (trivially) rational.
It remains to be proved $\log_{\sqrt 2} 3$ is irrational.
We have:
{{begin-eqn}}
{{eqn | l = \log_{\sqrt 2} 3
      | r = \frac {\log_2 3} {\log_2 \sqrt 2}
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac {\log_2 3} {1/2}
      | c = Logarithms of Powers: $\sqrt 2 = 2^{1/2}$ and $\log_2 2 = 1$
}}
{{eqn | r = 2 \, \log_2 3
      | c = 
}}
{{end-eqn}}
From Irrationality of Logarithm, $\log_2 3$ is irrational.
Therefore $2 \, \log_2 3$ is irrational.
Thus there exist two irrational numbers $a = \sqrt 2$ and $b = \log_{\sqrt 2} 3$ such that $a^b$ is rational.
{{qed}}
Theorem: Intersection is Associative

Set intersection is associative:
:$A \cap \paren {B \cap C} = \paren {A \cap B} \cap C$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in A \cap \paren {B \cap C}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A \land \paren {x \in B \land x \in C}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in A \land x \in B} \land x \in C
      | c = Rule of Association: Conjunction
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {A \cap B} \cap C
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
Therefore:
:$x \in A \cap \paren {B \cap C}$ {{iff}} $x \in \paren {A \cap B} \cap C$
Thus it has been shown that:
:$A \cap \paren {B \cap C}\ = \paren {A \cap B} \cap C$
{{qed}}
Theorem: Intersection is Associative

Set intersection is associative:
:$A \cap \paren {B \cap C} = \paren {A \cap B} \cap C$

Proof:
For every $\lambda \in \Lambda$, let $\ds T_\lambda = \bigcap_{i \mathop \in I_\lambda} S_i$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = S_i
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \lambda \in \Lambda: \forall i \in I_\lambda
      | l = x
      | o = \in
      | r = S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \lambda \in \Lambda
      | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I_\lambda} S_i = T_\lambda
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{\lambda \mathop \in \Lambda} T_\lambda
      | c = 
}}
{{end-eqn}}
Thus:
:$\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{\lambda \mathop \in \Lambda} T_\lambda = \bigcap_{\lambda \mathop \in \Lambda} \paren {\bigcap_{i \mathop \in I_\lambda} S_i}$
{{qed}}
Theorem: Intersection is Associative

Set intersection is associative:
:$A \cap \paren {B \cap C} = \paren {A \cap B} \cap C$

Proof:
{{begin-eqn}}
{{eqn | l = \bigcap_{i \mathop \in I} S_i
      | r = \map \complement {\map \complement {\bigcap_{i \mathop \in I} S_i} }
      | c = Complement of Complement
}}
{{eqn | r = \map \complement {\bigcup_{i \mathop \in I} \map \complement {S_i} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\bigcup_{\lambda \mathop \in \Lambda} \paren {\bigcup_{i \mathop \in I_\lambda} \map \complement {S_i} } }
      | c = General Associativity of Set Union
}}
{{eqn | r = \map \complement {\bigcup_{\lambda \mathop \in \Lambda} \paren {\map \complement {\bigcap_{i \mathop \in I_\lambda} S_i} } }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \bigcap_{\lambda \mathop \in \Lambda} \paren {\map \complement {\map \complement {\bigcap_{i \mathop \in I_\lambda} S_i} } }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Union
}}
{{eqn | r = \bigcap_{\lambda \mathop \in \Lambda} \paren {\bigcap_{i \mathop \in I_\lambda} S_i}
      | c = Complement of Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Center of Symmetric Group is Trivial

Let $n \in \N$ be a natural number.
Let $S_n$ denote the symmetric group of order $n$.
Let $n \ge 3$.
Then the center $\map Z {S_n}$ of $S_n$ is trivial.

Proof:
From its definition, the identity (here denoted by $e$) of a group $G$ commutes with all elements of $G$.
So by definition of center:
:$e \in \map Z {S_n}$
By definition of center:
:$\map Z {S_n} = \set {\tau \in S_n: \forall \sigma \in S_n: \tau \sigma = \sigma \tau}$
Let $\pi, \rho \in S_n$ be permutations of $\N_n$.
Let us choose an arbitrary $\pi \in S_n: \pi \ne e, \map \pi i = j, i \ne j$.
Since $n \ge 3$, we can find $\rho \in S_n$ which interchanges $j$ and $k$ (where $k \ne i, j$) and fixes everything else.
It follows that $\rho^{-1}$ does the same thing, and in particular both $\rho$ and $\rho^{-1}$ fix $i$.
So:
{{begin-eqn}}
{{eqn | l = \map {\rho \pi \rho^{-1} } i
      | r = \map {\rho \pi} i
      | c = 
}}
{{eqn | r = \map \rho j
      | c = 
}}
{{eqn | r = k
      | c = 
}}
{{end-eqn}}
So:
:$\map {\rho \pi \rho^{-1} } i = k \ne j = \map \pi i$
From Conjugate of Commuting Elements, if $\rho$ and $\pi$ were to commute, $\rho \pi \rho^{-1} = \pi$.
But they don't.
Whatever $\pi \in S_n$ is, you can ''always'' find a $\rho$ such that $\rho \pi \rho^{-1} \ne \pi$.
So no non-identity elements of $S_n$ commute with all elements of $S_n$.
Hence:
:$\map Z {S_n} = \set e$
{{Qed}}
Theorem: Center of Symmetric Group is Trivial

Let $n \in \N$ be a natural number.
Let $S_n$ denote the symmetric group of order $n$.
Let $n \ge 3$.
Then the center $\map Z {S_n}$ of $S_n$ is trivial.

Proof:
Let $\pi \in S_n$ such that $\pi \ne e$ be arbitrary.
Let $i, j \in \set {1, 2, \ldots, n}$ such that $\map \pi i = j \ne i$.
Let $m = \map \pi j$.
Then $m \ne j$.
Since $n \ge 3$, there exists $k \in \N$ such that $k \ne j, k \ne m$.
Let $\rho \in S_n$ interchange $j, k$ and fix everything else.
Then $\rho$ fixes $m$.
Then:
{{begin-eqn}}
{{eqn | q = 
      | l = \map {\rho \pi} j
      | r = \map \rho m
      | c = 
}}
{{eqn | r = m
      | c = 
}}
{{eqn | r = \map \pi j
      | c = 
}}
{{end-eqn}}
By definition of $\rho$:
:$k = \map \rho j$
So:
:$\map \pi k = \map {\pi \rho} j$
But because permutations are injective:
:$\map \pi j \ne \map \pi k$
Thus:
:$\map {\rho \pi} j \ne \map {\pi \rho} j$
That is, there exists a $\rho$ with which $\pi$ does not commute.
So $\pi \notin \map Z {S_n}$.
As $\pi \ne e$ is arbitrary, it follows that only $e$ is in $\map Z {S_n}$.
That is:
:$\map Z {S_n} = \set e$
Hence, by definition, $\map Z {S_n}$ is trivial.
{{Qed}}
Theorem: Square Root of 2 is Irrational

:$\sqrt 2$ is irrational.

Proof:
First we note that, from Parity of Integer equals Parity of its Square, if an integer is even, its square root, if an integer, is also even.
Thus it follows that:
:$(1): \quad 2 \divides p^2 \implies 2 \divides p$
where $2 \divides p$ indicates that $2$ is a divisor of $p$.
{{AimForCont}} that $\sqrt 2$ is rational.
So:
:$\sqrt 2 = \dfrac p q$
for some $p, q \in \Z$, and:
:$(2): \quad \gcd \set {p, q} = 1$
where $\gcd$ denotes the greatest common divisor.
Squaring both sides yields:
:$2 = \dfrac {p^2} {q^2} \iff p^2 = 2 q^2$
Therefore from $(1)$:
:$2 \divides p^2 \implies 2 \divides p$
That is, $p$ is an even integer.
So $p = 2 k$ for some $k \in \Z$.
Thus:
:$2 q^2 = p^2 = \paren {2 k}^2 = 4 k^2 \implies q^2 = 2 k^2$
so by the same reasoning:
:$2 \divides q^2 \implies 2 \divides q$
This contradicts our deduction $(2)$ that $\gcd \set {p, q} = 1$, since $2 \divides p, q$.
Therefore, from Proof by Contradiction, $\sqrt 2$ cannot be rational.
{{qed}}
Theorem: Square Root of 2 is Irrational

:$\sqrt 2$ is irrational.

Proof:
Special case of Square Root of Prime is Irrational.
{{qed}}
Theorem: Square Root of 2 is Irrational

:$\sqrt 2$ is irrational.

Proof:
{{AimForCont}} that $\sqrt 2$ is rational.
Then $\sqrt 2 = \dfrac p q$ for some $p, q \in \Z_{>0}$
Consider the quantity $\paren {\sqrt 2 - 1}$:
{{begin-eqn}}
{{eqn | ll= 1
      | l = <
      | o = \sqrt 2
      | r = <
      | rr = 2
      | c = Ordering of Squares in Reals
}}
{{eqn | lll = \leadsto
      | ll= 0
      | l = <
      | o = \sqrt 2 - 1
      | r = <
      | rr = 1
}}
{{end-eqn}}
Now, observe that for any $n \in \Z_{>0}$:
{{begin-eqn}}
{{eqn | l = \paren {\sqrt 2 - 1}^n
      | r = \sum_{k \mathop = 0}^n \binom n k \paren {\sqrt 2}^k \paren {-1}^{n-k}
      | c = Binomial Theorem
}}
{{eqn | r = \sum_{\substack {0 \mathop \le k \mathop \le n \\ k \, \text{even} } } \binom n k 2^{k/2} \paren {-1}^{n - k} + \sqrt 2 \sum_{\substack {0 \mathop \le k \mathop \le n \\ k \, \text{odd} } } \binom n k 2^{\paren {k - 1}/2} \paren {-1}^{n-k}
}}
{{eqn | r = a_n + b_n \sqrt 2
      | c = for some integers $a_n, b_n$
}}
{{eqn | r = a_n + b_n \paren {\frac p q}
      | c = recalling the assumption that $\sqrt 2 = \dfrac p q$
}}
{{eqn | r = \frac {a_n q + b_n p} q
}}
{{eqn | o = \ge
      | r = \frac 1 q
      | c = as the numerator is an integer and $\sqrt 2 - 1 > 0$
}}
{{end-eqn}}
By Sequence of Powers of Number less than One:
:$\ds \lim_{n \mathop \to \infty} \paren {\sqrt 2 - 1}^n = 0$
where $\lim$ denotes limit.
Recall the definition of $a_n$ and $b_n$.
By Lower and Upper Bounds for Sequences:
:$0 = \ds \lim_{n \mathop \to \infty} \frac {a_n q + b_n p} q \ge \frac 1 q$
which is a contradiction.
{{qed}}
Theorem: Square Root of 2 is Irrational

:$\sqrt 2$ is irrational.

Proof:
{{AimForCont}} that $\sqrt 2$ is rational.
Let $n$ be the smallest positive integer such that:
:$\sqrt 2 = \dfrac m n$
for some $m \in \Z_{>0}$
Then:
:$m = n \sqrt2 > n$
so:
:$(1): \quad m - n > 0$
We also have:
:$m = n \sqrt2 < 2 n$
so:
:$m < 2 n$
and therefore:
:$(2): \quad m - n < n$
Finally, we have
{{begin-eqn}}
{{eqn | l = m^2
      | r = 2 n^2
}}
{{eqn | ll= \leadsto
      | l = m^2 - n m 
      | r = 2 n^2 - n m
}}
{{eqn | ll= \leadsto
      | l = m \paren {m - n} 
      | r = \paren {2 n - m} n
}}
{{eqn | ll= \leadsto
      | l = \dfrac {2 n - m} {m - n} 
      | r = \dfrac m n
}}
{{end-eqn}}
It follows that:
:$\dfrac {2 n - m} {m - n} = \sqrt2$
By $(1)$, the denominator of $\dfrac {2 n - m} {m - n}$ is positive.
By $(2)$, the denominator of $\dfrac {2 n - m} {m - n}$ is less than $n$.
We have thus written $\sqrt2$ as a fraction with a smaller denominator than $n$.
This contradicts our assertion that $n$ is the smallest denominator of $\sqrt 2 = \dfrac m n$.
Hence the result by Proof by Contradiction
{{qed}}
Theorem: Square Root of 2 is Irrational

:$\sqrt 2$ is irrational.

Proof:
By the Rational Root Theorem, every rational root of the polynomial $n^2 - 2$ would have:
:a numerator that divides $2$
and:
:a denominator that divides $1$.
That is, the only possible rational roots are:
:$n = \pm 1, \pm 2$
But:
:$\paren {\pm 1}^2 - 2 \ne 0 \ne \paren {\pm 2}^2 - 2$
So its root $n = \sqrt 2$ is not a rational number.
{{qed}}
Theorem: Empty Set is Unique

The empty set is unique.

Proof:
Let $\O$ and $\O'$ both be empty sets.
From Empty Set is Subset of All Sets, $\O \subseteq \O'$, because $\O$ is empty.
Likewise, we have $\O' \subseteq \O$, since $\O'$ is empty.
Together, by the definition of set equality, this implies that $\O = \O'$.
Thus there is only one empty set.
{{Qed}}
Theorem: Empty Set is Unique

The empty set is unique.

Proof:
Let $A$ and $B$ both be empty sets.
Thus:
:$\forall x: \neg \paren {x \in A}$
and:
:$\forall x: \neg \paren {x \in B}$
Hence:
:$x \notin A \iff x \notin B$
and so:
:$x \in A \iff x \in B$
vacuously.
From the Axiom of Extension:
:$\forall x: \paren {x \in A \iff x \in B} \iff A = B$
Hence the result.
{{Qed}}
Theorem: Empty Set is Unique

The empty set is unique.

Proof:
From {{axiom-link|the Empty Set|Class Theory}} in the context of class theory, the empty class is a set.
The result follows from Empty Class Exists and is Unique.
{{Qed}}
Theorem: Principle of Non-Contradiction

The '''Principle of Non-Contradiction''' is a valid argument in types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
{{:Principle of Non-Contradiction/Proof Rule}}
=== Sequent Form ===
{{:Principle of Non-Contradiction/Sequent Form}}

Proof:
{{BeginTableau|p, \neg p \vdash \bot}}
{{Premise|1|p}}
{{Premise|2|\neg p}}
{{NonContradiction|3|1, 2|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Principle of Non-Contradiction

The '''Principle of Non-Contradiction''' is a valid argument in types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
{{:Principle of Non-Contradiction/Proof Rule}}
=== Sequent Form ===
{{:Principle of Non-Contradiction/Sequent Form}}

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin {array} {|cccc||c|} \hline
p & \land & \neg & p & \bot \\
\hline
\F & \F & \T & \F & \F \\
\T & \F & \F & \T & \F \\
\hline
\end {array}$</nowiki>
As can be seen by inspection, the truth value of the main connective, that is $\land$, is $F$ for each boolean interpretation for $p$.
{{qed}}
Theorem: Principle of Non-Contradiction

The '''Principle of Non-Contradiction''' is a valid argument in types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
{{:Principle of Non-Contradiction/Proof Rule}}
=== Sequent Form ===
{{:Principle of Non-Contradiction/Sequent Form}}

Proof:
{{BeginTableau|\vdash \neg \left({p \land \neg p}\right)}}
{{Assumption|1|p \land \neg p}}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|\neg p|1|2}}
{{NonContradiction|4|1|2|3}}
{{Contradiction|5||\neg \left({p \land \neg p}\right)|1|4}}
{{EndTableau|qed}}
Theorem: Principle of Non-Contradiction

The '''Principle of Non-Contradiction''' is a valid argument in types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
{{:Principle of Non-Contradiction/Proof Rule}}
=== Sequent Form ===
{{:Principle of Non-Contradiction/Sequent Form}}

Proof:
We apply the Method of Truth Tables to the proposition $\neg \paren {p \land \neg p}$.
As can be seen by inspection, the truth value of the main connective, that is $\neg$, is $T$ for each boolean interpretation for $p$.
:<nowiki>$\begin {array} {|ccccc|} \hline
\neg & (p & \land & \neg & p)\\
\hline
\T & \F & \F & \T & \F \\
\T & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Substitution

Let $S$ be a sequent of propositional logic that has been proved.
Then we may infer any sequent $S'$ resulting from $S$ by substitutions for letters.

Proof:
This is apparent from inspection of the proof rules themselves.
The rules concern only the broad structure of the propositional formulas involved, and this structure is unaffected by substitution of letters.
By performing the substitutions systematically throughout the given sequent, all applications of proof rules remain correct applications in the sequent.
{{Handwaving}}
Theorem: Rule of Sequent Introduction

Let the statements $P_1, P_2, \ldots, P_n$ be conclusions in a proof, on various assumptions.
Let $P_1, P_2, \ldots, P_n \vdash Q$ be a sequent for which we already have a proof.
Then we may infer, at any stage of a proof (citing '''SI'''), the conclusion $Q$ of the sequent already proved.
This conclusion depends upon the pool of assumptions upon which $P_1, P_2, \ldots, P_n$ rest.
This is called the '''rule of sequent introduction'''.

Proof:
By hypothesis we have a proof of:
:$P_1, P_2, \ldots, P_n \vdash Q$
Therefore we can include this proof in our current proof and arrive at $Q$ with the pool of assumptions upon which $P_1, P_2, \ldots, P_n$ rest.
{{qed}}
Theorem: Law of Identity

Every proposition entails itself:
=== Formulation 1 ===
{{:Law of Identity/Formulation 1}}
=== Formulation 2 ===
{{:Law of Identity/Formulation 2}}

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

Every proposition entails itself:
=== Formulation 1 ===
{{:Law of Identity/Formulation 1}}
=== Formulation 2 ===
{{:Law of Identity/Formulation 2}}

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

Every proposition entails itself:
=== Formulation 1 ===
{{:Law of Identity/Formulation 1}}
=== Formulation 2 ===
{{:Law of Identity/Formulation 2}}

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

Every proposition entails itself:
=== Formulation 1 ===
{{:Law of Identity/Formulation 1}}
=== Formulation 2 ===
{{:Law of Identity/Formulation 2}}

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

Every proposition entails itself:
=== Formulation 1 ===
{{:Law of Identity/Formulation 1}}
=== Formulation 2 ===
{{:Law of Identity/Formulation 2}}

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: Rule of Idempotence

The '''rule of idempotence''' is two-fold:
=== Conjunction ===
{{:Rule of Idempotence/Conjunction}}
=== Disjunction ===
{{:Rule of Idempotence/Disjunction}}

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

The '''rule of idempotence''' is two-fold:
=== Conjunction ===
{{:Rule of Idempotence/Conjunction}}
=== Disjunction ===
{{:Rule of Idempotence/Disjunction}}

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: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
{{BeginTableau|\vdash p \implies q, q \implies r \vdash p \implies r}}
{{Premise|1|p \implies q}}
{{Premise|2|q \implies r}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{Implication|6|1, 2|p \implies r|3|5}}
{{EndTableau}}
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
This proof uses $\mathscr H_2$, Instance 2 of the Hilbert proof systems.
Recall the sequent form of the Hypothetical Syllogism:
:$\vdash \paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }$
Applying the Rule of Detachment $\text {RST} 3$ twice, we obtain:
:$\vdash \paren {p \implies q} \implies \paren {p \implies r}$
and subsequently:
:$\vdash p \implies r$
as desired.
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
We apply the Method of Truth Tables to the propositions in turn.
As can be seen for all boolean interpretations by inspection, where the truth values under the main connective on the {{LHS}} is $\T$, that under the one on the {{RHS}} is also $\T$:
:<nowiki>$\begin{array}{|ccccccc||ccc|} \hline
(p & \implies & q) & \land & (q & \implies & r) & p & \implies & r \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \T & \F \\
\F & \T & \F & \T & \F & \T & \T & \F & \T & \T \\
\F & \T & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \F & \F \\
\T & \F & \F & \F & \F & \T & \T & \T & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
Hence the result.
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
{{BeginTableau|p \implies q, q \implies r, p \vdash r}}
{{Premise|1|p \implies q}}
{{Premise|2|q \implies r}}
{{Premise|3|p}}
{{SequentIntro|4|1, 2|p \implies r|1, 2|Hypothetical Syllogism: Formulation 1}}
{{ModusPonens|5|1, 2, 3|r|4|3}}
{{EndTableau}}
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
{{BeginTableau|p \implies q, q \implies r, p \vdash r}}
{{Premise|1|p \implies q}}
{{Premise|2|q \implies r}}
{{Premise|3|p}}
{{ModusPonens|4|1, 3|q|1|3}}
{{ModusPonens|5|1, 2, 3|r|2|4}}
{{EndTableau}}
{{qed}}