nyuuzyou/wikis huggingface dataset:
Between two Real Numbers exists Rational Number/Proof 1

== Theorem ==
== Proof ==
Suppose that $a \ge 0$.
As $a < b$ it follows that $a \ne b$ and so $b - a \ne 0$.
Thus:
:$\dfrac 1 {b - a} \in \R$
By the Axiom of Archimedes:
:$\exists n \in \N: n > \dfrac 1 {b - a}$
Let $M := \set {x \in \N: \dfrac x n > a}$.
By the Well-Ordering Principle, there exists $m \in \N$ such that $m$ is the smallest element of $M$.
That is:
:$m > a n$
and, by definition of smallest element:
:$m - 1 \le a n$
As $n > \dfrac 1 {b - a}$, it follows from Ordering of Reciprocals that:
:$\dfrac 1 n < b - a$
Thus:
Thus we have shown that $a < \dfrac m n < b$.
That is:
: $\exists r \in \Q: a < r < b$
such that $r = \dfrac m n$.
Now suppose $a < 0$.
If $b > 0$ then $0 = r$ is a rational number such that $a < r < b$.
Otherwise we have $a < b \le 0$.
Then $0 \le -b < -a$ and there exists $r \in \Q$ such that:
:$-b < r < -a$
where $r$ can be found as above.
That is:
:$a < -r < b$
All cases have been covered, and the result follows.
== Historical Note ==
== Sources ==
* : $1$: Review of some real analysis: $\S 1.1$: Real Numbers: Corollary $1.1.7$
Category:Between two Real Numbers exists Rational Number
Between two Real Numbers exists Rational Number/Proof 1/Historical Note

== Historical Note on Proof 1 of Between two Real Numbers exists Rational Number ==
When this proof was first published in , there was a mistake in it:
:
This was corrected in the second printing, along with an apologetic note:
;Preface to reprinted edition
:I am grateful to all who have pointed out errors in the first printing (even to those who mentioned that the proof of Corollary 1.1.7purported to establish the existence of a positive rational number between any two real numbers). In particular ...
Category:Historical Notes
Between two Real Numbers exists Rational Number/Proof 2

== Theorem ==
== Proof ==
As $a < b$ it follows that $a \ne b$ and so $b - a \ne 0$.
Thus:
:$\dfrac 1 {b - a} \in \R$
By the Axiom of Archimedes:
:$\exists n \in \N: n > \dfrac 1 {b - a}$
Let $M := \set {x \in \Z: x > a n}$.
By Set of Integers Bounded Below has Smallest Element, there exists $m \in \Z$ such that $m$ is the smallest element of $M$.
That is:
:$m > a n$
and, by definition of smallest element:
:$m - 1 \le a n$
As $n > \dfrac 1 {b - a}$, it follows from Ordering of Reciprocals that:
:$\dfrac 1 n < b - a$
Thus:
Thus we have shown that $a < \dfrac m n < b$.
That is:
:$\exists r \in \Q: a < r < b$
such that $r = \dfrac m n$.
== Sources ==
* : $\S 3$: Natural Numbers: Exercise $\S 3.6 \ (4)$
Category:Between two Real Numbers exists Rational Number
Between two Similar Plane Numbers exists one Mean Proportional

== Theorem ==
== Proof ==
Let $m$ and $n$ be similar plane numbers.
Then for some $p_1, p_2, q_1, q_2 \in \Z$ such that $p_1 < p_2$ and $q_1 < q_2$:
:$m = p_1 p_2$
:$n = q_1 q_2$
such that:
:$\dfrac {p_1}{q_1} = \dfrac {p_2}{q_2}$
Thus let:
:$r := p_1 q_2 = q_1 p_2$
So:
and:
Thus by definition, $\paren {m, r, n}$ is a geometric sequence.
By definition, $r$ is a mean proportional between $m$ and $n$.
Thus as:
:$\dfrac {p_1}{q_1} = \dfrac m r = \dfrac r n = \dfrac {p_2}{q_2}$
it follows that $m$ is in duplicate ratio to $n$ as their sides.
== Sources ==
* : Book $\text{VIII}$. Propositions
Category:Euclidean Number Theory
Between two Similar Solid Numbers exist two Mean Proportionals

