nyuuzyou/wikis huggingface dataset:
Rule of Material Implication/Formulation 2

== Theorem ==
:$\vdash \paren {p \implies q} \iff \paren {\neg p \lor q}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $\S \text{II}$: Exercise $11 \ \text{(b)}$
* : $\S 3.6$: Reference Formulae: $\text {RF} \, 17$
* : $\S 4.7$: The Derivation of Formulae: $\text D \, 25$
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text {T46}$
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement: $16.$
* : $\S \text{II}$: The Logic of Statements $(2):$: The remaining rules of inference: $16$
Category:Rule of Material Implication
Rule of Material Implication/Formulation 2/Forward Implication

== Theorem ==
: $\vdash \left({p \implies q}\right) \implies \left({\neg p \lor q}\right)$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$
Category:Rule of Material Implication
Rule of Material Implication/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|cccc|} \hline
(p & \implies & q) & \iff & (\neg & p & \lor & q) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T & \T \\
\hline
\end{array}$
== Sources ==
* : $\S \text{II}$: Exercise $13$
* : $\S \text{I}: 13$: Logical Equivalences
Category:Rule of Material Implication
Category:Truth Table Proofs
Rule of Material Implication/Formulation 2/Reverse Implication

== Theorem ==
:$\vdash \paren {\neg p \lor q} \implies \paren {p \implies q}$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.5: \ 2 \ \text{(i)}$
Category:Rule of Material Implication
Rule of Material Implication with Amphiboly

== Source Work ==
:
: Chapter $1$: Propositional logic
:: $1.2.1$ Rules for natural deduction: Exercises $1.5 \ 2 \ \text{(i)}$
== Mistake ==
Prove the sequent
:$\vdash \neg p \lor q \longrightarrow p \longrightarrow q$.
== Correction ==
This propositional formula as it stands is an amphiboly.
It needs parentheses put in:
: $\vdash \left({\neg p \lor q}\right) \implies \left({p \implies q}\right)$
See Rule of Material Implication/Formulation 2/Reverse Implication.
== Sources ==
* : $1.2.1$ Rules for natural deduction: Exercises $1.5 \ 2 \ \text{(i)}$
Category:Mistakes/Logic in Computer Science
Rule of Sequent Introduction

== Theorem ==
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.
== Also known as ==
This rule is also known as the rule of replacement.
== Also see ==
* Rule of Theorem Introduction, which is a direct corollary of this.
== Technical Note ==
== Sources ==
* : $\S 3.9$: Derivation by Substitution
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 4$
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement
Category:Rule of Sequent Introduction
Category:Rules of Inference
Category:Logic
Rule of Sequent Introduction/Technical Note

== Technical Note on Rule of Sequent Introduction ==
When invoking Rule of Sequent Introduction in a tableau proof, use the template:
:{{SequentIntro|line|pool|statement|depends|sequent}}
where:
:line is the number of the line on the tableau proof where Rule of Sequent Introduction 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
:sequent is the link to the sequent in question that will be displayed in the Notes column.
Category:Technical Notes
Rule of Simplification

== Sequent ==
The rule of simplification is a valid argument in types of logic dealing with conjunctions $\land$.
This includes propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
=== Sequent Form ===
== Explanation ==
== Also known as ==
== Also see ==
* Definition:Conjunction
* Rule of Conjunction
Category:Rule of Simplification
Category:Conjunction
Rule of Simplification/Also known as

== Rule of Simplification ==
The Rule of Simplification can also be referred to as the rule of and-elimination.
Some sources give this as the law of simplification for logical multiplication.
Such treatments may also refer to the Rule of Addition as the law of simplification for logical addition.
This extra level of wordage has not been adopted by , as it is argued that it may cause clarity to suffer.
Category:Rule of Simplification
Rule of Simplification/Explanation

