system/model invoking N), then □p is likewise a theorem (i.e. ). K, Distribution Axiom: The weakest normal modal logic, named "K" in honor of Saul Kripke, is simply the propositional calculus augmented by □, the rule N, and the axiom K. K is weak in that it fails to determine whether a proposition can be necessary but only contingently necessary. That is, it is not a theorem of K that if □p is true then □□p is true, i.e., that necessary truths are "necessarily necessary". If such perplexities are deemed forced and artificial, this defect of K is not a great one. In any case, different answers to such questions yield different systems of modal logic. Adding axioms to K gives rise to other well-known modal systems. One cannot prove in K that if "p is necessary" then p is true. The axiom T remedies this defect: T, Reflexivity Axiom: (If p is necessary, then p is the case.) T holds in most but not all modal logics. Zeman (1973) describes a few exceptions, such as S10. Other well-known elementary axioms are: 4: B: D: 5: These yield the systems (axioms in bold, systems in italics): K := K + N T := K + T S4 := T + 4 S5 := T + 5 D := K + D. K through S5 form a nested hierarchy of systems, making up the core of normal modal logic. But specific rules or sets of rules may be appropriate for specific systems. For example, in deontic logic, (If it ought to be that p, then it is permitted that p) seems appropriate, but we should probably not include that . In fact, to do so is to commit the naturalistic fallacy (i.e. to state that what is natural is also good, by saying that if p is the case, p ought to be permitted). The commonly employed system S5 simply makes all modal truths necessary. For example, if p is possible, then it is "necessary" that p is possible. Also, if p is necessary, then it is necessary that p is necessary. Other systems of modal logic have been formulated, in part because S5 does not describe every kind of modality of interest. Structural proof theory Sequent calculi and systems of natural deduction have been developed for several modal logics, but it has proven hard to combine generality with other features