nyuuzyou/wikis huggingface dataset:
Rule of Explosion

== Proof Rule ==
The rule of explosion is a valid argument in certain types of logic dealing with contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not Johansson's minimal logic.
=== Proof Rule ===
=== Sequent Form ===
== Explanation ==
== Variants ==
The following can be used as variants of this theorem:
=== Variant 1 ===
=== Variant 2 ===
=== Variant 3 ===
== Also known as ==
== Also see ==
* Definition:Contradiction
* False Statement implies Every Statement
Category:Contradiction
Category:Rule of Explosion
Rule of Explosion/Explanation

== Proof Rule ==
The Rule of Explosion can be expressed in natural language as:
:If you can prove a contradiction, you can prove anything.
Compare this with the colloquial expression:
:"If England win the World Cup this year, then I'm a kangaroo."
The assumption is that the concept of England winning the world cup is an inherent contradiction (it being taken worldwide as a self-evident truth that England will never win the World Cup again). Therefore, if England does win the World Cup this year, then this would imply a falsehood as the author of this page is certainly human.
This rule is denied validity in the system of Johansson's minimal logic.
Category:Rule of Explosion
Rule of Explosion/Proof Rule

== Proof Rule ==
The rule of explosion is a valid argument in certain types of logic dealing with contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not Johansson's minimal logic.
As a proof rule it is expressed in the form:
:If a contradiction can be concluded, it is possible to infer any statement $\phi$.
It can be written:
:$\ds {\bot \over \phi} \bot_e$
=== Tableau Form ===
== Explanation ==
== Also known as ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Technical Note ==
== Sources ==
* : $\S 1.2.1$: Rules for natural deduction
Category:Rule of Explosion
Category:Rules of Inference
Rule of Explosion/Proof Rule/Technical Note

== Technical Note on ==
When invoking the in a tableau proof, use the template:
:{{Explosion|line|pool|statement|depends}}
or:
:{{Explosion|line|pool|statement|depends|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
:depends is the line of the tableau proof upon which this line directly depends, the one with $\bot$ on it
:comment is the (optional) comment that is to be displayed in the Notes column.
Category:Technical Notes
Rule of Exportation/Formulation 1

== Theorem ==
:$\paren {p \land q} \implies r \dashv \vdash p \implies \paren {q \implies r}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $5$ Further Proofs: Résumé of Rules: Theorem $30$
* : $\S 1.2.1$: Rules for natural deduction
Category:Rule of Exportation
Rule of Exportation/Formulation 1/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccc|} \hline
(p & \land & q) & \implies & r & p & \implies & (q & \implies & r) \\
\hline
\F & \F & \F & \T & \F & \F & \T & \F & \T & \F \\
\F & \F & \F & \T & \T & \F & \T & \F & \T & \T \\
\F & \F & \T & \T & \F & \F & \T & \T & \F & \F \\
\F & \F & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \T & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \T & \F & \F & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
Category:Rule of Exportation
Category:Truth Table Proofs
Rule of Exportation/Formulation 2

== Theorem ==
:$\vdash \paren {\paren {p \land q} \implies r} \iff \paren {p \implies \paren {q \implies r} }$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
=== Proof of Forward Implication ===
=== Proof of Reverse Implication ===
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$: Theorem $\text{T27}$
* : $2$ Arguments Containing Compound Statements: $2.4$: Statement Forms: Exercise $\text{II}. \ 3$
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement: $18.$
* : $\S \text{II}$: The Logic of Statements $(2)$: The remaining rules of inference: $19$
Category:Rule of Exportation
Rule of Exportation/Forward Implication/Formulation 1/Proof

== Theorem ==
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Theorem $13$
* : $\S 1.2.1$: Rules for natural deduction: Example $1.13$
Category:Rule of Exportation
Rule of Exportation/Forward Implication/Formulation 2/Proof 2

== Theorem ==
== Proof ==
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccc|} \hline
((p & \land & q) & \implies & r) & \implies & (p & \implies & (q & \implies & r)) \\
\hline
F & F & F & T & F & T & F & T & F & T & F \\
F & F & F & T & T & T & F & T & F & T & T \\
F & F & T & T & F & T & F & T & T & F & F \\
F & F & T & T & T & T & F & T & T & T & T \\
T & F & F & T & F & T & T & T & F & T & F \\
T & F & F & T & T & T & T & T & F & T & T \\
T & T & T & F & F & T & T & F & T & F & F \\
T & T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
Category:Rule of Material Implication
Category:Truth Table Proofs
Rule of Exportation/Reverse Implication/Formulation 1/Proof

== Theorem ==
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Theorem $16$
* : $\S 1.2.1$: Rules for natural deduction: Example $1.14$
Category:Rule of Exportation
Rule of Exportation/Reverse Implication/Formulation 2