== Theorem ==
== Proof ==
Let $m$ and $n$ be similar solid numbers.
Then for some $a, b, c, d, e, f \in \Z$ such that $a \le b \le c$ and $d \le e \le f$:
:$m = a b c$
:$n = d e f$
such that:
:$\dfrac a d = \dfrac b e = \dfrac c f$
Let:
:$r := a e = b d = b f = c e$
So:
and:
Thus by definition, $\tuple {a b, r, d e}$ is a geometric sequence.
By definition, $r$ is a mean proportional between $a b$ and $d e$.
Now consider the products $r c$ and $r f$.
We have: 
and:
and:
That is:
:$\tuple {a b c, b c d, b d f, d e f}$ is a geometric sequence.
Also from the above:
:$\dfrac a d = \dfrac b e = \dfrac c f$
showing that $m$ is in triplicate ratio to $n$ as their sides.
== Sources ==
* : Book $\text{VIII}$. Propositions
::(in which a mistake apppears)
Category:Euclidean Number Theory
Between two Similar Solid Numbers exist two Mean Proportionals/Mistake

== Source Work ==
: Book $\text{VIII}$
:: Commentary on Proposition $19$
This mistake can be seen in the edition as published by Dover: ISBN 0-486-60089-0.
== Mistake ==
:[Euclid] next forms the products of $c, f$ respectively into the mean $b d$.
:Then $abc, cbd, fbd, def$ are in the ratio of $a$ to $d$ etc.
:For
The middle line of the above is incorrect -- it ought to read:
:$c b d : f b d = c : f$
Category:Mistakes/Euclid: The Thirteen Books of The Elements: Volume 2
Between two Squares exists one Mean Proportional

== Theorem ==
== Proof ==
Let $a^2$ and $b^2$ be square numbers.
Consider the number $a b$.
We have:
:$\dfrac {a^2} {a b} = \dfrac a b = \dfrac {a b} {b^2}$
By definition, it follows that $a b$ is the mean proportional between $a^2$ and $b^2$.
Then:
:$\paren {\dfrac a b}^2 = \dfrac {a^2} {b^2}$
By definition, it follows that $a^2$ has to $b^2$ the duplicate ratio that $a$ has to $b$.
== Sources ==
* : Book $\text{VIII}$. Propositions
Category:Euclidean Number Theory
Bhaskara's Lemma

== Lemma ==
Let $m \in \Z$ be an integer.
For $k \ne 0$:
:$N x^2 + k = y^2 \implies N \paren {\dfrac {m x + y} k}^2 + \dfrac {m^2 - N} k = \paren {\dfrac {m y + N x} k}^2$
== Proof ==
The implication goes the other way if $m^2 - N \ne 0$.
== Also see ==
This lemma is used when deriving the Chakravala Method of solving indeterminate quadratic equations.
Category:Algebra
Bhaskara II Acharya/Lilavati

== Problems by : ==
=== Chapter $\text {V}$. Progressions ===
=== Chapter $\text {VI}$. Plane Figure ===
</onlyinclude>
=== Chapter $\text {XIII}$. Combination of Digits ===
</onlyinclude>
Category:Examples of Algebra Problems
Category:Bhaskara II Acharya/Lilavati
Bhaskara II Acharya/Lilavati/Chapter V/124

== : : Chapter $\text {V}$: Progressions: $124$ ==
:In an expedition to seize his enemy's elephants, a king marched $2$ yojanas on the first day.
:Say, intelligent calculator, with what increasing rate of daily march did he proceed, since he reached his foe's city, a distance of $80$ yojanas, in a week?
== Solution ==
His march was increased by the rate of $\dfrac {22} 7$ yojanas per day.
== Proof ==
We are given that the daily rate of march increases each day by an arithmetic sequence.
Let the initial term be denoted by $a_0$.
Let the common difference, which we are to find, be denoted by $d$.
Let the number of days march be $n$.
Let the total number of yojanas marched be $T$.
Then:
== Sources ==
* : Part $\text {I}$: Arithmetic: Chap. $\text {IV}$: Of Progressions
* : Arithmetic (Lilavati): Chapter $\text {V}$: Progressions: $124$
* : Chapter $\text {V}$: Progressions: $124$
* 
* 
* : Indian Puzzles: $55$
Category:Bhaskara II Acharya/Lilavati
Bhaskara II Acharya/Lilavati/Chapter VI/150

== : Chapter $\text {VI}$: Plane Figure: $150$ ==
:A snake's hole is at the foot of a pillar which is $15$ cubits high and a peacock is perched on its summit.
:Seeing a snake, at a distance of thrice the pillar's height, gliding towards his hole, he pounces obliquely upon him.
:Say quickly at how many cubits from the snake's hole do they meet, both proceeding an equal distance?
== Solution ==
They meet $25$ cubits away from the pillar.
== Proof ==
Let $y$ be the distance away from the snake's hole where they meet.
Let the peacock and snake move $x$ cubits.
Then:
:$y = 45 = x$
The pillar, the ground and the flight of the peacock form a right triangle:
:with legs of $15$ and $45 - x$
:with hypotenuse $x$.
Hence:
It can be noted that the right triangle in question is the classic $\text {3-4-5}$ triangle expanded $5$ times.
== Sources ==
* : Part $\text {II}$: Chap. $\text {I}$: Of Geometrical Operations
* : Arithmetic (Lilavati): Chapter $\text {VI}$: Plane Figure: $150$
* : Chapter $\text {VI}$: Plane Figure: $150$
* 
* : Indian Puzzles: $56$
Category:Bhaskara II Acharya/Lilavati
Bhaskara II Acharya/Lilavati/Chapter XIII/269

