Post History

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](https://en.wikipedia.org/wiki/Rule_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:

[![kripke-5.svg](https://math.codidact.com/uploads/1btvtft74kvcfwoh0847gose0sdo)](https://xamidi.github.io/pmGenerator/svg/kripke-5.svg)

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](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Completeness_(logic))).

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](https://en.wikipedia.org/wiki/S5_(modal_logic)) 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](https://xamidi.github.io/pmGenerator/data/s5proofs.txt) for occurrences of `5` in proof strings.

The collection is part of [pmGenerator](https://github.com/xamidi/pmGenerator), a tool able to parse these so-called [condensed detachment](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Hilbert_system) — tend to have long proofs that are hard to find, but their theoretical properties are very bare-bones.