Rules of Inference in First-Order Logic

A comprehensive guide to the fundamental inference rules that form the basis of logical reasoning

Introduction to Inference Rules

First-order logic extends propositional logic with quantifiers and predicates. Inference rules are essential for constructing valid arguments and proofs in logical systems. These rules allow us to derive new statements from existing ones while preserving truth.

Core Rules from Propositional Logic

Modus Ponens

MP

If P implies Q, and P is true, then Q is true.

P → Q
P
∴ Q

Modus Tollens

MT

If P implies Q, and Q is false, then P is false.

P → Q
¬Q
∴ ¬P

Hypothetical Syllogism

HS

If P implies Q and Q implies R, then P implies R.

P → Q
Q → R
∴ P → R

Disjunctive Syllogism

DS

If P or Q is true, and P is false, then Q is true.

P ∨ Q
¬P
∴ Q

Conjunction

Conj

If P is true and Q is true, then P and Q is true.

P
Q
∴ P ∧ Q

Simplification

Simp

If P and Q is true, then P is true and Q is true.

P ∧ Q
∴ P

P ∧ Q
∴ Q

Quantifier Rules (Specific to First-Order Logic)

Universal Instantiation

UI

From a universally quantified statement, we can infer any instance.

∀x P(x)
∴ P(c)    (for any specific constant c)

Existential Generalization

EG

From a specific instance, we can infer an existentially quantified statement.

P(c)
∴ ∃x P(x)

Universal Generalization

UG

If we can prove P(c) for an arbitrary constant c, then we can infer ∀x P(x).

P(c)    (where c is arbitrary)
∴ ∀x P(x)

Existential Instantiation

EI

From an existentially quantified statement, we can introduce a new constant.

∃x P(x)
∴ P(c)    (where c is a new constant)

Example Proof

Let's prove: ∀x (P(x) → Q(x)), ∀x P(x) ∴ ∀x Q(x)

1.

∀x (P(x) → Q(x))

2.

∀x P(x)

3.

P(c) → Q(c)

4.

P(c)

5.

Q(c)

6.

∀x Q(x)

Important Notes

- Universal Generalization (UG) requires that the constant c is truly arbitrary (not appearing in any premises)

- Existential Instantiation (EI) requires introducing a new constant that hasn't been used before

- These rules form a complete system for first-order logic proofs

- Natural deduction systems organize these rules into introduction and elimination rules for each connective

Conclusion

These inference rules allow us to construct formal proofs in first-order logic, moving from premises to conclusions through valid logical steps. Mastering these rules is essential for understanding logical reasoning, mathematical proofs, and formal verification in computer science.

First-Order Logic Inference Rules | © 2023

Created as an educational resource for students of logic and computer science