== : Chapter $\text {XIII}$. Combination of Digits: $269$ ==
:How many are the variations of the form of the god Sambhu by the exchange of his $10$ attributes held reciprocally in his several hands:
:namely, the rope, the elephant's hook, the serpent, the tabor, the skull, the trident, the bedstead, the dagger, the arrow, and the bow:
:as those of Hari by the exchange of the mace, the discus, the lotus and the conch?
== Solution ==
For Sambhu: $3 \, 628 \, 800$.
For Hari: $24$.
== Proof ==
We have that Sambhu has $10$ objects which may be held in any of his $10$ hands.
Similarly, Hari has $4$ objects which may be held in any of his $4$ hands.
Thus we are asked: how many different possible representations can be made of each of these two gods, differentiating between them by means of which object is held in which hand?
Hence the question is an instance of Number of Permutations.
The number of permutations of $n$ objects from $n$ is given by:
:$^n P_n = n!$
Here we have that Sambhu has $10$ objects, and so:
:$10! = 3 \, 628 \, 800$
different representations.
Similarly we have that Hari has $4$ objects, and so:
:$4! = 24$
different representations.
== Historical Note ==
== Sources ==
* : Part $\text {IV}$: Of Transpositions
* : Arithmetic (Lilavati): Chapter $\text {XIII}$: Combination: $269$
* : Chapter $\text {XIII}$: Combination of Digits: $269$
* : Chapter $\text {IV}$: Algebra: Probability and Statistics: Permutations and Combinations
* 
* 
* : Indian Puzzles: $57$
Category:Bhaskara II Acharya/Lilavati
Bhaskara II Acharya/Lilavati/Chapter XIII/269/Historical Note

== Historical Note on Bhaskara II Acharya's Lilavati: Example $269$ ==
The specific names of the gods used in this example vary from text to text.
The canonical rendition from refers to Sambhu and Hari, while pointing out in a footnote that they are also called Siva and Vishnu.
 refers to Mahadev and Vishnu.
 points out:
:... the Hindus had different names for the god Hari according to the various arrangements of his four attributes in his four hands.
She then goes on to remark:
:We may imagine that Bhaskara had this in mind, and thought to astound his readers by the number of names that would have to be invented for Siva had that god been given a name for each of the ways in which his ten attributes could be placed in his ten hands.
== Sources ==
* : Part $\text {IV}$: Of Transpositions
* : Arithmetic (Lilavati): Chapter $\text {XIII}$: Combination: $269$
* : Chapter $\text {IV}$: Algebra: Probability and Statistics: Permutations and Combinations
Category:Historical Notes
Bias of Sample Variance

== Theorem ==
Let $X_1, X_2, \ldots, X_n$ form a random sample from a population with mean $\mu$ and variance $\sigma^2$.
Let: 
:$\ds \bar X = \frac 1 n \sum_{i \mathop = 1}^n X_i$
Then:
:$\ds {S_n}^2 = \frac 1 n \sum_{i \mathop = 1}^n \paren {X_i - \bar X}^2$
is a biased estimator of $\sigma^2$, with: 
:$\map {\operatorname {bias} } { {S_n}^2} = -\dfrac {\sigma^2} n$
== Proof == 
By definition, ${S_n}^2$ is a biased estimator of $\sigma^2$ : 
:$\expect { {S_n}^2} \ne \sigma^2$
We have: 
We have that: 
So:
So ${S_n}^2$ is a biased estimator of $\sigma^2$. 
Further, we have: 
:$\map {\operatorname {bias} } { {S_n}^2} = \sigma^2 - \dfrac {\sigma^2} n - \sigma^2 = -\dfrac {\sigma^2} n$
Category:Inductive Statistics
Biconditional/Examples/Monday iff Tomorrow Tuesday

== Examples of Biconditional ==
The following is an example of a biconditional statement:
:Either today is Monday today is the day before Tuesday.
== Sources ==
* : Chapter $1$: Elementary, my dear Watson: $\S 1.1$: You have a logical mind if... Example $1.1.1$
Category:Examples of Biconditional
Biconditional Elimination

