What kinds of proofs can be given for axioms, e.g. the modal axiom S5?

Question

From John Bigelow and Robert Pargetter's book, titled, 'Science and Necessity', they assert the following:

. . . . The resulting system, S5, contains all the theorems of S4 and all the theorems of B and nothing more. Given axiom T plus axiom S5, we can prove S4 and B; but conversely, too, given T plus both S4 and B, we can prove S5. Yet T plus S4 without B does not enable us to prove S5; and T plus B without S4 does not enable us to prove S5. (Axiom S5 is intuitively `If something is possibly true, then it must be true that it is possibly true'.)

On the basis of this statement, it would appear as if there could be a 'proof' of the S5 Axiom. Prior to this statement they sketched 'a fairly orthodox axiomatic system' which introduced items such as: definitions, rules of inference, expositions of Axiom K, Axiom D, Axiom T, etc. and shared a diagram visualizing the system they had just exposited.

Here's the question: there was a classmate of mine who presented a 'proof' of the S5 Axiom, what could be said of the 'legitimacy', if you will, regarding this supposed 'proof' of the S5 Axiom?

[W,R]

t ∈ W

t ⊩ A

ΔRt; Δ is an arbitrary variable accessible to t

Δ ⊩ □A; ∀Δ∀t(ΔRt) Serial Property

ΘRΔ; Θ is an arbitrary variable accessible to Δ

Θ ⊩ ⋄A; ∀Δ∃Θ(ΘRΔ) Serial Property

If t ⊩ A then t ⊩ ⋄A; ∀t(tRt) Reflexive Property

⋄A → □⋄A; ∀t∀Δ∃Θ(ΘRΔ ∧ ΔRt → ΘRt) Transitive Property

Q.E.D

Perhaps a better question could be: What proofs, if any, can there be given for the S5 Axiom?

Link to Original Question:

https://math.stackexchange.com/questions/3399637/what-could-be-said-of-the-legitimacy-if-you-will-regarding-this-supposed-pr

Answer 1

There are two general ways of "proving axioms": deductive and semantic. Deductively, one can take a different system with its own axioms, and ask whether the given "axiom" is deducible in it as a theorem. For example, we can add Zorn's lemma or Zermelo's well-ordering principle to the set theory ZF, and deduce the axiom of choice in the theory so extended. The same is possible for 5 in S4+T+B, as the OP quoted passage states. Some alternative axiomatizations of S4 (and hence S5) are discussed in SEP, Modern Origins of Modal Logic.

Semantically, we can prove that an axiom holds in the "intended model" of the theory (this presupposes some background theory of the model, usually a fragment of set theory). For example, Euclid's axioms can be proved if we take the Cartesian plane as the intended model of geometry. According to Kripke, the intended models for classical modal logic are given by a set of possible worlds (W), an accessibility relation on them (R), and a designated "actual world" (w*). □A is then interpreted as "A is true in every world from W accessible from the actual world w*" and ⋄A as "A is true in at least one world from W accessible from the actual world w*".

It is well-known that 5 holds in the models where the accessibility relation is an equivalence, i.e. where it is reflexive, symmetric and transitive, see Kripke semantics. This is what the proof quoted in the OP demonstrates formally (and it does use symmetry implicitly). In fact, T, B, and 4 correspond to the reflexivity, symmetry, and transitivity of the accessibility relation, respectively, so S5 holds in a model if and only if the accessibility relation is an equivalence, see Equivalence Relations and S5.