Copy-Test

This is a list of rules of inference, logical laws that relate to mathematical formulae.

Contents 1 Introduction 2 Rules for classical sentential calculus 2.1 Rules for negations 2.2 Rules for conditionals 2.3 Rules for conjunctions 2.4 Rules for disjunctions 2.5 Rules for biconditionals 3 Rules of classical predicate calculus 4 Table: Rules of Inference - a short summary 4.1 Example 1 4.2 Example 2 5 References

[edit] Introduction

Rules of inference are syntactical transform rules which one can use to infer a conclusion from a premise to create an argument. A set of rules can be used to infer any valid conclusion if it is complete, while never inferring an invalid conclusion, if it is sound. A sound and complete set of rules need not include every rule in the following list, as many of the rules are redundant, and can be proven with the other rules.

Discharge rules permit inference from a subderivation based on a temporary assumption. Below, the notation

indicates such a subderivation from the temporary assumption to .

[edit] Rules for classical sentential calculus

Sentential calculus is also known as propositional calculus.

[edit] Rules for negations

Reductio ad absurdum (or Negation Introduction)

Reductio ad absurdum (related to the law of excluded middle)

Noncontradiction (or Negation Elimination)

Double negation elimination

Double negation introduction

[edit] Rules for conditionals

Deduction theorem (or Conditional Introduction)

Modus ponens (or Conditional Elimination)

Modus tollens

[edit] Rules for conjunctions

Adjunction (or Conjunction Introduction)

Simplification (or Conjunction Elimination)

[edit] Rules for disjunctions

Addition (or Disjunction Introduction)

Case analysis

Disjunctive syllogism

[edit] Rules for biconditionals

Biconditional introduction

Biconditional Elimination

[edit] Rules of classical predicate calculus

In the following rules, is exactly like except for having the term everywhere has the free variable .

Universal Introduction (or Universal Generalization)

Restriction 1: does not occur in .
Restriction 2: is not mentioned in any hypothesis or undischarged assumptions.

Universal Elimination (or Universal Instantiation)

Restriction: No free occurrence of in falls within the scope of a quantifier quantifying a variable occurring in .

Existential Introduction (or Existential Generalization)

Restriction: No free occurrence of in falls within the scope of a quantifier quantifying a variable occurring in .

Existential Elimination (or Existential Instantiation)

Tags:   testing