Propositional Logic

The sentential logic of Principia Metaphysica is classical. Although we have presented the logic axiomatically, our axiom system has the same power as the 'natural deduction' systems of sentential logic that you find in any introductory text. These natural deduction systems present the logic by describing introduction and elimination rules for the connectives. These rules tell one how to draw inferences to and from sentences involving these connectives within a proof.

However, since we are using the axiomatic method rather than a natural-deduction system, we first present the logic axiomatically and then prove that the introduction and elimination rules used in 'natural deduction' systems are valid rules. The axiomatic development of our sentential logic is presented in the item Logic/Sentential Logic. For convenience, we reproduce the axioms and rules of sentential logic here:

Axioms of Sentential Logic

The basis of our system is classical sentential logic. So the axioms are the closures (modal closures, universal closures, actuality closures) of the following:

  1. φ → (ψ → φ)
  2. (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))
  3. (¬φ → ¬ψ) → ((¬φ → ψ) → φ)

Some Consequences:

In this section, we offer some basic examples of how to prove consequences of the axioms using the rules of inference described on the opening page of the tutorial. Basically, the method is to produce sequences of formulas that constitute derivations or proofs, or partial sequences to which one can apply metarules that guarantee that a proof sequence of the desired kind exists. With these methods, all of the tautologies of sentential logic can be derived as theorems.

A Derivation:

p ⊢ q → p

This asserts that from the single premise p we can derive the conditional if q then p. To see that this claim is true, consider the following sequence of three formulas:

p, p → (q → p), q → p

This sequence constitutes a derivation of if q then p from the premise p because: (a) it is a finite sequence of formulas ending in if q then p, (b) the first member of the sequence is a member of the set of premises, (c) the second member of the sequence is a logical axiom (this is an instance of the first axiom schema of sentential logic), and (d) the last member of the sequence follows from the first two by the rule Modus Ponens. So all of the conditions for claiming that there is a derivation of if q then p from p are met.

Logical Theorem Schema:

⊢ φ → φ

This asserts that every instance of the schema is a theorem of the system. Here is a proof:

  1. (φ → ((φ → φ) → φ)) → ((φ → (φ → φ)) → (φ → φ))
  2. φ → ((φ → φ) → φ)
  3. (φ → (φ → φ)) → (φ → φ)
  4. φ → (φ → φ)
  5. φ → φ

This constitutes a proof of the schema φ → φ from the empty set of premises because: (a) it is finite sequence of formulas ending with the schema; (b) line 1 is an instance of the second axiom schema of sentential logic (set φ to φ, ψ to (φ → φ), and χ to φ); (c) line 2 is an instance of the first axiom schema of sentential logic; (d) line 3 follows from lines 1 and 2 by Modus Ponens; (e) line 4 is another instance of the first axiom schema, and (f) line 5 follows from lines 3 and 4 by Modus Ponens. As a particular example, it follows that xF → xF is a theorem.

Metatheorems and Derived Rules

In what follows, we describe and sometimes prove metarules and derived rules of inference that can be derived from the basis of our logic. All of the natural deduction rules can be derived, though we only sketch a few of these.

Metatheorem (The Deduction Theorem)

If Γ, φ ⊢ ψ, then Γ ⊢ (φ → ψ)

This claim constitutes a metatheorem about the system of Principia Metaphysica. It is often used and cited “Conditional Proof”. We shall not prove this metatheorem here, but rather, offer an example. Assume as a premise that All Greeks are European, formalized as ∀x(Gx → Ex). Let this be the sole element of the set of premises designated by the Greek letter Γ in the statement of the metatheorem. Now consider the claim Clinton is Greek, formalized as Gc. Let this be the designation of the Greek letter φ). It is a fact that by quantificational logic we can derive Clinton is European (Ec) from the premises All Greeks are European and Clinton is Greek. To see this, employ an appropriate instance of the axiom ∀αφ → (τ↓ → φ[τ/α]) by setting α to x, φ to Gx → Ex, τ to c, and φ[τ/α]) to Gc → Ec, which yields the axiom:

∀x(Gx → Ex) → (c↓ → (Gc → Ec))

So from Γ (as assigned above) and this axiom, it follows by MP that:

c↓ → (Gc → Ec)