== Theorem ==
The rule of biconditional elimination is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
=== Sequent Form ===
== Also known as ==
== Also see ==
* Definition:Biconditional
* Definition:Conditional
* Biconditional Introduction
Category:Biconditional
Category:Biconditional Elimination
Category:Conditional
Biconditional Elimination/Proof Rule

== Theorem ==
The rule of biconditional elimination is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in either of the two forms:
:$(1): \quad$ If we can conclude $\phi \iff \psi$, then we may infer $\phi \implies \psi$.
:$(2): \quad$ If we can conclude $\phi \iff \psi$, then we may infer $\psi \implies \phi$.
It can be written:
:$\ds {\phi \iff \psi \over \phi \implies \psi} {\iff}_{e_1} \qquad \text{or} \qquad {\phi \iff \psi \over \psi \implies \phi} {\iff}_{e_2}$
Thus it is used to introduce the biconditional operator into a sequent.
=== Tableau Form ===
== Also known as ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Technical Note ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$
* : $\S 1.2.5$: An aside: proof by contradiction: Exercises $1.6: \ 7$
Category:Rules of Inference
Category:Biconditional Elimination
Biconditional Elimination/Proof Rule/Tableau Form

== Proof Rule ==
Let $\phi \iff \psi$ be a well-formed formula] in a tableau proof whose main connective is the biconditional operator.
Biconditional Elimination is invoked for $\phi \iff \psi$ in either of the two forms:
;Form 1:
;Form 2:
== Also denoted as ==
Sources which refer to this rule as the biconditional-conditional rule may as a consequence give the abbreviation $\mathrm {BC}$.
Category:Tableau Proofs
Category:Biconditional Elimination
Biconditional Elimination/Proof Rule/Technical Note

== Technical Note on ==
When invoking in a tableau proof, use the template:
:{{BiconditionalElimination|line|pool|statement|depend|1 or 2}}
or:
:{{BiconditionalElimination|line|pool|statement|depend|1 or 2|comment}}
where:
:line is the number of the line on the tableau proof where is to be invoked
:pool is the pool of assumptions (comma-separated list)
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:depend is the line of the tableau proof upon which this line directly depends
:1 or 2 should hold 1 for BiconditionalElimination_1, and 2 for BiconditionalElimination_2
:comment is the (optional) comment that is to be displayed in the Notes column.
Category:Technical Notes
Biconditional Elimination/Sequent Form/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
$\begin{array}{|ccc||ccc|ccc|} \hline
p & \iff & q & p & \implies & q & q & \implies & p \\
\hline
\F & \T & \F & \F & \T & \F & \F & \T & \F \\
\F & \F & \T & \F & \T & \T & \T & \F & \F \\
\T & \F & \F & \T & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T \\
\hline
\end{array}$
As can be seen, when $p \iff q$ is true so are both $p \implies q$ and $q \implies p$.
Category:Truth Table Proofs
Category:Biconditional Elimination
Biconditional Equivalent to Biconditional of Negations/Formulation 1

== Theorem ==
:$p \iff q \dashv \vdash \neg p \iff \neg q$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== 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.
$\begin{array}{|ccc||ccccc|} \hline
p & \iff & q & \neg & p & \iff & \neg & q \\
\hline
\F & \T & \F & \T & \F & \T & \T & \F \\
\F & \F & \T & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \T & \F & \T & \F \\
\T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end{array}$
Category:Biconditional Equivalent to Biconditional of Negations
Category:Truth Table Proofs
Biconditional Equivalent to Biconditional of Negations/Formulation 1/Forward Implication

== Theorem ==
:$p \iff q \vdash \neg p \iff \neg q$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $4$ The Biconditional: Exercise $1 \ \text{(c)}$
Category:Biconditional Equivalent to Biconditional of Negations
Biconditional Equivalent to Biconditional of Negations/Formulation 1/Reverse Implication

== Theorem ==
:$\neg p \iff \neg q \vdash p \iff q$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $4$ The Biconditional: Exercise $1 \ \text{(d)}$
Category:Biconditional Equivalent to Biconditional of Negations
Biconditional Equivalent to Biconditional of Negations/Formulation 2

== Theorem ==
: $\vdash \left({p \iff q}\right) \iff \left({\neg p \iff \neg q}\right)$
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T96}$
Category:Biconditional Equivalent to Biconditional of Negations
Biconditional Introduction

== Proof Rule ==
The rule of biconditional introduction is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
=== Sequent Form ===
== Also known as ==
== Also see ==
* Definition:Biconditional
* Definition:Conditional
* Biconditional Elimination
Category:Biconditional Introduction
Category:Biconditional
Category:Conditional
Biconditional Introduction/Proof Rule