== Theorem ==
:$\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}$
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $\S \text{II}$: Exercise $12 \ \text{(b)}$
Category:Rule of Exportation
Rule of Exportation/Reverse Implication/Formulation 2/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccc|} \hline
(p & \implies & (q & \implies & r)) & \implies & ((p & \land & q) & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \T & \F & \T & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \F & \T & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \F & \T & \T & \T \\
\T & \T & \F & \T & \F & \T & \T & \F & \F & \T & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
== Sources ==
* : $\S \text{II}$: Exercise $13$
Category:Rule of Material Implication
Category:Truth Table Proofs
Rule of Idempotence

== Theorem ==
The rule of idempotence is two-fold:
=== Conjunction ===
=== Disjunction ===
Its abbreviation in a tableau proof is $\textrm{Idemp}$.
== Also known as ==
Some sources give this as the rule of tautology or law of tautology, but this is discouraged so as to avoid confusion with the definition of tautology.
== Technical Note ==
Category:Conjunction
Category:Disjunction
Category:Rule of Idempotence
Rule of Idempotence/Conjunction

== Theorem ==
The conjunction operator is idempotent:
=== Formulation 1 ===
=== Formulation 2 ===
Its abbreviation in a tableau proof is $\textrm{Idemp}$.
== Also known as ==
This rule is also known as the law of tautology for logical multiplication (or conjunction).
Category:Rule of Idempotence
Rule of Idempotence/Conjunction/Formulation 1

== Theorem ==
The conjunction operator is idempotent:
:$p \dashv \vdash p \land p$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
== Technical Note ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $5$ Further Proofs: Résumé of Rules: Exercise $1 \ \text{(b)}$
* : $\S 2.3.3$
Category:Rule of Idempotence
Rule of Idempotence/Conjunction/Formulation 1/Proof

== Theorem ==
== 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}$
Category:Rule of Idempotence
Category:Truth Table Proofs
Rule of Idempotence/Conjunction/Formulation 2

== Theorem ==
The conjunction operator is idempotent:
:$\vdash p \iff \paren {p \land p}$
== Proof ==
== Sources ==
* : $\S \text{II}.13$: Symbolism of sentential calculus
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$: Theorem $\text{T41}$
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement: $19.$
* : $\S \text{II}$: The Logic of Statements $(2)$: The remaining rules of inference: $18$
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic: Exercise $(1) \ \text{(i)}$
Category:Rule of Idempotence
Rule of Idempotence/Conjunction/Technical Note

== Technical Note on Rule of Idempotence: Conjunction ==
When invoking this version of the Rule of Idempotence in a tableau proof, use the Idempotence template:
:{{Idempotence|line|pool|statement|depends|type}}
where:
:line is the number of the line on the tableau proof where Rule of Idempotence 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
:depends is the line (or lines) of the tableau proof upon which this line directly depends
:type is the type of Rule of Idempotence whose link will be displayed in the Notes column: in this instance Conjunction.
Category:Technical Notes
Rule of Idempotence/Disjunction

== Theorem ==
The disjunction operation is idempotent:
=== Formulation 1 ===
=== Formulation 2 ===
Its abbreviation in a tableau proof is $\textrm{Idemp}$.
== Also known as ==
This rule is also known as the law of tautology for logical addition (or disjunction).
Category:Rule of Idempotence
Rule of Idempotence/Disjunction/Formulation 1

== Theorem ==
The disjunction operation is idempotent:
:$p \dashv \vdash p \lor p$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
== Technical Note ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $5$ Further Proofs: Résumé of Rules: Theorem $33$
* : $\S 2.3.3$
Category:Rule of Idempotence
Rule of Idempotence/Disjunction/Formulation 1/Forward Implication

== Theorem ==
:$p \vdash p \lor p$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $5$ Further Proofs: Résumé of Rules: Theorem $33 \ \text{(a)}$
Category:Rule of Idempotence
Rule of Idempotence/Disjunction/Formulation 1/Proof by Truth Table

== Theorem ==
== 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}$
Category:Truth Table Proofs
Category:Rule of Idempotence
Rule of Idempotence/Disjunction/Formulation 1/Reverse Implication

== Theorem ==
:$p \lor p \vdash p$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $5$ Further Proofs: Résumé of Rules: Theorem $33 \ \text{(b)}$
Category:Rule of Idempotence
Rule of Idempotence/Disjunction/Formulation 2

== Theorem ==
The disjunction operation is idempotent:
: $\vdash p \iff \paren {p \lor p}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
== Sources ==
* : $\S \text{II}.13$: Symbolism of sentential calculus
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T47}$
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement: $19.$
* : $\S \text{II}$: The Logic of Statements $(2)$: The remaining rules of inference: $18$
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic: Exercise $(1) \ \text{(ii)}$
Category:Rule of Idempotence
Rule of Idempotence/Disjunction/Technical Note