But it is also axiomatic that c↓, since all primitive constants are assigned a denotation. So from this axiom and the above it follows that Gc → Ec. But we let φ be Gc. So from our last result and φ, it follows by MP that Ec. So if ψ is the formula Ec, we have an instance of a derivation of ψ from Γ and φ, i.e., we have a witness to Γ, φ ⊢ ψ. Hence, the Deduction Theorem tells us that from Γ alone, we have a derivation of the conditional φ → ψ, i.e., from ∀x(Gx → Ex), there is a proof of Gc → Ec.

Now when all of the premises in Γ are axioms, then the Deduction Theorem simplifies to the assertion: If there is a derivation of ψ from φ, then there is a proof of φ → ψ, i.e., if φ ⊢ ψ, then ⊢ φ → ψ.

Metarule: Reductio Ad Absurdum (RAA)

If Γ, ¬φ ⊢ ¬ψ and Γ, ¬φ ⊢ ψ, then Γ ⊢ φ

To prove this is a good rule, we show that any derivation of φ from Γ involving RAA can be converted to a proof of φ from Γ without using RAA. So suppose we have a derivation of φ from Γ using RAA. Then, by assumption, the antecedent of the rule is true. So if we apply the Deduction Theorem to the first conjunct of the rule's hypothesis, we know:

Γ ⊢ ¬φ → ¬ψ

Call a sequence of formulas that must exist according to this claim Sequence 1. Now if we apply the Deduction Theorem to the second conjunct of the rule's antecedent, we know:

Γ ⊢ ¬φ → ψ

Again, call the sequence of formulas that must exist according to this claim Sequence 2. Now we produce a proof of phi from Gamma without using RAA as follows: combine Sequence 1 and Sequence 2; then append to this new sequence the third axiom of sentential logic:

(¬φ → ¬ψ) → ((¬phi; → ψ) → φ)

Now we append to the resulting sequence the result of applying Modus Ponens to the axiom just added and the last line of Sequence 1; finally we append to the resulting sequence the result of applying Modus Ponens to the last line and the last line of Sequence 2. The result constitutes a proof of phi from Gamma without using RAA.

Derived Rule: Modus Tollens

φ → ψ, ¬ψ ⊢ ¬φ

Instead of a proof, we offer an example: from the claims If the sun is shining, then John is happy and It is not the case that John is happy, it follows by Modus Tollens that It is not the case that the sun is shining. As a more specific example involving the language of the theory, it follows from the claims If it is possible that xF, then it is necessary that xF and It is not necessary that xF that It is not possible that xF.

Derived Rules: Double Negation

φ ⊣⊢ ¬¬φ

For example, from the claim John is happy it follows by Double Negation that It is not the case that it is not the case that John is happy, and vice versa. As a more specifc example involving the language of the theory, it follows from the claim that xF that It is not the case that it is not the case xF, and vice versa.

Derived Rule: & Introduction

φ, ψ ⊢ φ & ψ

For example, from the premises John is happy and Mary is sad we may draw the conjunctive conclusion John is happy & Mary is sad. Similarly, from aF and it is not the case that Fa, we may conclude aF & it is not the case that Fa.

Exercise:

Find an introductory logic text and search for other rules of inference. Construct examples of these rules. Find rules for & Elimination, Disjunction Introduction and Elimination, Biconditional Introduction and Elimination, Contraposition and Disjunctive Syllogism.

Some Further Theorems

We conclude with some examples that show the usefulness of the rules of Conditional Proof and RAA.

Theorem Schema:

⊢ (φ → ψ) → ((ψ → χ) → (φ → χ))

To prove this Theorem Schema, first consider the following sequence of formulas:

  1. φ → ψ
  2. ψ → χ
  3. φ
  4. ψ
  5. χ

Notice that this sequence of formulas demonstrates the following fact:

φ → ψ, ψ → χ, φ ⊢ χ

The sequence demonstrates this fact because: (a) it is finite in length, (b) lines 1, 2, and 3 are all premises, and (c) lines 4 and 5 follow from previous lines by Modus Ponens. So, given this fact, it follows by the Deduction Theorem that:

φ → ψ, ψ → χ ⊢ φ → χ

And given two further applications of the Deduction Theorem, we have proved:

⊢ (φ → ψ) → ((ψ → χ) → (φ → χ))

Exercise: Prove the Law of Excluded Middle and the Law of Noncontradiction using RAA.