FOL Inference Rules

Philosophy 202

The inference rules that follow enable us to prove that sentences are logical consequences of other sentences, or what is the same, that arguments are valid. As such, these rules constitute a formal deductive system, which is a framework consisting of inference rules in which one constructs proofs.

The deductive system we develop and use in this class is not the only one available; in fact, there are as many deductive systems as there are combinations of inference rules. Selection of one system from among the many options is usually guided by three factors: (a) strength of the system (i.e., the number of different types of claims that can be proven within the system), (b) parsimony---we would like to say as much as we can with the fewest rules possible, and (c) convenience. In the next logic class, the focus would be on the properties of deductive systems generally.

In Chapter 2, two of the rules concern the predicate "=". We introduce rules for this predicate because we are studying the structure of first-order languages in general, and = is the one predicate that shows up in most particular first-order languages. If we were concentrating on a specific first-order language, we would introduce inference rules involving other predicates.

In the remaining chapters, the rules concern the connectives and quantifiers. Notice that for each new syntactical device there is an introduction and an elimination rule. This has a ready explanation: you will occasionally need to derive a sentence with a particular piece of syntax in it from sentences that do not contain that piece, and for this you will need introduction rules; on the other hand, you will occasionally want to derive a sentence that lacks a certain piece of syntax from a sentence or sentences containing it, and for this you will need elimination rules.

CHAPTER TWO RULES

2.1: Reflexivity of Identity: One can validly infer a sentence of the form n=n from any premise whatsoever or from no premises at all.

2.2: Indiscernibility of Identity: If n=m can be established, anything that holds of n can be asserted to hold of m.

2.3: Reiteration: If you have already inferred a sentence P, you can validly reassert it.

CHAPTER FOUR & SIX RULES

4.1: Substitution of Logical Equivalents: If you have proven some sentence P, you may assert any sentence Q that you have established is logically equivalent to P.

4.2: Assertion of Logical Truth: If you have established that some sentence P is a logical truth, you may assert it at any point in a proof.

6.1: Conjunction Elimination: If you have established P & Q, you may assert P and you may assert Q.

6.2: Conjunction Introduction: IF you have established P and you have established Q, then you may assert P & Q.

6.3:* Disjunction Elimination (Proof by Cases): In order to prove that a claim Q follows from a disjunction P(1) v ... v P(n), prove that it follows from each of the disjuncts.

6.4: Disjunction Introduction: If you have established P, you may assert P v Q for any Q.

6.5: Negation Elimination: If you have established ¬¬P, then you may assert P.

6.6:* Negation Introduction (Proof by Contradiction): To prove that ¬P follows from certain premises, assume P and show that it leads to a contradiction.

CHAPTER EIGHT RULES

8.1: Conditional Elimination (Modus Ponens): If you have proven P -> Q and P, you can validly assert Q.

8.2:* Conditional Introduction (Conditional Proof): To prove a sentence of the form P -> Q, assume P and show Q.

8.3: Biconditional Elimination: If you have proven P and either P <-> Q or Q <-> P, then you can validly infer Q.

8.4:* Biconditional Introduction: To prove P <-> Q, assume P and prove Q, and then assume Q and show P.

CHAPTER TWELVE & THIRTEEN RULES

12.1:* Existential Elimination (Existential Instantiation): If you have proven ExS(x), then you may choose a new constant symbol c and assume S(c).

12.2: Existential Introduction (Existential Generalization): From S(c), infer ExS(x), so long as c denotes an object in the domain of discourse.

12.3: Universal Elimination (Universal Instantiation): From AxS(x), infer S(c), so long as c denotes an object in the domain of discourse.

12.4:* Universal Introduction (Universal Generalization): If you want to prove AxS(x), choose a new constant symbol c and prove S(c).

12.5: General Conditional Proof: If you want to prove Ax(P(x) -> Q(x)), then you may choose a new constant symbol c, assume P(c), and show Q(c).