== Rule of Simplification ==
The rule of simplification consists of two proof rules in one.
The first of the two can be expressed in natural language as:
:Given a conjunction, we may infer the first of the conjuncts.
The second of the two can be expressed in natural language as:
:Given a conjunction, we may infer the second of the conjuncts.
Category:Rule of Simplification
Rule of Simplification/Proof Rule

== Proof Rule ==
The rule of simplification is a valid argument in types of logic dealing with conjunctions $\land$.
This includes 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 \land \psi$, then we may infer $\phi$.
:$(2): \quad$ If we can conclude $\phi \land \psi$, then we may infer $\psi$.
It can be written:
:$\ds {\phi \land \psi \over \phi} \land_{e_1} \qquad \qquad {\phi \land \psi \over \psi} \land_{e_2}$
=== Tableau Form ===
== Explanation ==
== Also known as ==
== Also see ==
* This is a rule of inference of the following proof system:
** Definition:Natural Deduction
* Rule of Conjunction
== Technical Note ==
== Sources ==
* : $\S \text{II}.12$: Laws of sentential calculus
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction
* : $\S \text{II}$: The Logic of Statements $(2): \ 1$: Decision procedures and proofs: $7$
* : $\S 1.2.1$: Rules for natural deduction
Category:Rule of Simplification
Category:Rules of Inference
Rule of Simplification/Proof Rule/Tableau Form

== Proof Rule ==
Let $\phi \land \psi$ be a well-formed formula in a tableau proof whose main connective is the conjunction operator.
The Rule of Simplification is invoked for $\phi \land \psi$ in either of the two forms:
;Form 1:
;Form 2:
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction
Category:Tableau Proofs
Rule of Simplification/Proof Rule/Technical Note

== Technical Note on ==
When invoking the in a tableau proof, use the template:
:{{Simplification|line|pool|statement|depend|1 or 2}}
or:
:{{Simplification|line|pool|statement|depend|1 or 2|comment}}
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
:depend is the line of the tableau proof upon which this line directly depends
:1 or 2 should hold 1 for Simplification_1, and 2 for Simplification_2
:comment is the (optional) comment that is to be displayed in the Notes column.
Category:Technical Notes
Rule of Simplification/Sequent Form/Formulation 1/Form 1

== Theorem ==
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $2$ Arguments Containing Compound Statements: $2.3$: Argument Forms and Truth Tables: Exercise $\text{I} \ \mathbf b.$
* : $3$: The Method of Deduction: $3.1$: Formal Proof of Validity: Rules of Inference: $7.$
Category:Rule of Simplification
Rule of Simplification/Sequent Form/Formulation 1/Form 1/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
$\begin{array}{|ccc||c|} \hline
p & \land & q & p \\
\hline
\F & \F & \F & \F \\
\F & \F & \T & \F \\
\T & \F & \F & \T \\
\T & \T & \T & \T \\
\hline
\end{array}$
As can be seen, when $p \land q$ is true so is $p$.
== Sources ==
* : $\S 1$: Informal statement calculus: $\S 1.2$: Truth functions and truth tables: Example $1.8 \ \text{(a)}$
Category:Truth Table Proofs
Category:Rule of Simplification
Rule of Simplification/Sequent Form/Formulation 1/Form 2/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
$\begin{array}{|ccc||c|} \hline
p & \land & q & q \\
\hline
\F & \F & \F & \F \\
\F & \F & \T & \T \\
\T & \F & \F & \F \\
\T & \T & \T & \T \\
\hline
\end{array}$
As can be seen, when $p \land q$ is true so is $q$.
Category:Truth Table Proofs
Category:Rule of Simplification
Rule of Simplification/Sequent Form/Formulation 1/Proof

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
$\begin{array}{|ccc||c|c|} \hline
p & \land & q & p & q \\
\hline
F & F & F & F & F \\
F & F & T & F & T \\
T & F & F & T & F \\
T & T & T & T & T \\
\hline
\end{array}$
As can be seen, when $p \land q$ is true so are both $p$ and $q$.
Category:Truth Table Proofs
Category:Rule of Simplification
Rule of Simplification/Sequent Form/Formulation 2/Form 1

