Rules of Inference

Equivalence Rules

Aliases

Conjunction Introduction (&I, ∧I, ⦁I)

Example

Discussion

The justification takes the form "a,b &I", where [a] is the left conjunct and [b] is the right conjunct of [c]. If the lines are cited in reverse order (i.e., "b,a &I"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (&I), The Logic Book (&I), Accessible Introduction (∧I), Logics (&I), Logic Primer (&I), Symbolic Logic (&I), Modern Logic (&I), MacLogic (&I)

Custom: Select "&I" from Preferences > Rules.

Variants

Conj/&I (Alias)

Conjunction Elimination (&E, ∧E, ⦁E)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Deductions Default (&E), The Logic Book (&E), Accessible Introduction (∧E), Logics (&E), Logic Primer (&E), Symbolic Logic (&E), Modern Logic (&E), MacLogic (&E)

Custom: Select "&E" from Preferences > Rules.

Variants

&E (Rule), &ER (Rule), Simp/&E (Alias), Simp/&ER (Alias)

Conditional Introduction (→I, ⊃I)

Example

Discussion

The justification takes the form "a,b →I", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a →I"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

Availability

Deductions Default (→I), The Logic Book (⊃I), Accessible Introduction (→I), Logics (→I), Logic Primer (⊃I), Symbolic Logic (⊃I), Modern Logic (→I), MacLogic (→I)

Custom: Select "→I" from Preferences > Rules.

Variants

CP (Alias)

Conditional Elimination (→E, ⊃E)

Example

Discussion

The justification takes the form "a,b →E", where [a] is the conditional and [b] is the antecedent of the conditional. If the lines are cited in reverse order (i.e., "b,a →E"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (→E), The Logic Book (⊃E), Accessible Introduction (→E), Logics (→E), Logic Primer (⊃E), Symbolic Logic (⊃E), Modern Logic (→E), MacLogic (→E)

Custom: Select "→E" from Preferences > Rules.

Variants

MP (Alias)

Negation Introduction (~I, ¬I)

Example

Discussion

The justification takes the form "a,b ~I", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~I"), Deductions will flip the order (autocorrect). If the formula at [d] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation introduction rule, where the contradiction appears on separate lines.

Availability

Deductions Default (~I), The Logic Book (~I), Accessible Introduction (~I), Logics (~I), Logic Primer (~I), Modern Logic (~I), MacLogic (~I)

Custom: Select "~I" from Preferences > Rules.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~IE/RAA (Alias)

Negation Elimination (~E, ¬E)

Example

Discussion

The justification takes the form "a,b ~E", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~E"), Deductions will flip the order (autocorrect). If the formula at [d] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation elimination rule, where the contradiction appears on separate lines.

Availability

Deductions Default (~E), The Logic Book (~E), Accessible Introduction (~E), Logics (~E), Logic Primer (~E), Modern Logic (~E), MacLogic (~E)

Custom: Select "~E" from Preferences > Rules.

Variants

~E (Rule), ~EC (Rule), ~EP (Rule), RAA (Rule), ~E/~EP (Alias), ~E/~EC (Alias), IP/~EC (Alias), ~IE/RAA (Alias)

Disjunction Introduction (∨I)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Deductions Default (∨I), The Logic Book (∨I), Accessible Introduction (∨I), Logics (∨I), Logic Primer (∨I), Symbolic Logic (∨I), Modern Logic (∨I), MacLogic (∨I)

Custom: Select "∨I" from Preferences > Rules.

Variants

Disjunction Introduction (Rule), Disjunction Introduction/Restricted (Rule), Addition/∨I (Alias), Addition/∨IR (Alias)

Disjunction Elimination (∨E)

Example

Discussion

The justification takes the form "a,b-c,d-e ∨E", where [a] is a disjunction, [b] is an assumption of the left disjunct, [d] is an assumption of the right disjunct. If the formula at [f] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumptions are left undischarged, Deductions will mark them as discharged (autodischarge).

Availability

Deductions Default (∨E), The Logic Book (∨E), Accessible Introduction (∨E), Logics (∨E), Symbolic Logic (∨E), Modern Logic (∨E), MacLogic (∨E)

Custom: Select "∨E" from Preferences > Rules.

Variants

None

Biconditional Introduction (↔I, ≡I)

Example

Discussion

The justification takes the form "a-b,c-d ↔I", where [a] is the assumption of the left side of the target biconditional, and [c] is the assumption of the right side of target biconditional. If the formula at [e] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumptions are left undischarged, Deductions will mark them as discharged (autodischarge).

Availability

Deductions Default (↔I), The Logic Book (≡I), Accessible Introduction (↔I), Logics (↔I), Symbolic Logic (≡I)

Custom: Select "↔I" from Preferences > Rules.

Variants

Df (Rule), BC (Rule)

Biconditional Elimination (↔E, ≡E)

Example

Discussion

The justification takes the form "a,b ↔E", where [a] is right (or left) side of the biconditional, and [b] is the left (or right) side of the biconditional. If the lines are cited in reverse order (i.e., "b,a ↔E"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (↔E), The Logic Book (≡E), Accessible Introduction (↔E), Logics (↔E), Symbolic Logic (≡E)

Custom: Select "↔E" from Preferences > Rules.

Variants

Df (rule), BD (rule), ↔E/BD

Negation Introduction/Conjunction (~IC, ¬IC)

Example

Discussion

The justification takes the form "a,b ~IC", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~IC"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation introduction rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as &I or Conj). In most cases, this rule will be aliased as ~I or IP.

Availability

Deductions Default (~IC)

Custom: Select "~IC" from Preferences > Rules.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~IE/RAA (Alias)

Negation Elimination/Conjunction (~EC, ¬EC)

Example

Discussion

The justification takes the form "a,b ~EC", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~EC"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation introduction rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as &I or Conj). In most cases, this rule will be aliased as ~E.

Availability

Deductions Default (~EC)

Custom: Select "~EC" from Preferences > Rules.

Variants

~E (Rule), ~EC (Rule), ~EP (Rule), RAA (Rule), ~E/~EP (Alias), ~E/~EC (Alias), IP/~EC (Alias), ~IE/RAA (Alias)

Negation Introduction/Primitive (~IP, ¬IP)

Example

Discussion

The justification takes the form "a,b ~IP", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~IP"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This negation introduction rule is "primitive" in the sense that its schema does not involve any connective other than the negation. The successful use of this rule depends, in many cases, on a rule that is able to generate the contradiction symbol ("Λ") (such as ~EP). In most cases, this rule will be aliased as ~I.

Availability

Deductions Default (~IP)

Custom: Select "~IP" from Preferences > Rules.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~E (Rule), ~EC (Rule), ~EP (Rule), RAA (Rule), ~E/~EP (Alias), ~E/~EC (Alias), IP/~EC (Alias), ~IE/RAA (Alias)

Negation Elimination/Primitive (~EP, ¬EP)

Example

Discussion

The justification takes the form "a,b ~EP", where [a] is a negation, and [b] is the main subformula of that negation. If the lines are cited in reverse order (i.e., "b,a ~EP"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer "Λ" (autoinfer).

This negation elimination rule is "primitive" in the sense that its schema does not involve any connective other than the negation. In most cases, this rule will be aliased as ~E.

Availability

Deductions Default (~EP)

Custom: Select "~EP" from Preferences > Rules.

Variants

~E (Rule), ~EC (Rule), ~EP (Rule), RAA (Rule), ~E/~EP (Alias), ~E/~EC (Alias), IP/~EC (Alias), ~IE/RAA (Alias)

Reductio Ad Absurdum (RAA)

Example

Discussion

The justification takes the form "a-b RAA", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b-a RAA"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as &I or Conj). RAA functions an inclusive disjunction of negation introduction/conjunction and negation elimination/conjunction: if the sequent is valid on either ~IC or ~EC, it will be valid on RAA.

Availability

Deductions Default (RAA)

Custom: Select "RAA" from Preferences > Rules.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~IE/RAA (Alias)

Definition (Df)

Example

Discussion

If the formula at [b] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

This rule takes a conjunction and infers a biconditional, or takes a biconditional and infers a conjunction. The left and right sides of the biconditional formula have an order that corresponds to the antecedent and consequent of the left conjunct of the conjunction.

Availability

Deductions Default (Df), Modern Logic (Df), MacLogic (Df)

Custom: Select "Df" from Preferences > Rules.

Variants

↔I (Rule), ↔E (Rule), BC (Rule), BD (Rule)

Double Negation (DN)

Example

Discussion

If the formula at [b] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

This rule removes a double-negation from the beginning of a formula, but does not add a double-negation to the beginning of a formula. See DNE for a rule that does both. The use of DN together with ~I, ~IC or ~IP guarantees a classical system of logic.

Availability

Deductions Default (DN), Modern Logic (DN), MacLogic (DN)

Custom: Select "DN" from Preferences > Rules.

Variants

EFQ (Rule), DNE (Rule)

Ex Falso Quodlibet (EFQ)

Example

Discussion

Autoinfer is not available for this rule.

Although EFQ allows any formula to be inferred from "Λ", it does not discharge any assumptions. The use of EFQ together with ~IP and ~EP, with all other negation rules and rules that involve negation turned off (i.e., ~I, ~E, ~IC, ~EC, RAA, DN, DS, MT, DNE) guarantees an intuitionist system of logic.

Availability

Deductions Default (EFQ), Modern Logic (EFQ), MacLogic (EFQ)

Custom: Select "EFQ" from Preferences > Rules.

Variants

DN (Rule), DNE (Rule)

Disjunctive Syllogism (DS)

Example

Discussion

The justification takes the form "a,b DS", where [a] is a disjunction, and [b] is the negation of the left or right disjunct. If the lines are cited in reverse order (i.e., "b,a DS"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (DS), Introduction to Logic (DS), Logic and Philosophy (DS), The Power of Logic (DS), A Concise Introduction to Logic (DS)

Custom: Select "DS" from Preferences > Rules.

Variants

∨E (Alias)

Modus Tollens (MT)

Example

Discussion

The justification takes the form "a,b MT", where [a] is a conditional, and [b] is the negation of the consequent. If the lines are cited in reverse order (i.e., "b,a MT"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (MT), Introduction to Logic (MT), Logic and Philosophy (MT), The Power of Logic (MT), A Concise Introduction to Logic (MT)

Custom: Select "MT" from Preferences > Rules.

Variants

None

Hypothetical Syllogism (HS)

Example

Discussion

The justification takes the form "a,b HS". If the lines are cited in reverse order (i.e., "b,a HS"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (HS), Introduction to Logic (HS), Logic and Philosophy (HS), The Power of Logic (HS), A Concise Introduction to Logic (HS)

Custom: Select "HS" from Preferences > Rules.

Variants

None

Absorption (Abs)

Example

Discussion

If the formula at [b] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (Abs), Introduction to Logic (Abs)

Custom: Select "Abs" from Preferences > Rules.

Variants

None

Constructive Dilemma (CD)

Example

Discussion

The justification takes the form "a,b,c CD", where [a] is a disjunction, [b] is a conditional whose antecedent is the same as the left disjunct as [a], and [c] is a conditional whose antecedent is the same as the right disjunct of [a]. If the lines are cited with the disjunction in the third position (i.e., "b,c,a CD"), Deductions will change the order so that the disjunction is in the first position (autocorrect). If the formula at [d] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (CD), Introduction to Logic (CD), Logic and Philosophy (CD), The Power of Logic (CD), A Concise Introduction to Logic (CD)

Custom: Select "CD" from Preferences > Rules.

Variants

Constructive Dilemma/Conjunction (Rule)

Constructive Dilemma/Conjunction (CDC)

Example

Discussion

The justification takes the form "a,b CDC", where [a] is a disjunction, and [b] is a conjunction of conditionals. The antecedent of the left conditional is the same as the left disjunct of [a], and the antecedent of the right conditional is the same as the right disjunct of [a]. If the lines are cited in reverse order (i.e., "b,a CDC"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Deductions Default (CDC)

Custom: Select "CDC" from Preferences > Rules.

Variants

Constructive Dilemma (Rule)

Biconditional Composition (BC)

Example

Discussion

If the formula at [b] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

This rule takes a conjunction and infers a biconditional. The left and right sides of the biconditional formula have an order that corresponds to the antecedent and consequent of the left conjunct of the conjunction. In most cases, this rule will be aliased as ↔E.

Availability

Deductions Default (BC)

Custom: Select "BC" from Preferences > Rules.

Variants

Biconditional Introduction (Rule), Df (Rule)

Biconditional Decomposition (BD)

Example

Discussion

Autoinfer is not available for this rule.

In most cases, this rule will be aliased as ↔E.

Availability

Deductions Default (BD)

Custom: Select "BD" from Preferences > Rules.

Variants

Biconditional Elimination (Rule), Df (Rule)

Conjunction Elimination/Restricted (&ER, ∧ER, ⦁ER)

Example

Discussion

If the formula at [b] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

This rule differs from conjunction elimination in that only the left conjunct is inferred. In most cases, this rule is aliased as Simp.

Availability

Deductions Default (&ER)

Custom: Select "&ER" from Preferences > Rules.

Variants

&E (Rule), &ER (Rule), Simp/&E (Alias), Simp/&ER (Alias)

Disjunction Introduction/Restricted (∨IR)

Example

Discussion

Autoinfer is not available for this rule.

This rule differs from disjunction introduction in that the added disjunct is only on the right. In most cases, this rule is aliased as Add.

Availability

Deductions Default (∨IR)

Custom: Select "∨IR" from Preferences > Rules.

Variants

Disjunction Introduction (Rule), Disjunction Introduction/Restricted (Rule), Addition/∨I (Alias), Addition/∨IR (Alias)

Universal Introduction (∀I)

Example

Discussion

Autoinfer is not available for this rule. n is either an arbitrary constant or a free variable (depending on language parameters).

The following restrictions apply to universal introduction: (i) x in [b] must replace every instance of n in [a], (ii) x may not appear in [a] and n may not appear in [b], and (iii) n may not appear in any premise or undischarged assumption.

Availability

Deductions Default (∀I), The Logic Book (∀I), Accessible Introduction (∀I), Logics (∀I), Logic Primer (UI), Symbolic Logic (∀I), Modern Logic (∀I), MacLogic (∀I)

Custom: Select "∀I" from Preferences > Rules.

Variants

∀I (Rule), UG (Rule), UG/∀I (Alias)

Universal Elimination (∀E)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Deductions Default (∀E), The Logic Book (∀E), Accessible Introduction (∀E), Logics (∀E), Logic Primer (UI), Symbolic Logic (∀E), Modern Logic (∀E), MacLogic (∀E)

Custom: Select "∀E" from Preferences > Rules.

Variants

UI (Alias)

Existential Introduction (∃I)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Deductions Default (∃I), The Logic Book (∃I), Accessible Introduction (∃I), Logics (∃I), Logic Primer (EG), Symbolic Logic (∃I), Modern Logic (∃I), MacLogic (∃I)

Custom: Select "∃I" from Preferences > Rules.

Variants

∃I (Rule), EG/∃I (Alias)

Existential Elimination (∃E)

Example

Discussion

Autoinfer is not available for this rule. n is either an arbitrary constant or a free variable (depending on language parameters).

The following restrictions apply to existential elimination: (i) n in [b] must replace every instance of x in [a], (ii) n may not appear in [c] or [d], and (iii) n does not appear in any premise or undischarged assumption.

Availability

Deductions Default (∃E), The Logic Book (∃E), Accessible Introduction (∃E), Logics (∃E), Logic Primer (EI), Symbolic Logic (∃E), Modern Logic (∃E), MacLogic (∃E)

Custom: Select "∃E" from Preferences > Rules.

Variants

∃E (Rule), EI (Rule), EI (Alias)

Identity Introduction (=I)

Example

Discussion

Autoinfer is not available for this rule.

No lines are cited in the justification of =I.

Availability

Deductions Default (=I), The Logic Book (=I), Accessible Introduction (=I), Logics (=I), Logic Primer (=I), Symbolic Logic (=I), Modern Logic (=I), MacLogic (=I)

Custom: Select "=I" from Preferences > Rules.

Variants

=I (Rule), Id (Rule), IR/=I (Alias)

Identity Elimination (=E)

Example

Discussion

The justification takes the form "a,b =E", where [a] is the identity formula. If the lines are cited in reverse order (i.e., "b,a =E"), Deductions will flip the order (autocorrect).

Availability

Deductions Default (=E), The Logic Book (=E), Accessible Introduction (=E), Logics (=E), Logic Primer (=E), Symbolic Logic (=E), Modern Logic (=E), MacLogic (=E)

Custom: Select "=E" from Preferences > Rules.

Variants

=E (Rule), Id (Rule), ID/=E (Alias)

Universal Generalization (UG)

Example

Discussion

Autoinfer is not available for this rule. n is either an arbitrary constant or a free variable (depending on language parameters).

The following restrictions apply to universal generalization: (i) x in [b] must replace every instance of n in [a], (ii) x may not appear in [a] and n may not appear in [b], (iii) n may not appear in any premise or undischarged assumption, and (iv) n does not appear free in any previous line derived by existential instantiation (EI, Rule).

Availability

Deductions Default (UG), Introduction to Logic (UG), Logic and Philosophy (UG), The Power of Logic (UG), A Concise Introduction to Logic (UG)

Custom: Select "UG" from Preferences > Rules.

Variants

∀I (Rule), UG (Rule), UG/∀I (Alias)

Existential Instantiation (EI)

Example

Discussion

Autoinfer is not available for this rule. n is either an arbitrary constant or a free variable (depending on language parameters).

Availability

Deductions Default (EI), Introduction to Logic (EI), Logic and Philosophy (EI), The Power of Logic (EI), A Concise Introduction to Logic (EI)

Custom: Select "EI" from Preferences > Rules.

Variants

∃E (Rule), EI (Rule), EI (Alias)

Quantifier Shift (QS)

Example

Discussion

Autoinfer is not available for this rule.

This rule is not an equivalence rule. See Change of Quantifier (CQ) for the related equivalence rule.

Availability

Deductions Default (QS), Modern Logic (QS), MacLogic (QS)

Custom: Select "QS" from Preferences > Rules.

Variants

QS (Rule), CQ (Rule), QN/QS (Alias), QN/CQ (Alias)

Identity (Id)

Example

Discussion

Autoinfer is not available for this rule.

Identity is a hybrid rule with three different schemata. The schema followed is determined by the number of lines cited in the justification: with no lines cited, the Id rule follows identity introduction (=I); with one line cited, the Id rule follows identity equivalence (IdE); with two lines cited, the Id rule follows identity elimination (=E).

Availability

Deductions Default (Id), A Concise Introduction to Logic (Id)

Custom: Select "Id" from Preferences > Rules.

Variants

=I (Rule), =E (Rule), Id (Rule), IR/=I (Alias), ID/=E (Alias)

Change of Quantifier (CQ)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

This is not an inference rule. See Quantifier Shift (QS) for the related inference rule.

Availability

Deductions Default (CQ), A Concise Introduction to Logic (CQ)

Custom: Select "CQ" from Preferences > Rules.

Variants

QS (Rule), CQ (Rule), QN/QS (Alias), QN/CQ (Alias)

Identity Equivalence (IdE)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (IdE)

Custom: Select "IdE" from Preferences > Rules.

Variants

Id (Rule)

Existential Instantiation/Restricted (EIR)

Example

Discussion

Autoinfer is not available for this rule. n is a constant. This rule is "restricted" in the sense that n may not be a free variable, even if free variables are permitted in the language. In most cases, this rule will be aliased as EI, and is combined with UG and a language that permits free variables (but not arbitrary constants).

Availability

Deductions Default (EIR),

Custom: Select "EIR" from Preferences > Rules.

Variants

Existential Elimination (Rule)

Double Negation Equivalence (DNE)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (DNE)

Custom: Select "DNE" from Preferences > Rules.

Variants

DN (Rule)

DeMorgan's Theorem (DeM)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (DeM)

Custom: Select "DeM" from Preferences > Rules.

Variants

None

Commutation (Comm)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Comm), Introduction to Logic (Comm), Logic and Philosophy (Comm), The Power of Logic (Comm), A Concise Introduction to Logic (Comm)

Custom: Select "Comm" from Preferences > Rules.

Variants

None

Association (Assoc)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Assoc), Introduction to Logic (Assoc), Logic and Philosophy (Assoc), The Power of Logic (Assoc), A Concise Introduction to Logic (Assoc)

Custom: Select "Assoc" from Preferences > Rules.

Variants

None

Distribution (Dist)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Dist), Introduction to Logic (Dist), Logic and Philosophy (Dist), The Power of Logic (Dist), A Concise Introduction to Logic (Dist)

Custom: Select "Dist" from Preferences > Rules.

Variants

None

Tautology (Taut)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Taut), Introduction to Logic (Taut), Logic and Philosophy (Taut), The Power of Logic (Taut), A Concise Introduction to Logic (Taut)

Custom: Select "Taut" from Preferences > Rules.

Variants

Re/Taut (Alias)

Implication (Impl)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Impl), Introduction to Logic (Impl), Logic and Philosophy (Impl), The Power of Logic (Impl), A Concise Introduction to Logic (Impl)

Custom: Select "Impl" from Preferences > Rules.

Variants

None

Exportation (Exp)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Exp), Introduction to Logic (Exp), Logic and Philosophy (Exp), The Power of Logic (Exp), A Concise Introduction to Logic (Exp)

Custom: Select "Exp" from Preferences > Rules.

Variants

None

Contraposition (Contra)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Contra), Introduction to Logic (Contra), Logic and Philosophy (Contra), The Power of Logic (Contra), A Concise Introduction to Logic (Contra)

Custom: Select "Contra" from Preferences > Rules.

Variants

None

Material Equivalence (Equiv)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

Deductions Default (Equiv), Introduction to Logic (Equiv), Logic and Philosophy (Equiv), The Power of Logic (Equiv), A Concise Introduction to Logic (Equiv)

Custom: Select "Equiv" from Preferences > Rules.

Variants

None

Conjunction/&I (Conj)

Example

Discussion

The justification takes the form "a,b Conj", where [a] is the left conjunct and [b] is the right conjunct of [c]. If the lines are cited in reverse order (i.e., "b,a Conj"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Introduction to Logic (Conj), Logic and Philosophy (Conj), The Power of Logic (Conj), A Concise Introduction to Logic (Conj)

Custom: Select "Rename &I as Conj" from Preferences > Aliases.

Variants

&I (Rule)

Simplification/&E (Simp)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Logic and Philosophy (Simp), The Power of Logic (Simp)

Custom: Select "Rename &E as Simp" from Preferences > Aliases.

Variants

&E (Rule), &ER (Rule), Simp/&E (Alias), Simp/&ER (Alias)

Conditional Proof/→I (CP)

Example

Discussion

The justification takes the form "a,b CP", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a CP"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

Availability

Introduction to Logic (CP), Logic and Philosophy (CP), The Power of Logic (CP), A Concise Introduction to Logic (CP)

Custom: Select "Rename →I as CP" from Preferences > Aliases.

Variants

→I (Rule)

Modus Ponens/→E (MP)

Example

Discussion

The justification takes the form "a,b MP", where [a] is the conditional and [b] is the antecedent of the conditional. If the lines are cited in reverse order (i.e., "b,a MP"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Introduction to Logic (MP), Logic and Philosophy (MP), The Power of Logic (MP), A Concise Introduction to Logic (MP)

Custom: Select "Rename →E as MP" from Preferences > Aliases.

Variants

→E (Rule)

Addition/∨I (Add)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Logic and Philosophy (Add), The Power of Logic (Add)

Custom: Select "Rename ∨I as Add" from Preferences > Rules.

Variants

Disjunction Introduction (Rule), Disjunction Introduction/Restricted (Rule), Addition/∨I (Alias), Addition/∨IR (Alias)

Disjunction Elimination/DS (∨E)

Example

Discussion

The justification takes the form "a,b ∨E", where [a] is a disjunction, and [b] is the negation of the left or right disjunct. If the lines are cited in reverse order (i.e., "b,a ∨E"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Logic Primer (∨E)

Custom: Select "Rename DS as ∨E" from Preferences > Rules.

Variants

DS (Rule)

Biconditional Introduction/BC (↔I, ≡I)

Example

Discussion

If the formula at [b] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

This rule takes a conjunction and infers a biconditional. The left and right sides of the biconditional formula have an order that corresponds to the antecedent and consequent of the left conjunct of the conjunction.

Availability

Logic Primer (≡I), Logics (↔I)

Custom: Select "Rename BC as ↔I" from Preferences > Rules.

Variants

Biconditional Introduction (Rule), Df (Rule), Biconditional Composition (Rule)

Biconditional Elimination/BD (↔E, ≡E)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Logic Primer (≡E), Logics (↔E)

Custom: Select "Rename BD as ↔E" from Preferences > Rules.

Variants

Biconditional Elimination (Rule), Df (Rule), Biconditional Decomposition (Rule)

Constructive Dilemma/CDC (CD)

Example

Discussion

The justification takes the form "a,b CD", where [a] is a disjunction, and [b] is a conjunction of conditionals. The antecedent of the left conditional is the same as the left disjunct of [a], and the antecedent of the right conditional is the same as the right disjunct of [a]. If the lines are cited in reverse order (i.e., "b,a CD"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

Availability

Introduction to Logic (CDC), A Concise Introduction to Logic (CDC) Custom: Select "Rename CD as CDC" from Preferences > Rules.

Variants

CD (Rule)

Redundancy/Taut (Re)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

Availability

The Power of Logic (Re)

Custom: Select "Rename Taut as Re" from Preferences > Aliases.

Variants

Taut (Rule)

Simplification/&ER (Simp)

Example

Discussion

If the formula at [b] is left blank but the justification is entered, Deductions will infer the formula (autoinfer).

This rule differs from conjunction elimination in that only the left conjunct is inferred.

Availability

Introduction to Logic (Simp), A Concise Introduction to Logic (Simp)

Custom: Select "Rename &ER as Simp" from Preferences > Aliases.

Variants

&E (Rule), &ER (Rule), Simp/&E (Alias), Simp/&ER (Alias)

Addition/∨IR (Add)

Example

Discussion

Autoinfer is not available for this rule.

This rule differs from disjunction introduction in that the added disjunct is only on the right.

Availability

Introduction to Logic (Add), A Concise Introduction to Logic (Add)

Custom: Select "Rename ∨IR as Add" from Preferences > Aliases.

Variants

Disjunction Introduction (Rule), Disjunction Introduction/Restricted (Rule), Addition/∨I (Alias), Addition/∨IR (Alias)

Negation Introduction/~IP (~I, ¬I)

Example

Discussion

The justification takes the form "a,b ~I", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~I"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This negation introduction rule is "primitive" in the sense that its schema does not involve any connective other than the negation. The successful use of this rule depends, in many cases, on a rule that is able to generate the contradiction symbol ("Λ") (such as ~EP).

Availability

Modern Logic (~I)

Custom: Select "Rename ~IP as ~I" from Preferences > Aliases.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~IE/RAA (Alias)

Negation Elimination/~EP (~E, ¬E)

Example

Discussion

The justification takes the form "a,b ~E", where [a] is a negation, and [b] is the main subformula of that negation. If the lines are cited in reverse order (i.e., "b,a ~E"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer "Λ" (autoinfer).

This negation elimination rule is "primitive" in the sense that its schema does not involve any connective other than the negation.

Availability

Modern Logic (~E)

Custom: Select "Rename ~EP as ~E" from Preferences > Aliases.

Variants

~E (Rule), ~EC (Rule), ~EP (Rule), RAA (Rule), ~E/~EP (Alias), ~E/~EC (Alias), IP/~EC (Alias), ~IE/RAA (Alias)

Negation Introduction/~IC (~I, ¬I)

Example

Discussion

The justification takes the form "a,b ~I", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~I"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation introduction rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as & or Conj).

Availability

Deductions Default (~IC)

Custom: Select "Rename ~IC as ~I" from Preferences > Aliases.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~IE/RAA (Alias)

Negation Elimination/~EC (~E, ¬E)

Example

Discussion

The justification takes the form "a,b ~E", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a ~E"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation introduction rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as &I or Conj).

Availability

Deductions Default (~EC)

Custom: Select "Rename ~EC as ~E" from Preferences > Aliases.

Variants

~E (Rule), ~EC (Rule), ~EP (Rule), RAA (Rule), ~E/~EP (Alias), ~E/~EC (Alias), IP/~EC (Alias), ~IE/RAA (Alias)

Indirect Proof/~IC (IP)

Example

Discussion

The justification takes the form "a,b IP", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a IP"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation introduction rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as & or Conj).

Availability

Deductions Default (~IC)

Custom: Select "Rename ~IC as IP" from Preferences > Aliases.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~IE/RAA (Alias)

Indirect Proof/~EC (IP)

Example

Discussion

The justification takes the form "a,b IP", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b,a IP"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation introduction rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as &I or Conj).

Availability

Deductions Default (~EC)

Custom: Select "Rename ~EC as IP" from Preferences > Aliases.

Variants

~E (Rule), ~EC (Rule), ~EP (Rule), RAA (Rule), ~E/~EP (Alias), ~E/~EC (Alias), IP/~EC (Alias), ~IE/RAA (Alias)

Negation Intro-Elim/RAA (~IE, ¬IE)

Example

Discussion

The justification takes the form "a-b ~IE", where [a] is an assumption that is discharged at [b]. If the lines are cited in reverse order (i.e., "b-a ~IE"), Deductions will flip the order (autocorrect). If the formula at [c] is left blank but the justification is entered, Deductions will infer the formula (autoinfer). If the assumption is left undischarged, Deductions will mark it as discharged (autodischarge).

This is a Fitch-style negation rule, where the contradiction appears as a conjunction on a single line. As such, the successful use of this rule depends, in many cases, on a rule that will generate conjunctions (such as &I or Conj). ~IE functions an inclusive disjunction of negation introduction/conjunction and negation elimination/conjunction: if the sequent is valid on either ~IC or ~EC, it will be valid on ~IE.

Availability

Deductions Default (RAA)

Custom: Select "Rename RAA as ~IE" from Preferences > Aliases.

Variants

~I (Rule), ~IC (Rule), ~IP (Rule), RAA (Rule), ~I/~IP (Alias), ~I/~IC (Alias), IP/~IC (Alias), ~IE/RAA (Alias)

Universal Generalization/∀I (UG)

Example

Discussion

Autoinfer is not available for this rule. n is either an arbitrary constant or a free variable (depending on language parameters).

The following restrictions apply to universal introduction: (i) x in [b] must replace every instance of n in [a], (ii) x may not appear in [a] and n may not appear in [b], and (iii) n may not appear in any premise or undischarged assumption.

Availability

Deductions Default (∀I), The Logic Book (∀I), Accessible Introduction (∀I), Logics (∀I), Logic Primer (UI), Symbolic Logic (∀I), Modern Logic (∀I), MacLogic (∀I)

Custom: Select "Rename ∀I as UG" from Preferences > Aliases.

Variants

∀I (Rule), UG (Rule), UG/∀I (Alias)

Universal Instantiation/∀E (UI)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Deductions Default (∀E), The Logic Book (∀E), Accessible Introduction (∀E), Logics (∀E), Logic Primer (UI), Symbolic Logic (∀E), Modern Logic (∀E), MacLogic (∀E)

Custom: Select "Rename ∀E as UI" from Preferences > Aliases.

Variants

∀I (Rule), UG (Rule), UG/∀I (Alias)

Existential Generalization/∃I (EG)

Example

Discussion

Autoinfer is not available for this rule.

Availability

Deductions Default (∃I), The Logic Book (∃I), Accessible Introduction (∃I), Logics (∃I), Logic Primer (EG), Symbolic Logic (∃I), Modern Logic (∃I), MacLogic (∃I)

Custom: Select "Rename ∃I as EG" from Preferences > Aliases.

Variants

∃I (Rule), EG/∃I (Alias)

Existential Instantiation/∃E (EI)

Example

Discussion

Autoinfer is not available for this rule. n is either an arbitrary constant or a free variable (depending on language parameters).

The following restrictions apply to existential elimination: (i) n in [b] must replace every instance of x in [a], (ii) n may not appear in [c] or [d], and (iii) n does not appear in any premise or undischarged assumption.

Availability

Deductions Default (∃E), The Logic Book (∃E), Accessible Introduction (∃E), Logics (∃E), Logic Primer (EI), Symbolic Logic (∃E), Modern Logic (∃E), MacLogic (∃E)

Custom: Select "Rename ∃E as EI" from Preferences > Aliases.

Variants

∃E (Rule), EI (Rule), EI (Alias)

IR/=I (IR)

Example

Discussion

Autoinfer is not available for this rule.

No lines are cited in the justification of IR.

Availability

Deductions Default (=I), The Logic Book (=I), Accessible Introduction (=I), Logics (=I), Logic Primer (=I), Symbolic Logic (=I), Modern Logic (=I), MacLogic (=I)

Custom: Select "Rename =I as IR" from Preferences > Aliases.

Variants

=I (Rule), Id (Rule), IR/=I (Alias)

Identity/=E (ID)

Example

Discussion

The justification takes the form "a,b ID", where [a] is the identity formula. If the lines are cited in reverse order (i.e., "b,a ID"), Deductions will flip the order (autocorrect).

Availability

Deductions Default (=E), The Logic Book (=E), Accessible Introduction (=E), Logics (=E), Logic Primer (=E), Symbolic Logic (=E), Modern Logic (=E), MacLogic (=E)

Custom: Select "Rename =E as ID" from Preferences > Aliases.

Variants

=E (Rule), Id (Rule), ID/=E (Alias)

Quantifier Negation/QS (QN)

Example

Discussion

Autoinfer is not available for this rule.

This rule is not an equivalence rule. See Change of Quantifier (CQ) for the related equivalence rule.

Availability

Deductions Default (QS), Modern Logic (QS), MacLogic (QS)

Custom: Select "Rename QS as QN" from Preferences > Aliases.

Variants

QS (Rule), CQ (Rule), QN/QS (Alias), QN/CQ (Alias)

Quantifier Negation/CQ (QN)

Example

Discussion

This rule is an equivalence rule. Autoinfer is not available for this rule.

This is not an inference rule. See Quantifier Shift (QS) for the related inference rule.

Availability

Deductions Default (CQ), A Concise Introduction to Logic (CQ)

Custom: Select "CQ" from Preferences > Rules.

Variants

QS (Rule), CQ (Rule), QN/QS (Alias), QN/CQ (Alias)

Existential Instantiation/EIR (EI)

Example

Discussion

Autoinfer is not available for this rule. n is a constant. This rule is "restricted" in the sense that n may not be a free variable, even if free variables are permitted in the language. In most cases, this rule is combined with UG and a language that permits free variables (but not arbitrary constants).

Availability

Deductions Default (EIR),

Custom: Select "Rename EIR as EI" from Preferences > Aliases.

Variants

Existential Elimination (Rule)