== Technical Note on Rule of Idempotence ==
When invoking this version of the Rule of Idempotence in a tableau proof, use the Idempotence template:
:{{Idempotence|line|pool|statement|depends|type}}
where:
:line is the number of the line on the tableau proof where Rule of Idempotence 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
:depends is the line (or lines) of the tableau proof upon which this line directly depends
:type is the type of Rule of Idempotence whose link will be displayed in the Notes column: in this instance Disjunction.
Category:Technical Notes
Rule of Idempotence/Technical Note

== Technical Note on Rule of Idempotence ==
When invoking Rule of Idempotence in a tableau proof, use the template:
:{{Idempotence|line|pool|statement|depends|type}}
where:
:line is the number of the line on the tableau proof where Rule of Idempotence 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
:depends is the line (or lines) of the tableau proof upon which this line directly depends
:type is the type of Rule of Idempotence: Disjunction or Conjunction, whose link will be displayed in the Notes column.
Category:Technical Notes
Rule of Implication

== Proof Rule ==
The rule of implication is a valid argument in types of logic dealing with conditionals $\implies$.
This includes propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
=== Sequent Form ===
== Explanation ==
== Also known as ==
== Also see ==
* Definition:Conditional
* Modus Ponendo Ponens
* Rule of Assumption
== Sources ==
* : $2$ Arguments Containing Compound Statements: $2.4$: Statement Forms
Category:Rule of Implication
Category:Conditional
Rule of Implication/Proof Rule

== Proof Rule ==
The rule of implication is a valid argument in types of logic dealing with conditionals $\implies$.
This includes propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in the form:
:If, by making an assumption $\phi$, we can conclude $\psi$ as a consequence, we may infer $\phi \implies \psi$.
:The conclusion $\phi \implies \psi$ does not depend on the assumption $\phi$, which is thus discharged.
It can be written:
:$\ds {\begin {array} {|c|} \hline \phi \\ \vdots \\ \psi \\ \hline \end {array} \over \phi \implies \psi} \to_i$
=== Tableau Form ===
== Explanation ==
== Also known as ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Technical Note ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$
* : Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation
* : $\S \text{II}$: The Logic of Statements $(2): \ 7$: Conditional proof
* : $\S 1.2.1$: Rules for natural deduction
Category:Rule of Implication
Category:Rules of Inference
Rule of Implication/Proof Rule/Tableau Form

== Proof Rule ==
Let $\phi$ and $\psi$ be two well-formed formulas in a tableau proof.
The Rule of Implication is invoked for $\phi$ and $\psi$ in the following manner:
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation
Category:Tableau Proofs
Category:Rule of Implication
Rule of Implication/Proof Rule/Technical Note

== Technical Note on ==
When invoking the in a tableau proof, use the template:
:{{Implication|line|pool|statement|start|end}}
where:
:line is the number of the line on the tableau proof where the 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
:start is the line of the tableau proof where the antecedent can be found
:end is the line of the tableau proof where the consequent can be found
Category:Technical Notes
Rule of Implication/Sequent Form/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
$\begin{array}{|c|c||ccc|} \hline
p & q & p & \implies & q\\
\hline
\F & \F & \F & \T & \F \\
\F & \T & \F & \T & \T \\
\T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T \\
\hline
\end{array}$
As can be seen by inspection, only when $p$ is true and $q$ is false, then so is $p \implies q$ also false.
Category:Truth Table Proofs
Category:Rule of Implication
Rule of Inference/Examples/Modus Ponendo Ponens

== Example of Rule of Inference ==
In the context of propositional logic, an example of a rule of inference is:
:If $p$ is a theorem, and $p \implies q$ is a theorem, then $q$ is a theorem.
which expresses Modus Ponendo Ponens.
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$
* : $\text{II}.10$ Formal Proofs
Category:Examples of Rules of Inference
Rule of Material Equivalence

== Theorem ==
The Rule of Material Equivalence is a valid deduction sequent in propositional logic:
:If we can conclude that $p$ implies $q$ and if we can also conclude that $q$ implies $p$, then we may infer that $p$ $q$.
==== Formulation 1 ====
==== Formulation 2 ====
== Sources ==
* : $\S \text{II}.12$: Laws of sentential calculus
* 
* 
Category:Rule of Material Equivalence
Category:Biconditional
Category:Conditional
Category:Conjunction
Rule of Material Equivalence/Formulation 1