== Theorem ==
:$\vdash p \land q \implies p$
== Proof ==
== Sources ==
* : $\S 3.6$: Reference Formulae: $RF \, 4$
* : $\S 4.7$: The Derivation of Formulae: $D \, 28$
Category:Rule of Simplification
Rule of Simplification/Sequent Form/Formulation 2/Proof 1/Form 1

== Theorem ==
:$\vdash p \land q \implies p$
== Proof ==
== Sources ==
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules: Theorem $41$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.4: \ 1 \ \text{(a)}$
Category:Rule of Simplification
Rule of Simplification/Sequent Form/Formulation 2/Proof 2

== 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|c||c|c|} \hline
p & \land & q & p & q & p \land q \implies p & p \land q \implies q \\
\hline
\F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
== Sources ==
* : $\S \text{II}.13$: Symbolism of sentential calculus
* 
* 
Category:Rule of Simplification
Category:Truth Table Proofs
Rule of Substitution

== Theorem ==
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.
== Also known as ==
Some sources amplify the name to rule of uniform substitution.
== Applications ==
This proof leads on to the Rule of Sequent Introduction.
== Technical Note ==
== Sources ==
* : $\S \text{II}.15$: Rules of inference
* : $\S 4.2$: The Construction of an Axiom System: $RST \, 1$
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 4$
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules
* : $\S 1.6$: Truth Tables and Tautologies
Category:Rule of Substitution
Rule of Substitution/Technical Note

== Technical Note on Rule of Substitution ==
When invoking the Rule of Substitution in a tableau proof, use the template:
:{{Substitution|line|pool|statement|depends|instance 1}}
:{{Substitution|line|pool|statement|depends|instance 1|substitution 1}}
:{{Substitution|line|pool|statement|depends|instance 1|substitution 1|instance 2|substitution 2}}
:{{Substitution|line|pool|statement|depends|instance 1|substitution 1|instance 2|substitution 2|instance 3|substitution 3}}
where:
:line is the number of the line on the tableau proof where the Rule of Substitution is to be invoked
:pool is the pool of assumptions (comma-separated list) of the statement on which the Rule of Substitution is to be used
: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 of the statement on which the Rule of Substitution is to be used
:instance 1 is that which is being substituted
:substitution 1 is what it is being replaced with
Optionally you can perform up to $3$ substitutions:
:instance 2 is that which is being substituted: instance 2
:substitution 2 is what it is being replaced with: instance 2
:instance 3 is that which is being substituted: instance 3
:substitution 3 is what it is being replaced with: instance 3.
Category:Technical Notes
Rule of Theorem Introduction

== Definition ==
We may infer, at any stage of a proof (citing $\text {TI}$), a theorem already proved, together with a reference to the theorem that is being cited.
== Proof ==
This theorem is a corollary of the Rule of Sequent Introduction.
== Application ==
Using this rule, we can use theorems that we have derived in order to shorten proofs which may otherwise be long and unwieldy.
== Technical Note ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 4$
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules
Category:Rule of Theorem Introduction
Category:Rules of Inference
Category:Logic
Rule of Theorem Introduction/Technical Note

== Technical Note on Rule of Theorem Introduction ==
When invoking Rule of Theorem Introduction in a tableau proof, use the template:
:{{TheoremIntro|line|statement|theorem}}
where:
:line is the number of the line on the tableau proof where the Rule of Theorem Introduction is to be invoked
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:theorem is the link to the theorem in question that will be displayed in the Notes column.
Category:Technical Notes
Rule of Top-Introduction

== Proof Rule ==
The Rule of Top-Introduction is a valid deduction sequent in propositional logic:
At any stage, we may conclude a tautology $\top$.
It can be written:
:$\ds {\hspace{4em} \over \top} \top_i$
=== Sequent Form ===
The Rule of Top-Introduction can be symbolised by the sequent:
:$\vdash \top$
=== Tableau Form ===
== Explanation ==
This entirely obvious rule allows to manipulate formulae involving $\top$ in tableau proofs.
== Technical Note ==
When invoking the Rule of Top-Introduction in a tableau proof, use the template:
:{{TopIntro|line}}
where:
:line is the number of the line on the tableau proof where the Rule of Top-Introduction is to be invoked
Category:Tautology
Category:Rules of Inference
Rule of Transposition

