What is the significance of the K-axiom in modal logic S5?
In normal modal logic S5, the K axiom says $\square (p \rightarrow q) \rightarrow (\square p \rightarrow \square q)$.
First of all, is this an abuse of notation? https://en.m.wikipedia.org/wiki/S5_(modal_logic)
The middle implication arrow is meta-logical, isn’t it? It’s saying, “if statement 1 is true, then statement 2 is true”. This is not the same as the intra-logical implication arrow. Shouldn’t it be $\square (p \rightarrow q) \implies (\square p \rightarrow \square q)$?
Secondly, why is this axiom so critical or definitive to S5? It has been conceptualized in a few ways. One, that necessity distributes over implication. But why should it? Does this imply that possibility also distributes over implication? Or that modal operators distribute over other connectives, like and and or?
It has also been interpreted as saying “necessary consequences of necessary truths are also necessary truths”, which I find more intuitive. Still, I find myself wondering if that claim could be derived from something else, as in that expression it sounds self-evident - even necessary.
1 answer
Axioms exist to define proof systems, i.e. syntactical ways to derive theorems — in contrast to semantics, which concerns meaning. This is accomplished by combining axioms with (meta-logical) rules of inference in so-called proofs.
The middle implication arrow is meta-logical, isn’t it?
No, it is not, since it is not a rule. A formula is nothing else than the syntactic structure of an assertion. The K axiom has the following syntax tree:
It to be an axiom means that all formulas of that form (i.e. $p$ and $q$ can be substituted with arbitrary formulas) are considered proven by definition. Then, with meta-logical rules of the system (such as modus ponens), those formulas can be combined to form new formulas, called theorems.
Secondly, why is this axiom so critical or definitive to S5?
There certainly are alternatives to this axiom, but it is hard to find a small set of such concise and intuitive formulas from which an entire system can be proven (which we desire for completeness).
In this case, axiom K combined with modus ponens (MP), allows us to derive formulas of the form $□p→□q$ from formulas of the form $□(p→q)$, since MP means ⊢ψ,⊢ψ→φ ⇒ ⊢φ, i.e. "if (the proposition) ψ is provable and (the proposition) ψ→φ is provable, then thereby (the proposition) φ is provable".
The fact that we are required to be able to do so is entailed by the semantics of alethic modal logic. This could be noted by $[\![□(p→q),w]\!]=1\Rightarrow[\![□p→□q,w]\!]=1$ for all formulas $p,q$ and all worlds $w$, where $[\![\cdot]\!]:\mathcal{L}\times\mathcal{W}\rightarrow\mathbb{B}$ is the semantics. This is indeed valid in every Kripke model.
So, the K axiom is not essential in that one has to use it for the definition of a proof system. Alternative sets of axioms simply must be able to do what it does. It is, however, essential in systems where it is usually used, in the way that one cannot derive certain theorems without using it, since the remaining axioms are incomplete.
An example: S5 with the K axiom
A typical way to define a proof system for the modal logic S5 is by using six axioms
p→(q→p), (p→(q→r))→((p→q)→(p→r)), (¬p→¬q)→(q→p), □p→p, □(p→q)→(□p→□q), ◇p→□◇p
where ◇ is actually short-hand for ¬□¬. These formulas, with only the rules of MP and necessitation (NE; ⊢ψ ⇒ ⊢□ψ), can prove all S5-valid formulas in terms of $\{→,¬,□\}$.
Note that the 5th axiom is axiom K, and when removing it, the remaining formulas are unable to prove axiom K, despite it being valid according to all Kripke models.
In terms of usage, you may look at this little proof collection for occurrences of 5 in proof strings.
The collection is part of pmGenerator, a tool able to parse these so-called condensed detachment proofs. To give you a sense of how complex these proofs really are, here is the comparatively short 25-step proof D3DD2D14DD2DD2D13DD2D1311 for p→◇p, an alternative for □p→p as an axiom, written in terms of formulas:
1. ¬¬□¬0→(1→¬¬□¬0) (1)
2. ¬¬□¬0→(¬¬(1→¬¬□¬0)→¬¬□¬0) (1)
3. (¬¬(1→¬¬□¬0)→¬¬□¬0)→(¬□¬0→¬(1→¬¬□¬0)) (3)
4. ((¬¬(1→¬¬□¬0)→¬¬□¬0)→(¬□¬0→¬(1→¬¬□¬0)))→(¬¬□¬0→((¬¬(1→¬¬□¬0)→¬¬□¬0)→(¬□¬0→¬(1→¬¬□¬0)))) (1)
5. ¬¬□¬0→((¬¬(1→¬¬□¬0)→¬¬□¬0)→(¬□¬0→¬(1→¬¬□¬0))) (D):3,4
6. (¬¬□¬0→((¬¬(1→¬¬□¬0)→¬¬□¬0)→(¬□¬0→¬(1→¬¬□¬0))))→((¬¬□¬0→(¬¬(1→¬¬□¬0)→¬¬□¬0))→(¬¬□¬0→(¬□¬0→¬(1→¬¬□¬0)))) (2)
7. (¬¬□¬0→(¬¬(1→¬¬□¬0)→¬¬□¬0))→(¬¬□¬0→(¬□¬0→¬(1→¬¬□¬0))) (D):5,6
8. ¬¬□¬0→(¬□¬0→¬(1→¬¬□¬0)) (D):2,7
9. (¬□¬0→¬(1→¬¬□¬0))→((1→¬¬□¬0)→□¬0) (3)
10. ((¬□¬0→¬(1→¬¬□¬0))→((1→¬¬□¬0)→□¬0))→(¬¬□¬0→((¬□¬0→¬(1→¬¬□¬0))→((1→¬¬□¬0)→□¬0))) (1)
11. ¬¬□¬0→((¬□¬0→¬(1→¬¬□¬0))→((1→¬¬□¬0)→□¬0)) (D):9,10
12. (¬¬□¬0→((¬□¬0→¬(1→¬¬□¬0))→((1→¬¬□¬0)→□¬0)))→((¬¬□¬0→(¬□¬0→¬(1→¬¬□¬0)))→(¬¬□¬0→((1→¬¬□¬0)→□¬0))) (2)
13. (¬¬□¬0→(¬□¬0→¬(1→¬¬□¬0)))→(¬¬□¬0→((1→¬¬□¬0)→□¬0)) (D):11,12
14. ¬¬□¬0→((1→¬¬□¬0)→□¬0) (D):8,13
15. (¬¬□¬0→((1→¬¬□¬0)→□¬0))→((¬¬□¬0→(1→¬¬□¬0))→(¬¬□¬0→□¬0)) (2)
16. (¬¬□¬0→(1→¬¬□¬0))→(¬¬□¬0→□¬0) (D):14,15
17. ¬¬□¬0→□¬0 (D):1,16
18. □¬0→¬0 (4)
19. (□¬0→¬0)→(¬¬□¬0→(□¬0→¬0)) (1)
20. ¬¬□¬0→(□¬0→¬0) (D):18,19
21. (¬¬□¬0→(□¬0→¬0))→((¬¬□¬0→□¬0)→(¬¬□¬0→¬0)) (2)
22. (¬¬□¬0→□¬0)→(¬¬□¬0→¬0) (D):20,21
23. ¬¬□¬0→¬0 (D):17,22
24. (¬¬□¬0→¬0)→(0→¬□¬0) (3)
25. 0→¬□¬0 (D):23,24
Note that in this notation, variables in formulas are simply referred to by natural numbers. The above proof is actually minimal for its system and can be obtained by using the following command:
pmGenerator -c -n -N -1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp --parse D3DD2D14DD2DD2D13DD2D1311 -j -1 -u
The given exemplary proofs that make use of axiom K are much longer, but they require its usage several times. All (sub-)proofs in that collection were optimized in terms of length, such that those with up to 31 steps are known to be minimal.
The here used proof systems — so called Hilbert systems — tend to have long proofs that are hard to find, but their theoretical properties are very bare-bones.
0 comment threads
0 comment threads