In Principia Logico-Metaphysica, we take the all the closures of all the instances of the following as axioms:
We'll reason from these axioms with the primitive rule Modus Ponens, and the two metarules introduced on the opening page of this tutorial, namely, the Rule of Generalization and the Rule of Necessitation.
In the examples below, we sometimes appeal to the intuitive notion of a possible world, i.e., a complete way things might be. Our world is just one possible world of an infinite number of such worlds. Though Principia Logico-Metaphysica provides a precise definition of possible world and offers proofs of the main principles of possible world theory, let's suppose for now that we have an intuitive understanding of possible worlds. Then we may intuitively think of the claim □φ as true when φ is true in all possible worlds, and ◇φ as true when it φ is true in some possible world. We will exploit these intuitions in what follows to help us to get a picture of (i.e., intuitive model of) the axioms and theorems.
Instance of Axiom 1
Recall that the predicate E! denotes being concrete. If we suppose S denotes the property having a shape. Then the above asserts that:
If it is necessarily true that (if x isn't concrete, then x doesn't have a shape), then if x necessarily fails to be concrete, then x necessarily fails to have a shape.
The antecedent of this instance of Axiom 1 can be derived from the principle that necessarily, if x has a shape, then x is concrete, since if we contrapose the embedded conditional, it follows that necessarily, if x isn't concrete then x doesn't have a shape. If we extend object theory with this principle, then from our instance of Axiom 1, it follows that if x necessarily fails to be concrete, then x fails to have a shape. Now objects that necessarily fail to be concrete are, by definition, abstract objects. So our instance of Axiom 1 will help us to prove that abstract objects necessarily fail to have a shape.
Instance of Axiom 2
This simply asserts: if it is necessary that x encodes F, then x encodes F. Intuitively, any statement true at all possible worlds is true (at the actual world).
Instance of Axiom 3
Let the predicate P denote the property of being a politician. Let the constant c denote Clinton. Then this instance of Axiom 3 asserts: if Clinton might not have been a politician, then it is necessary that he might not have been a politician. Intuitively, this axiom just tells us that statements having the weakest modal status, namely, being possibly true, have that status necessarily.
The Rule of Necessitation (introduced on the opening page of the tutorial) basically asserts that anything derivable from necessary truths is a necessary truth, and that any theorem proved only on the basis of necessary axioms is itself necessary. With the exception of the modally fragile axiom governing the actuality operator, which asserts 𝒜φ → φ, all of the axioms of our system are necessary truths. So anything derivable from the necessary axioms alone is a necessary truth. Moreover, if we can derive any consequence that depends solely on modal axioms or added premises which are themselves necessary truths, then such a consequence is also a necessary truth. Such derivations are modally strict.
In is worth noting that in many developments of modal logic, the Rule of Necessitation is formulated as a primitive rule of inference. The axioms of such systems do not include the modal closures of the axioms 1 – 3 at the top of this page. In such formulations, it is assumed that all of the axioms are necessary truths. Since anything derivable solely from such necessary truths will itself be necessary, RN never takes one from truth to falsehood.
However, when formulating a modal logic in which one of the axioms is not a necessary truth, RN must be restricted. It works normally in any proof where the conclusion rests only on axioms that are necessary. But when the conclusion rests on an axiom that is not necessary, the application of RN is invalid.
For example, on one construal, the conditional claim 𝒜φ → φ (“if it is actually the case that φ, then φ”) is a logical truth but not a necessary truth. This conditional is logically true because it is part of the very meaning of the operator it is actually the case that (𝒜). The formula 𝒜φ is true whenever φ is true at the actual world w0. However, to see that 𝒜φ → φ is not a necessary truth, we need only find a possible world where this conditional is false. Suppose that φ is true at the actual world w0, but false at w1. Then evaluate the truth of the conditional 𝒜φ → φ at w1. The antecedent 𝒜φ is true at w1 because, by hypothesis, φ is true at w0. But the consequent, φ, is false at w1. Since the antecedent of 𝒜φ → φ is true at w1 but the consequent is false at w1, the entire conditional is false at w1. So the conditional is not a necessary truth since there is a world where it is false.
So we don’t want to apply the Rule of Necessitation to the axiom 𝒜φ → φ, or apply it to any theorem that is derived from that axiom. So we can have the Rule of Necessitation as a primitive rule that can be applied to any theorem.
So we've developed the modal logic of object theory so that it can accomodate reasoning with such contingent, modally fragile axioms and assumptions. The technique is simply to include, as axioms, all of the modal closures of all the axioms of the system other than the modally fragile axioms. Then the Rule of Necessitation can be derived in restricted form, so that it may not be applied to any theorem derived from a contingency. RN behaves classically in cases where the derivation involves only necessary truths.
Derivation Schema: Modal Modus Ponens
In other words, there is a derivation of □ψ from the premises □φ and □(φ → ψ). This derivation schema grounds a reasoning pattern often found in natural deduction systems of modal logic. The reasoning pattern can be justified intuitively as follows:
Consider an arbitrary world w. Since □φ is also a premise, it is true at all possible worlds and so is true at w. Since □(φ → ψ) is a premise, it, too, is true at all possible worlds, and so it is true at w. But now both φ → ψ and φ are both true at w, and so, by Modus Ponens, ψ is true at w. Since w was arbitrarily chosen, we've established that ψ is true at all possible worlds, i.e., that □ψ is true.
The present derivation schema underlies and grounds this kind of reasoning.
It is easy to prove Modal Modus Ponens, given Axiom 1 of modal logic. Consider the following sequence of formulas:
1. □φ Premise2. □(φ → ψ) Premise3. □(φ → ψ) → (□φ → □ψ) Instance of the K schema (i.e., Axiom 1)4. □φ → □ψ From 2 and 3 by Modus Ponens5. □ψ From 4 and 1 by Modus Ponens
This is a proof because: (a) lines 1 and 2 are members of the premise set, (b) line 3 is an instance of Axiom 1 of modal logic, (c) line 4 results from lines 1 and 3 by MP, and (d) line 5 results from lines 2 and 4 by MP.
Theorem Schema and Derivation Schema:
The first of these is a theorem schema that asserts: if necessarily, φ implies ψ, then if φ is possible, then so is ψ. The proof justification of this theorem schema appeals to an instance of the K axiom:
(A) □(¬ψ → ¬φ) → (□¬ψ → □¬φ)
But since contraposed formulas are necessarily equivalent, we may substitute them for one another whenever they occur as subformulas, so that the antecedent of (A) is equivalent to:
□(φ → ψ)
and the consequence of (A) is equivalent to:
¬□¬φ → ¬□¬ψ
But the definition, ◇φ ≡df ¬□¬φ, tells us that the definiendum and definiens formulas are necessarily equivalent, and so they too may be substituted for one another when they occur as subformulas. Hence, the formula displayed immediate above becomes:
◇φ → ◇ψ
So, assembling formulas that are equivalent to the antecedent and consequence of (A), we have an informal proof sketch of:
⊢ □(φ → ψ) → (◇φ → ◇ψ)
Now consider the second of the two bulleted formulas. This is a derivation schema that tells us that there is a of ◇ψ from the premises □(φ → ψ) and ◇φ. It follows from the theorem schema by facts about the derivability relation. But, intuitively, it is justified as follows: the premise □(φ → ψ) requires that φ → ψ be true at every possible world. The premise ◇φ requires that φ be true at some possible world. Suppose w1 is such a world. Then since φ → ψ is true at every world, it is true at w1. So by Modus Ponens, ψ is true at w1. So there is a possible world, namely w1, where ψ is true. Hence ◇ψ. So, we have intuitively derived ◇φ from our two premises.
These are all theorem schemas. In what follows, we develop a number of Lemmas and Derived Rules, to be followed by a proof of BF:
Proof of Lemma 1: φ → □◇φ
1. □¬φ → ¬φ instance of the T schema2. φ → ¬□¬φ contraposition, 13. φ → ◇φ definition of ◇, 24. ◇φ → □◇φ instance of 5 schema5. φ → □◇φ propositional logic, 3, 4
Proof of Lemma 2: ◇□φ → φ
1. ¬φ → □◇¬φ Instance of Lemma 12. ¬□◇¬φ → φ contraposition, 13. ◇□φ ≡ ¬□◇¬φ Modal theorem about negation and interdefinability of ◇ and □4. ◇□φ → φ Hypothetical syllogism, 3, 2
Proof of Derived Rule 1 (DR1): χ → θ ⊢ □χ → □θ
1. χ → θ Premise2. □(χ → θ) Rule RN, 13. □(χ → θ) → (□χ → □θ) Instance of K schema4. □χ → □θ Modus Ponens, 3, 4
Proof of Derived Rule 2 (DR2): ◇χ → θ ⊢ χ → □θ
Exercise: By DR1, Lemma 1, and propositional logic.
Using these theorems and rules, we can now follow Arthur Prior’s proof of BF:
⊢ ∀x□φ → □∀xφ
1. ∀x□φ → □φ Axiom of quantifier logic2. □(∀x□φ → □φ) RN, 13. □(∀x□φ → □φ) → (◇∀x□φ → ◇□φ) A theorem of S54. ◇∀x□φ → ◇□φ MP, 2, 35. ◇□φ → φ Lemma 26. ◇∀x□φ → φ propositionall logic, 4, 57. ∀x(◇∀x□φ → φ) GEN, 68. ∀x(◇∀x□φ → φ) → (◇∀x□φ → ∀xφ) Axiom of quantifier logic9. ◇∀x□φ → ∀xφ MP, 7,810. ∀x□φ → □∀xφ DR2, 9
Proof of BF◇
⊢ ◇∃xφ → ∃x◇φ
1. ∀x□¬φ → □∀x¬φ Instance of BF2. ¬□∀x¬φ → ¬∀x□¬φ contraposition, 13. ◇¬∀x¬φ → ¬∀x¬◇φ apply modal negation equivalents to antecedent, consequent of 2, via Rule of Substitution4. ◇∃xφ → ∃x◇φ apply definition of ∃ to antecedent, consequent of 3, via a Rule of Substitution
⊢ □∀xφ → ∀x□φ
1. ∀xφ → φ Axiom of quantifier logic2. □(∀xφ → φ) RN, 13. □(∀xφ → φ) → (□∀xφ → □φ) Instance of the K Schema (Axiom 1 at the top of the page)4. □∀xφ → □φ MP, 2, 35. ∀x(□∀xφ → □φ) GEN, 46. ∀x(□∀xφ → □φ) → (□∀xφ → ∀x□φ) Axiom of quantifier logic7. □∀xφ → ∀x□φ MP, 5, 6