== Theorem ==
=== Formulation 1 ===
=== Formulation 2 ===
== Variants ==
The following are variants of this rule:
=== Variant 1 ===
=== Variant 2 ===
== Also known as ==
== Also see ==
* Definition:Contrapositive Statement
* Modus Tollendo Tollens
== Sources ==
* : $\S \text{II}.14$: Application of laws of sentential calculus in inference
* : $\S 1$: Some mathematical language: Axioms
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic
* 
* 
* 
Category:Rule of Transposition
Category:Conditional
Category:Logical Negation
Category:Modus Tollendo Tollens
Rule of Transposition/Also known as

== Rule of Transposition: Also known as ==
The Rule of Transposition is also known as:
:the Law of Transposition
:the Rule of Contraposition
:the Law of Contraposition.
== Sources ==
* : $\S \text{II}.14$: Application of laws of sentential calculus in inference
* : $\S 3.6$: Reference Formulae: $\text {RF} \, 16$
* : $\S 4$: The implies sign ($\Rightarrow$): $4.1$
* : $\S 1.13$: Tableau Problems (TAB1): CONTR
Category:Rule of Transposition
Rule of Transposition/Formulation 1

== Theorem ==
A statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
Its abbreviation in a tableau proof is $\textrm {TP}$.
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof 1 ==
=== Law of the Excluded Middle ===
The proof of the reverse implication depends on the Law of the Excluded Middle, by way of Double Negation Elimination.
This is one of the logical axioms that was determined by , and forms part of the backbone of classical (Aristotelian) logic.
However, the intuitionist school rejects the Law of the Excluded Middle as a valid logical axiom.
This in turn invalidates the proof of the reverse implication from an intuitionistic perspective.
== Proof by Truth Table ==
== Also known as ==
== Also see ==
* Definition:Contrapositive Statement
== Sources ==
* : Introduction: Logic
* : $\S 4$: The implies sign ($\Rightarrow$): $4.1$
* : $\S 1$: Informal statement calculus: $\S 1.2$: Truth functions and truth tables: Exercise $6 \ \text{(a)}$
* : $\S 1.2.4$: Provable equivalence
* : $\S 2.3.3$
Category:Rule of Transposition
Rule of Transposition/Formulation 1/Forward Implication

== Theorem ==
== Proof ==
== Sources ==
* : $\S1.2$: Some Remarks on the Use of the Connectives and, or, implies
* : $2$ Arguments Containing Compound Statements: $2.3$: Argument Forms and Truth Tables: Exercise $\text{II} \ \mathbf 7.$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.4: \ 2 \ \text{(m)}$
Category:Rule of Transposition
Rule of Transposition/Formulation 1/Proof 1

== Theorem ==
:$p \implies q \dashv \vdash \neg q \implies \neg p$
== Proof ==
=== Proof of Forward Implication ===
=== Proof of Reverse Implication ===
=== Law of the Excluded Middle ===
The proof of the reverse implication depends on the Law of the Excluded Middle, by way of Double Negation Elimination.
This is one of the logical axioms that was determined by , and forms part of the backbone of classical (Aristotelian) logic.
However, the intuitionist school rejects the Law of the Excluded Middle as a valid logical axiom.
This in turn invalidates the proof of the reverse implication from an intuitionistic perspective.
Category:Rule of Transposition
Rule of Transposition/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}{|ccc||ccccc|} \hline
p & \implies & q & \neg & q & \implies & \neg & p \\
\hline
\F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \F & \T & \T & \T & \F \\
\T & \F & \F & \T & \F & \F & \F & \T \\
\T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end{array}$
Category:Truth Table Proofs
Category:Rule of Transposition
Rule of Transposition/Formulation 1/Reverse Implication