== Theorem ==
The biconditional operation can be interpreted as the conjunction of conditionals:
:$p \iff q \dashv \vdash \paren {p \implies q} \land \paren {q \implies p}$
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $4$ The Biconditional
* : $\S 1$: Naive Set Theory: $\S 1.1$: What is a Set?
* : Chapter $1$: Elementary, my dear Watson: $\S 1.1$: You have a logical mind if...: Ponderable $1.1.1$
* : $\S 2.3.3$
Category:Rule of Material Equivalence
Rule of Material Equivalence/Formulation 1/Proof by Truth Table

== Theorem ==
== 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}{|ccc|ccccccc|} \hline
p & \iff & q & (p & \implies & q) & \land & (q & \implies & p) \\
\hline
\F & \T & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \F & \T & \F & \T & \T & \F & \T & \F & \F \\
\T & \F & \F & \T & \F & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
== Sources ==
* : $\S 2.5$: Further Logical Constants
* : $\S1.2$: Some Remarks on the Use of the Connectives and, or, implies
* : $\S \text{I}: 12$: Material Equivalence and Alternation
Category:Rule of Material Equivalence
Category:Truth Table Proofs
Rule of Material Equivalence/Formulation 2

== Theorem ==
:$\vdash \paren {p \iff q} \iff \paren {\paren {p \implies q} \land \paren {q \implies p} }$
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T81}$
* : $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:Rule of Material Equivalence
Rule of Material Equivalence/Formulation 2/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
$\begin{array}{|ccc|c|ccccccc|} \hline
(p & \iff & q) & \iff & (p & \implies & q) & \land & (q & \implies & p) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \F & \T & \T & \F & \T & \T & \F & \T & \F & \F \\
\T & \F & \F & \T & \T & \F & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
== Sources ==
* : $\S \text{I}: 13$: Logical Equivalences
Category:Rule of Material Equivalence
Category:Truth Table Proofs
Rule of Material Implication

== Theorem ==
The Rule of Material Implication is a valid deduction sequent in propositional logic:
==== Formulation 1 ====
==== Formulation 2 ====
That is:
:statement $p$ implies statement $q$
is logically equivalent to:
:statement $p$ is false or statement $q$ is true
== As a definition ==
== Also known as ==
== Also see ==
The following are related argument forms:
* Modus Ponendo Tollens
* Modus Tollendo Tollens
* Definition:Formal Implication
== Sources ==
* : $\S \text{II}.8$: Implication or Conditional Sentence
* : $\S 2.3$: Basic Truth-Tables of the Propositional Calculus
* : $2$ Arguments Containing Compound Statements: $2.2$: Conditional Statements
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic
* 
* 
Category:Rule of Material Implication
Category:Disjunction
Category:Conditional
Category:Logical Negation
Rule of Material Implication/Also known as

== Rule of Material Implication: Also known as == 
The Rule of Material Implication is sometimes seen referred to as the definition of material implication, as some sources use this rule as a definition of the conditional, so as to justify its semantics.
A material implication is sometimes expressed in the amplified form implication in material meaning.
== Sources ==
* : $\S \text{II}.8$: Implication or Conditional Sentence
* : $\S 2.3$: Basic Truth-Tables of the Propositional Calculus
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic
Category:Rule of Material Implication
Rule of Material Implication/Formulation 1

== Theorem ==
:$p \implies q \dashv \vdash \neg p \lor q$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof by Truth Table ==
== Sources ==
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules: Theorem $49$
* : $\S 1$: Informal statement calculus: $\S 1.2$: Truth functions and truth tables: Exercise $4$
* : $\S 1$: Naive Set Theory: $\S 1.1$: What is a Set?
* : $\S 1.2.4$: Provable equivalence
* : $\S 2.3.3$
* : $\S 2.10$: Exercise $2.3$
Category:Rule of Material Implication
Rule of Material Implication/Formulation 1/Forward Implication

== Theorem ==
:$p \implies q \vdash \neg p \lor q$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $5$ Further Proofs: Résumé of Rules: Exercise $1 \ \text {(i)}$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.5: \ 2 \ \text{(h)}$
Category:Rule of Material Implication
Rule of Material Implication/Formulation 1/Proof by Truth Table

== Theorem ==
== 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} {|ccc||cccc|} \hline
p & \implies & q & \neg & p & \lor & q \\
\hline
\F & \T & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T \\
\hline
\end {array}$
== Sources ==
* : $\S 2.3$: Basic Truth-Tables of the Propositional Calculus
* : Chapter $2$: The Propositional Calculus $2$: $3$ Truth-Tables
* : $\S 1$: Some mathematical language: Connectives
* : $\S 1$: Informal statement calculus: $\S 1.2$: Truth functions and truth tables: Example $1.4 \ \text{(a)}$
* : $\S 1.4.1$: The meaning of logical connectives: Exercise $1.8: \ 1$
Category:Rule of Material Implication
Category:Truth Table Proofs