== Proof Rule ==
The rule of biconditional introduction is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in the form:
:If we can conclude both $\phi \implies \psi$ and $\psi \implies \phi$, then we may infer $\phi \iff \psi$.
It can be written:
:$\ds { {\phi \implies \psi \qquad \psi \implies \phi} \over \phi \iff \psi} \iff_i$
Thus it is used to introduce the biconditional operator into a sequent.
=== Tableau Form ===
== Also known as ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Technical Note ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$
* : $\S 1.2.5$: An aside: proof by contradiction: Exercises $1.6: \ 7$
Category:Rules of Inference
Category:Biconditional Introduction
Biconditional Introduction/Proof Rule/Tableau Form

== Proof Rule ==
Let $\phi \implies \psi$ and $\psi \implies \phi$ be two conditional statements involving the two well-formed formulas $\phi$ and $\psi$ in a tableau proof.
Biconditional Introduction is invoked for $\phi$ and $\psi$ in the following manner:
== Also denoted as ==
Sources which refer to this rule as the conditional-biconditional rule may as a consequence give the abbreviation $\mathrm {CB}$.
Category:Tableau Proofs
Biconditional Introduction/Proof Rule/Technical Note

== Technical Note on ==
When invoking in a tableau proof, use the template:
:{{BiconditionalIntro|line|pool|statement|first|second}}
or:
:{{BiconditionalIntro|line|pool|statement|first|second|comment}}
where:
:line is the number of the line on the tableau proof where is to be invoked
:pool is the combined pool of assumptions of each of the constituents (comma-separated list)
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:first is the first of the two lines of the tableau proof upon which this line directly depends
:second is the second of the two lines of the tableau proof upon which this line directly depends
:comment is the (optional) comment that is to be displayed in the Notes column.
Category:Technical Notes
Biconditional Introduction/Sequent Form

== Theorem ==
Biconditional Introduction can be symbolised by the sequent:
:$p \implies q, q \implies p \vdash p \iff q$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 1.2.5$: An aside: proof by contradiction: Exercises $1.6: \ 7$
Category:Biconditional Introduction
Biconditional Introduction/Sequent Form/Proof 2

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
$\begin{array}{|ccccccc||ccc|} \hline
(p & \implies & q) & \land & (q & \implies & p) & p & \iff & q\\
\hline
F & T & F & T & F & T & F & F & T & F \\
F & T & T & F & T & F & F & F & F & T \\
T & F & F & F & F & T & T & T & F & F \\
T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
As can be seen, only when both $p \implies q$ and $q \implies p$ are true, then so is $p \iff q$.
Category:Truth Table Proofs
Category:Biconditional Introduction
Biconditional as Disjunction of Conjunctions

== Theorem ==
==== Formulation 1 ====
==== Formulation 2 ====
== Also known as ==
This rule is also sometimes included as another form of the Rule of Material Equivalence
Category:Biconditional as Disjunction of Conjunctions
Category:Biconditional
Category:Disjunction
Category:Conjunction
Biconditional as Disjunction of Conjunctions/Formulation 1

== Theorem ==
: $p \iff q \dashv \vdash \paren {p \land q} \lor \paren {\neg p \land \neg q}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
Category:Biconditional as Disjunction of Conjunctions
Biconditional as Disjunction of Conjunctions/Formulation 1/Proof

== Theorem ==
== 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.
$\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}$
Category:Biconditional as Disjunction of Conjunctions
Category:Truth Table Proofs
Biconditional as Disjunction of Conjunctions/Formulation 2

== Theorem ==
:$\vdash \paren {p \iff q} \iff \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} }$
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T83}$
* : $2$ Arguments Containing Compound Statements: $2.4$: Statement Forms: Exercise $\text{II}. \ 8$
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement: $17.$
* : $\S \text{II}$: The Logic of Statements $(2):$: The remaining rules of inference: $17$
Category:Biconditional as Disjunction of Conjunctions
Biconditional as Disjunction of Conjunctions/Formulation 2/Proof by Truth Table

== Theorem ==
== 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}$
== Sources ==
* : $\S \text{I}: 13$: Logical Equivalences: Exercise $\text{(A)} \ 12$
Category:Biconditional as Disjunction of Conjunctions
Category:Truth Table Proofs
Biconditional iff Disjunction implies Conjunction/Formulation 1

== Theorem ==
:$p \iff q \dashv \vdash \paren {p \lor q} \implies \paren {p \land q}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
Category:Biconditional iff Disjunction implies Conjunction