== Theorem ==
:$\neg q \implies \neg p \vdash p \implies q$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation: Exercise $1 \ \text{(h)}$
* : $\S1.2$: Some Remarks on the Use of the Connectives and, or, implies: Exercise $1$
* : $\S 1.14$: Exercise $17 \ \text{(iv)}$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.5: \ 1 \ \text{(a)}$
Category:Rule of Transposition
Rule of Transposition/Formulation 2

== Theorem ==
:$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$
== Proof 1 ==
== Proof by Truth Table ==
== Also known as ==
== Also see ==
* Definition:Contrapositive Statement
== Sources ==
* : $\S 3.6$: Reference Formulae: $\text {RF} \, 16$
* : $\S 4.7$: The Derivation of Formulae: $\text D \, 18 - 20$
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T111}$
* : $2$ Arguments Containing Compound Statements: $2.4$: Statement Forms: Exercise $\text{II}. \ 2$
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement: $15.$
* : $\S \text{II}$: The Logic of Statements $(2)$: The remaining rules of inference: $15$
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic: Exercise $(3)$
* : $\S 1.13$: Tableau Problems (TAB1): CONTR
Category:Rule of Transposition
Rule of Transposition/Formulation 2/Forward Implication/Proof

== Theorem ==
:$\vdash \paren {p \implies q} \implies \paren {\neg q \implies \neg p}$
== Proof ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 5$: Theorem $\text{T13}$
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules: Theorem $42$
Category:Rule of Transposition
Rule of Transposition/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 connectives match for all boolean interpretations.
$\begin{array}{|ccc|c|ccccc|} \hline
p & \implies & q) & \iff & (\neg & q & \implies & \neg & p) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F \\
\T & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end{array}$
== Sources ==
* : $\S \text{I}: 13$: Logical Equivalences: Exercise $\text{(A)} \ 7$
Category:Rule of Transposition
Category:Truth Table Proofs
Rule of Transposition/Formulation 2/Reverse Implication/Proof

== Theorem ==
: $\vdash \left({\neg q \implies \neg p}\right) \implies \left({p \implies q}\right)$
== Proof ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 5$: Theorem $\text{T16}$
* : Axiom $A3$
Category:Rule of Transposition
Rule of Transposition/Variant 1/Formulation 1/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 connectives match for all boolean interpretations.
$\begin{array}{|cccc||cccc|} \hline
p & \implies & \neg & q & q & \implies & \neg & p \\
\hline
F & T & T & F & F & T & T & F \\
F & T & F & T & T & T & T & F \\
T & F & T & F & F & F & F & T \\
T & T & F & T & T & T & F & T \\
\hline
\end{array}$
Category:Truth Table Proofs
Category:Rule of Transposition
Rule of Transposition/Variant 1/Formulation 2

== Theorem ==
:$\vdash \paren {p \implies \neg q} \iff \paren {q \implies \neg p}$
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T112}$
Category:Rule of Transposition
Rule of Transposition/Variant 1/Formulation 2/Forward Implication

== Theorem ==
:$\vdash \paren {p \implies \neg q} \implies \paren {q \implies \neg p}$
== Proof ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 5$: Theorem $\text{T14}$
Category:Rule of Transposition
Rule of Transposition/Variant 2/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}{|cccc||cccc|} \hline
\neg & p & \implies & q & \neg & q & \implies & p \\
\hline
\T & \F & \T & \F & \T & \F & \T & \F \\
\T & \F & \T & \T & \F & \T & \T & \F \\
\F & \T & \F & \F & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$
Category:Truth Table Proofs
Category:Rule of Transposition
Rule of Transposition/Variant 2/Formulation 2

== Theorem ==
: $\vdash \left({\neg p \implies q}\right) \iff \left({\neg q \implies p}\right)$
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T113}$
Category:Rule of Transposition