Systems of Formal Deduction



Systems of Formal Deduction

Inference Rules

Systems of formal deduction (or formal derivation, or formal proof) consist of a set of formal inference rules. The inference rules are formal in the sense that they allow sentences to be derived from other sentences on the basis of the formal structure of those sentences. For example, an inference rule can state that when you have a sentence of the form (((, then you can derive the sentence ( from that.

Normally, the inference rules try and capture basic and valid inferences that we make when we reason. In the example above, ( is indeed logically implied by (((, and this is a very basic inference. For this reason, systems of formal deduction are sometimes called systems of natural deduction. It is important to keep in mind, however, that we can define inference rules in any way we want. Thus, we could add a non-basic (though valid) inference rule that says that you can infer ( ( ( from ( ( (( ( (( and (( ( (( ( (. More importantly, we could define an invalid inference rule that says that you can infer ( from ( ( ( and (. In other words, while normally the inference rules in some system of formal deduction capture inferences that are both basic and valid, we cannot assume this.

Obviously, systems of formal deduction differ in that they have different sets of inference rules. As such, we are going to define a formal proof relative to any system S:

A formal proof in system S is a sequence of sentences, starting with a set of sentences ( (usually called premises or assumptions), and ending with a sentence ( (usually called the conclusion), where each sentence ( in the sequence after ( is derived from a subset of the sentences in the sequence before ( by the application of some inference rule as defined by S. If there exists a formal proof in S from ( to (, we write ( ⊢S (.

Many systems of derivation have rules that deal with what are called subproofs. A subproof can be started at any point during a formal proof by making some additional assumption. Sentences that are derived from that point on are said to be within the scope of that assumption, until the subproof is closed. Once the subproof is closed, none of the sentences that occur within that subproof can be used to derive further sentences. Subproofs can be started within subproofs. Subproofs need to be closed one at a time, and any subproof within a subproof (the ‘inner’ subproof’) should be closed before the ‘outer’ subproof is closed. Although we will not do so here, the definition of a formal proof obviously needs to be modified to account for subproofs.

In general, then, an inference rule can be written as {(1 , ( ,(n} ⊢ (, which indicates that ( can be derived from (1 , ( ,(n , where each (i is either a sentence or a subproof (written as ( ⊢ (, where ( is the assumption of that subproof and ( the last sentence of that subproof) that occurs anywhere earlier in the proof but not within the scope of some subproof that has been closed.

Example: The System F

System F, as defined in “Language, Proof, and Logic” by Jon Barwise and John Etchemendy, contains the following inference rules:

|Conjunction Elimination ( ( Elim ) |Conjunction Introduction ( ( Intro ) |

| | |

|{( ( (} |{(, (} |

|⊢ ( (or () |⊢ ( ( ( |

|Disjunction Elimination ( ( Elim ) |Disjunction Introduction ( ( Intro ) |

| | |

|{( ( ( , ( ⊢ (, ( ⊢ (} |{( (or ()} |

|⊢ ( |⊢ ( ( ( |

|Negation Elimination ( ( Elim ) |Negation Introduction ( ( Intro ) |

| | |

|{(((} |{( ⊢ (} |

|⊢ ( |⊢ (( |

|Contradiction Elimination ( ( Elim ) |Contradiction Introduction ( ( Intro ) |

| | |

|{(} |{(, ((} |

|⊢ ( |⊢ ( |

|Conditional Elimination ( ( Elim ) |Conditional Introduction ( ( Intro ) |

| | |

|{( ( (, (} |{( ⊢ (} |

|⊢ ( |⊢ ( ( ( |

|Biconditional Elimination ( ( Elim ) |Biconditional Introduction ( ( Intro ) |

| | |

|{( ( ( (or ( ( (), (} |{( ⊢ (, ( ⊢ (} |

|⊢ ( |⊢ ( ( ( |

A final rule is Reiteration, which is {(} ⊢ (.

The inference pattern of ( Elim is also called Proof by Cases, the inference pattern of ( Intro is known as Proof by Contradiction, Indirect Proof, or Reductio ad Absurdum, and the inference pattern of ( Intro as Conditional Proof.

Other Fitch-Style Derivational Systems, and Derivational Equivalence

System F is what is called a Fitch-style system. Fitch-style systems have a single elimination and an introduction rule for every truth-functional connective (possibly including ().

Another Fitch-style system is SD, as defined in “The Logic Book”, by Merrie Bergmann, James Moor, and Jack Nelson. SD has the same inference rules as F, except that the Negation Elimination rule in SD is defined as {(( ⊢ (} ⊢ (.

(Actually, the syntax of the sentences over which SD is defined uses ~ for (, & for (, ( for (, ( for (, and does not have (. Thus, Negation Introduction is actually defined as {( ⊢ (, ( ⊢ ~(} ⊢ ~(, and the Negation Elimination rule as {~( ⊢ (, ~( ⊢ ~(} ⊢ (. For the point I am about to make though, this is not important.)

Now, an obvious question to ask is: Can the two systems derive the same things, or is there anything that can be derived in F, but not in SD (or vice versa)? To be precise, is it the case that for any set of sentences ( and any sentence, ( ⊢F ( iff ( ⊢SD (?

It turns out that the answer to this question is “Yes”. To demonstrate this, we will demonstrate that SD can do whatever F accomplishes with its Negation Elimination rule, and vice versa. From this, the result immediately follows.

First, here’s how we can do SD’s Negation Elimination in F:

(( ⊢ (

((( (( Intro)

( (( Elim)

Second, here’s how we can do F’s Negation Elimination in SD:

(((

(( (assumption)

← (( Intro)

( (( Elim)

Because ( ⊢F ( iff ( ⊢SD (, we say that F and SD are derivationally equivalent.

Non-Fitch-style Systems

Non-Fitch-style systems do not restrict themselves to having a single Elimination and Introduction rule for each connective. As such, these kinds of systems can have other valid and basic inference rules. This usually makes them less mathematically elegant, but much easier to use. Below is a list of typical rules of inference. Most Non-Fitch-style systems use some subset of these:

|Modus Ponens (MP) |Modus Tollens (MT) |

| | |

|{( ( (, (} |{( ( (, ((} |

|⊢ ( |⊢ (( |

|Disjunctive Syllogism (DS) |Hypothetical Syllogism (HS) |

| | |

|{( ( ( , (( (or (() } |{( ( (, ( ( (} |

|⊢ ( (or () |⊢ ( ( ( |

|Simplification (Simp) |Conjunction (Conj) |

| | |

|{( ( (} |{(, (} |

|⊢ ( (or () |⊢ ( ( ( |

|Constructive Dilemma (CD) |Destructive Dilemma (DD) |

| | |

|{( ( (, ( ( (, ( ( (} |{( ( (, ( ( (, (( ( ((} |

|⊢ ( ( ( |⊢ (( ( (( |

|Addition (Add) |Absorption (Abs) |

| | |

|{( (or ()} |{( ( (} |

|⊢ ( ( ( |⊢ ( ( (( ( () |

|Weakening the Consequent (Weakening) |Strengthening the Antecedent (Strengthening) |

| | |

|{( ( (( ( ()} |{( ( (} |

|⊢ ( ( ( |⊢ (( ( () ( ( |

|Conditional Proof (CP) |Indirect Proof (IP) |

| | |

|{( ⊢ (} |{( ⊢ (, ( ⊢ ((} |

|⊢ ( ( ( |⊢ (( |

Generalized Inference Rules

Some of the inference rules can be generalized by considering generalized conjunctions or generalized disjunctions, or by considering multiple statements.

|Generalized Simplification |Generalized Conjunction |

| | |

|{(1 ( ( ( (i ( ( ( (n} |{(1 , ( , (n} |

|⊢ (i |⊢ (1 ( ( ( (n |

|Generalized Proof by Cases |Generalized Addition |

| | |

|{(1 ( ( ( (n , (1 ⊢ (, (, (n ⊢ (} |{(i} |

|⊢ ( |⊢ (1 ( ( ( (i ( ( ( (n |

|Generalized Disjunctive Syllogism |Generalized Hypothetical Syllogism |

| | |

|{(1 ( ( ( (i ( ( ( (n , |{(1 ( (2, (2 ( (3, (, (n-1 ( (n} |

|((1, (, ((i -1, ((i +1( ,((n } |⊢ (1 ( (n |

|⊢ (i | |

|Generalized Constructive Dilemma |Generalized Destructive Dilemma |

| | |

|{(1 ( (1,(, (n ( (n, (1 ( ( ( (n} |{(1 ( (1,(, (n ( (n, ((1 ( ( ( ((n } |

|⊢ (1 ( ( ( (n |⊢ ((1 ( ( ( ((n |

Notice that with these generalizations, Modus Ponens has become a special case of Generalized Constructive Dilemma, and Modus Tollens a special case of Generalized Destructive Dilemma.

In F, Conjunction Elimination and Introduction are in fact respectively defined as Generalized Simplification and Generalized Conjunction, and Disjunction Elimination and Introduction as Generalized Proof by Cases and Generalized Addition. For theoretical as well as practical purposes, however, we will not consider any such generalized rules when doing metatheory.

Rules of Equivalence

Besides rules of inference, non-Fitch-style systems usually also make use of rules of equivalence. Rules of equivalence are inference rules as well, but they are of a somewhat different nature. Rules of equivalence allow one to use the Principle of Substitution of Logical Equivalents on any sentence, and to infer the result from the original sentence. The rules of equivalence state which equivalences can be used to perform this substitution. Typical equivalences used in non-Fitch-style derivational systems are:

|Double Negation (DN) |Idempotence (Idem) |

| | |

|( ( ((( |( ( ( ( ( |

| |( ( ( ( ( |

|Commutation (Com) |Association (Assoc) |

| | |

|( ( ( ( ( ( ( |( ( (( ( () ( (( ( () ( ( |

|( ( ( ( ( ( ( |( ( (( ( () ( (( ( () ( ( |

|Distribution (Dist) |DeMorgan (DeM) |

| | |

|( ( (( ( () ( (( ( () ( (( ( () |((( ( (( ( (( ( (( |

|( ( (( ( () ( (( ( () ( (( ( () |((( ( (( ( (( ( (( |

|Transposition (Trans) |Exportation (Exp) |

| | |

|( ( ( ( (( ( (( |( ( (( ( (( ( (( ( (( ( ( |

|Implication (Impl) |Equivalence (Equiv) |

| | |

|( ( ( ( (( ( ( |( ( ( ( (( ( (( ( (( ( (( |

|((( ( () ( ( ( (( |( ( ( ( (( ( (( ( ((( ( ((( |

|Subsumption (Sub) | |

| | |

|( ( (( ( () ( ( | |

|( ( (( ( () ( ( | |

Rules of Equivalence differ in two ways from rules of inference:

1. Rules of Inference go one way only, whereas rules of equivalence go both ways

2. Rules of Inference apply to whole sentences only, whereas rules of equivalence can be applied to component parts.

Examples: C1, C2, and H

In “Symbolic Logic”, 5th ed., Irving Copi defines a non-Fitch-style derivational system (I’ll call it C1) with the following Rules:

Rules of Inference: MP, MT, DS, HS, Simp, Conj, Add, CD, DD

Rules of Equivalence: DN, Idem, Com, Assoc, Dist, DeM, Trans, Exp, Impl, Equiv

Rules of Subproof: CP, IP

In “Introduction to Logic”, 11th ed., Irving Copi and Carl Cohen define (C2):

Rules of Inference: MP, MT, DS, HS, Simp, Conj, Add, CD, Abs

Rules of Equivalence: DN, Idem, Com, Assoc, Dist, DeM, Trans, Exp, Impl, Equiv

Rules of Subproof: CP, IP

In “A Concise Introduction to Logic”, Patrick Hurley uses (H):

Rules of Inference: MP, MT, DS, HS, Simp, Conj, Add, CD

Rules of Equivalence: DN, Idem, Com, Assoc, Dist, DeM, Trans, Exp, Impl, Equiv

Rules of Subproof: CP, IP

In “Introductory Modal Logic”, Kenneth Konyndyk uses (K):

Rules of Inference: MP, MT, DS, HS, Simp, Conj, Add

Rules of Equivalence: DN, Idem, Com, Assoc, Dist, DeM, Trans, Exp, Impl, Equiv

Rules of Subproof: CP, IP

Theorem: for any ( and (: ( ⊢C1 ( iff ( ⊢C2 ( iff ( ⊢H ( iff ( ⊢K (

Proof: Easy, and left to reader

Theorem: for any ( and (: ( ⊢F ( iff ( ⊢K (

Proof: Unfortunately, there is no straightforward way to prove that ( ⊢F ( if ( ⊢K ( because it is not clear how one would emulate the equivalence rules of K in F. However, it is pretty straightforward to show that ( ⊢K ( if ( ⊢F (. We’ll do the other half later!

Homework: Define system B (Bram) as follows:

Rules of Inference: MP, Simp, Conj, Add

Rules of Equivalence: DN, Idem, Com, Assoc, Dist, DeM, Trans, Exp, Impl, Equiv

Rules of Subproof: CP

Show that for any ( and (: ( ⊢B ( iff ( ⊢K (

................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download