Being in a position to know

Abstract

The concept of being in a position to know is an increasingly popular member of the epistemologist’s toolkit. Some have used it as a basis for an account of propositional justification. Others, following Timothy Williamson, have used it as a vehicle for articulating interesting luminosity and anti-luminosity theses. It is tempting to think that while knowledge itself does not obey any closure principles, being in a position to know does. For example, if one knows both p and ‘If p then q’, but one dies or gets distracted before being able to perform a modus ponens on these items of knowledge and for that reason one does not know q, one is still plausibly in a position to know q. It is also tempting to suppose that, while one does not know all logical truths, one is nevertheless in a position to know every logical truth. Putting these temptations together, we get the view that being in a position to know has a normal modal logic. A recent literature has begun to investigate whether it is a good idea to give in to these twin temptations—in particular the first one. That literature assumes very naturally that one is in a position to know everything one knows and that one is not in a position to know things that one cannot know. It has succeeded in showing that, given the modest closure condition that knowledge is closed under conjunction elimination (or ‘distributes over conjunction’), being a position to know cannot satisfy the so-called K axiom (closure of being in a position to know under modus ponens) of normal modal logics. In this paper, we explore the question of the normality of the logic of being in a position to know in a more far-reaching and systematic way. Assuming that being in a position to know entails the possibility of knowing and that knowing entails being in a position to know, we can demonstrate radical failures of normality without assuming any closure principles at all for knowledge. (However, as we will indicate, we get further problems if we assume that knowledge is closed under conjunction introduction.) Moreover, the failure of normality cannot be laid at the door of the K axiom for knowledge, since the standard principle NEC of necessitation also fails for being in a position to know. After laying out and explaining our results, we briefly survey the coherent options that remain.

1 Introduction

The concept of being in a position to know is an increasingly popular member of the epistemologist’s toolkit. Some have used it as a basis for an account of propositional justification.¹ Others, following Timothy Williamson,² have used it as a vehicle for articulating interesting luminosity and anti-luminosity theses. It is tempting to think that, while knowledge itself does not obey any closure principles, being in a position to know does. It is easy enough to see why closure principles for knowledge might be denied: death or distraction may prevent one from knowing the logical consequences of what one knows. Nevertheless, if one knows—and therefore is in a position to know—both p and p → q, but one dies or gets distracted before being able to perform a modus ponens on these items of knowledge and for that reason one never gets to know q, one was still plausibly in a position to know q.³, ⁴ It is also tempting to suppose that, while one does not know all logical truths, one is nevertheless in a position to know every logical truth.⁵ Putting these temptations together, we get the view that being in a position to know has a normal modal logic. As evidence of these temptations, we note that the use of normal epistemic logics is sometimes justified by glossing their epistemic operators using ‘in a position to know that’ and synonyms or near synonyms such as ‘can know that’ and ‘able to know that’.⁶ A recent literature has begun to investigate whether it is a good idea to give in to these temptations.⁷ That literature assumes very naturally that one is in a position to know everything one knows and that one is not in a position to know things that one cannot know. It has succeeded in showing that, given the modest closure condition that knowledge is closed under conjunction elimination (or ‘distributes over conjunction’), being a position to know cannot satisfy the so-called K axiom (closure of being in a position to know under modus ponens) of normal modal logics. In this paper, we explore the question of the normality of the logic of being in a position to know in a more far-reaching and systematic way. Assuming that being in a position to know entails the possibility of knowing and that knowing entails being in a position to know, we can demonstrate radical failures of normality for being in a position to know without assuming any closure principles for knowledge. This means that there is no easy way to rescue a normal modal logic for being in a position to know by denying that knowledge obeys any closure principles. (However, as we will indicate, we get further problems if we assume that knowledge is closed under conjunction elimination.) Moreover, the failure of normality cannot be laid at the door of the K axiom for knowledge, since the standard principle NEC of necessitation (or modal generalization) also fails for being in a position to know. After laying out and explaining our results, we briefly survey the coherent options that remain and give some reasons for preferring our favorite option, which is that ‘one is in a position to know’ is approximately synonymous with ‘one can know’, and thus it’s no surprise that it doesn’t behave like a necessity operator.

2 The logic

Our investigation of the logic of being in a position to know will be conducted using a language of propositionally quantified modal logic. The language has an infinite stock of atomic sentences, an infinite stock of propositional variables p, q, r, …, the standard truth-functional connectives, a universal quantifier ∀p for each propositional variable p, the propositional operators K^P (‘one is in a position to know that’), K (‘one knows that’), □ (‘necessarily’), @ (‘actually’), and the usual formation rules and metalinguistic abbreviations (thus ◇φ is ¬□¬φ and ∃pφ is ¬∀p¬φ). We will assume the logic characterized by the following rules and axioms, where the final two are standard axioms for the logic of actuality.⁸

(Taut):

All tautologies

(MP):

Modus ponens

(UG):

If ⊢ φ → ψ, then ⊢ φ → ∀pψ, where p is not free in φ

(UI):

∀pφ → φ[^ψ/_p], where ψ is free for p in φ

(T_K):

Kφ → φ

(K^P/◇):

K^Pφ → ◇Kφ

(K/K^P):

Kφ → K^Pφ

(T_□):

□φ → φ

(K_□):

□(φ → ψ) → (□φ → □ψ)

(NEC_□):

If φ is provable using only the axioms and rules already specified, then ⊢ □φ.⁹

(T_@):

@φ → φ

(RIG_@):

φ → □@φ

We will call this logic ‘L’, and will also write ‘⊢ φ’ for ‘φ ∈ L’.¹⁰

Here are the further candidate axioms and rules that will be discussed below.

(KKP)	KP(φ → ψ) → (KPφ → KPψ)
(NECKP)	If ⊢ φ, then ⊢ KPφ
(DISTK)	K(φ ∧ ψ) → (Kφ ∧ Kψ)

We will call the logic that results from adding any axioms or rules X₁, …, X_n to L ‘L + X₁ + ⋯ + X_n’, and we will write ‘X₁, …, X_n ⊢ φ’ when L + X₁ + ⋯ + X_n includes φ. We will say that the logic of a propositional operator P is normal in L + X₁ + ⋯ + X_n when L + X₁ + ⋯ + X_n includes.

(KP)	P(φ → ψ) → (Pφ → Pψ)

and is closed under the rule

(NECP)

If ⊢ φ, then ⊢ Pφ

Thus, for example, the logic of K^P in L + (K_K^P) + (NEC_K^P) is normal, and L + (K_K^P) + (NEC_K^P) ⊢ K^P(Kφ → φ), since ⊢ Kφ → φ.

3 Our main results

In this section we will present our main results informally. The formal proofs are included in the "Appendix".

The sentence

α:	∀p(p ↔ @p)

will play a starring role in our discussion. α has two interesting features. First, α is a logical truth. Second, the truth α expresses is extremely modally fragile: if things had been different in any way, it would have been false. After all, α says that everything is as it actually is, and if things had been different in any way, things would not have been as they actually are. Owing to this fragility, one only gets one shot, so to speak, at knowing α.¹¹,¹² If one doesn’t know α, then it is impossible for one to know α, since if one doesn’t know α, then, if one had known α, things would have been different than they actually are and α would have been false. Thus, if one doesn’t know α, then one could not have known α. Ditto for the conjunction of α with anything else: if one doesn’t know α ∧ φ, then one cannot know α ∧ φ. Formally:

(i)	⊢ α
(ii)	⊢ ¬Kα → ¬◇Kα
(iii)	⊢ ¬K(α ∧ φ) → ¬◇K(α ∧ φ)

Let us say that one conjunctively knows φ iff one knows the conjunction of φ and some proposition (∃pK(p ∧ φ), abbreviated as K^∧φ¹³). Our first result is:

(1)	(KKP) + (NECKP) ⊢ KPφ ↔ K∧φ

That is: If the logic of being in a position to know is normal, then one is in a position to know something if and only if one conjunctively knows it.

Informal argument: Suppose that the logic of being in a position to know is normal, so that one is in a position to know all logical truths (that is, suppose (NEC_K^P)), and being in a position to know the premises of a modus ponens entails being in a position to know its conclusion (that is, suppose (K_K^P)). Let φ be anything one is in a position to know. Since α is a logical truth, so is φ → (α ∧ φ). By (NEC_K^P), then, it follows that one is in a position to know φ → (α ∧ φ), and by (K_K^P), that one is in a position to know α ∧ φ. Since one is in a position to know something only if it is possible for one to know it (i.e., by (K^P/◇)), it is possible for one to know α ∧ φ. But, as we just saw in the previous paragraph (by (iii)), it is possible for one to know α ∧ φ only if one actually knows α ∧ φ, and so only if one actually knows the conjunction of φ with something. It follows that if one is in a position to know φ, then one conjunctively knows φ. What we have just seen is that, if the logic of being in a position to know is normal, then if one is in a position to know something, one conjunctively knows it. We can also use normality to establish that one is in a position to know anything one conjunctively knows. If one knows α ∧ φ, one is in a position to know α ∧ φ. Since (α ∧ φ) → φ is a logical truth, one is in a position to know it (by the (NEC_K^P) part of normality). Then one is in a position to know φ (by the (K_K^P) part of normality). Assuming normality for being in a position to know we have now established both directions of the biconditional: one is in a position to know something if and only if one conjunctively knows it. This is result (1).

An immediate consequence of (1) is (2):

(2)	The logic of K∧ in L + (KKP) + (NECKP) is normal

That is: if the logic of being in a position to know is normal, then the logic of conjunctive knowledge is normal.

What happens if the logic of being in a position to know is normal and knowledge distributes over conjunction, in the sense that one who knows a conjunction knows each conjunct? The result is arguably even more disturbing than (1). By (1) it already follows that one is in a position to know something if and only if one conjunctively knows it. If knowledge furthermore distributes over conjunction, then one knows everything one conjunctively knows, and it follows that one is in a position to know something if and only if one knows it. This is our third main result:

(3)	(KKP) + (NECKP) + (DISTK) ⊢ KPφ ↔ Kφ

Our fourth main result states an obvious corollary:

(4)	The logic of K in L + (KKP) + (NECKP) + (DISTK) is normal.

That is: if the logic of being in a position to know is normal and knowledge distributes over conjunction, then the logic of knowledge is normal.

Let us next see what we can show about the individual components of a normal modal logic for being in a position to know, (NEC_K^P) and (K_K^P), beginning with the former.

Suppose, as (NEC_K^P) states, that one is in a position to know every logical truth. Let λ be an arbitrary logical truth. It follows that α ∧ λ is a logical truth, and so that one is in a position to know α ∧ λ, and so that it is possible for one to know α ∧ λ. But, once again, it is only possible for one to know α ∧ λ if one actually knows α ∧ λ, and so actually conjunctively knows λ. It follows that, if one is in a position to know every logical truth, then one conjunctively knows every logical truth. This is our fifth main result:

(5)	L + (NECKP) is closed under (NECK∧)

Our sixth main result states the obvious corollary:

(6)	L + (NECKP) + (DISTK) is closed under (NECK)

That is: if one is in a position to know every logical truth and knowledge distributes over conjunction, then one knows every logical truth.

Let us finally turn to the hypothesis that being in a position to know is closed under modus ponens (that is, (K_K^P)). That is, if one is in a position to know the premises of a modus ponens, then one is in a position to know its conclusion. Our seventh main result is:

(7)	(KKP) ⊢ KP(φ → ψ) → (KPφ → ◇Kψ)

This amounts to the observation that this entails that, if one is in a position to know the premises of a modus ponens, then—because being in a position to know entails the possibility of knowing—it is possible for one to know its conclusion.

The example of α serves as a useful reminder of how problematic (7) is. Replacing ψ with α ∧ φ in (7), we get:

(!??)

KP(φ → (α ∧ φ)) → (KPφ → ◇K(α ∧ φ))

There are two main ways to generate counterexamples to (!??). First, insofar as we are willing to countenance any unknown logical truths at all, we should accept that there are cases in which one is in a position to know φ → (α ∧ φ) as well as φ but one does not know either φ → (α ∧ φ) or α ∧ φ. The details can be filled in in a variety of plausible ways. Perhaps φ is some humdrum truth (such as ‘We had lunch at Scott’s Seafood Restaurant in Mayfair on December 7th, 2019’) that one knows, and therefore is in a position to know, but, although one is in a position to know φ → (α ∧ φ), one has never considered the issue, and for that reason one knows neither φ → (α ∧ φ) nor α ∧ φ. Second, and perhaps even more decisively, consider someone who knows, and so is in a position to know, the logical truth φ → (α ∧ φ) but is merely in a position to know φ, knowing neither φ nor α ∧ φ. Both kinds of case are counterexamples to (!??): by (!??), if one is in a position to know both φ and φ → (α ∧ φ), it is possible for one to know α ∧ φ, which in turn entails that one does know α ∧ φ.¹⁴

4 Alternatives

We have seen that the principle that knowledge entails being in a position to know and that being in a position to know entails possibly knowing, which are axioms of our logic:

(K/KP)	Kφ → KPφ
(KP/◇)	KPφ → ◇Kφ

produce disastrous results when combined with either component of a normal logic for being in a position to know along with a minimal logic of necessity and actuality. We see two main lines of retreat, one of which we find clearly preferable to the other.

But first we will briefly address three general methodological concerns that a number of people have expressed to us in conversation.

The first concern is that our results are uninteresting because, after all, not even the necessity operator can be true of all logical truths (since the actuality operator generates some contingent ones). There is of course an symmetry here: neither ‘being in a position to know’ nor ‘it is necessary that’ will be applicable to all logical truths. But there is also an important asymmetry: In the language with @, while one won’t be able to apply ‘it is necessary that’ to all logical truths (though of course one can still apply that operator to all truth-functional tautologies in the expanded language), there will be no counterexamples to closure for ‘It is necessary that’. By contrast, in the expanded language, ‘one is in a position to know that’ is not only inapplicable to certain logical truths but also fails to obey K.

This is all relevant to a second concern someone might raise, namely that our conception of logical truth is too expansive. One might hope to escape the conclusions of this paper by saying ‘I prefer a narrow conception of logical truth. I agree with all your principles concerning actuality, but I deny that those principles have the status of logical truths.’ It would take us too far afield to properly engage with modes of conceptualizing logical truth that might motivate this restrictive vision.¹⁵ But in any case they do not provide an escape route. Let us be concessionary and adopt the interlocutor’s position. There won’t be any clear counterexamples to a rule of necessitation for ‘being in a position to know’ since the operative conception of logical truth is sufficiently narrow as to avoid the counterexamples of the paper. Still, the counterexamples to closure will be unimpugned, since they relied on the truth, not the logical truth, of the principles concerning actuality.

The third concern is that we do not offer a ‘semantics’, specifically a ‘possible-worlds semantics’, for our logic. Some contemporary philosophers are so enamored of the model-theoretic apparatus introduced by Kripke for investigating modal logics¹⁶ that they will only accept our proofs—and in particular our proof of α¹⁷—after we have given them a possible-worlds model theory on which they are valid. The demand is misguided. Beyond establishing consistency (which is not in doubt in this case) model theory—whether done in the possible-worlds style or any other—cannot be used for justifying axioms or rules of inference. It’s rather the other way around: the right model theory is whatever the logic being studied is sound and complete on.¹⁸

The first line of retreat involves rejecting axiom (K^P/◇), according to which being a position to know entails the possibility of knowing, and accepting that being in a position know has a normal modal logic.¹⁹ Here is one natural way to develop this thought: The logic of being in a position to know is normal, and one is in a position to know a proposition if and only if one knows it under an idealization to perfect rationality. It need not be metaphysically possible for that idealization to hold, and, under a metaphysically impossible idealization, one may know some propositions without knowing all propositions.²⁰ This way of thinking may have some precedent in natural and social science. An idealization to frictionless surfaces may have an explanatory point even if frictionless surfaces are metaphysically impossible. And perhaps an idealization to market economies that are free of certain ‘noise’ has a point even if such economies are metaphysically impossible. Similarly, for example, one who does not know a logical truth containing α may know α under an idealization to perfect rationality even when it is metaphysically impossible for one to know α. Drop the assumption that being in a position to know entails the possibility of knowing, and weaken our logic by dropping the corresponding axiom (K^P/◇), and you will no longer face the logical problems we have presented for far.

The reader should not underestimate the difficulties here, however. The problem with this proposal is that it doesn’t allow one to know that one doesn’t know a particular logical truth. As long as the logic of being in a position to know is normal—indeed, as long as (NEC_K^P) holds, with or without (K_K^P) or (K^P/◇)—we have the following result.

(12)	If ⊢ φ, then ⊢ K¬Kφ → (KPφ ∧ KP¬Kφ)21

By (12), whenever φ is a logical truth one knows oneself to not know, one is in a position to know φ and one is in a position to know that one doesn’t know φ. This is inconsistent with the conception of being in a position to know we are entertaining, since, according to that conception, the truth of.

K^Pφ ∧ K^P¬Kφ

amounts to the truth of the inconsistent

Kφ ∧ K¬Kφ

under an idealization to perfect rationality. That idealization may be metaphysically impossible, but it is not (or so its advocates should hope) inconsistent.

Here is a second observation. As long as the logic of being in a position to know is normal, we can prove, even without (K^P/◇):

(13)	If ⊢ φ, then ⊢ K¬Kφ → KP(φ ∧ ¬Kφ)

By (13), being in a position to know that one does not know a logical truth φ implies being in a position to know the conjunction: φ and one does not know φ.

The idealization picture suggests a further principle:

(NECKPK)

If ⊢ φ, then ⊢ KPKφ

The idea is that one not only knows but knows that one knows each logical truth under an idealization to perfect rationality. But if we have (NEC_K^P_K), we certainly cannot have a normal logic for being in a position to know. If we had both, we could prove, again without (K^P/◇):

(14)	If ⊢ φ, then ⊢ K¬Kφ → KP⊥

That is, we would get the result that one is in a position to know that one does not know a logical truth only if one is in a position to know a contradiction.

We thus do not think that the idealization picture provides a happy path to normality. Of course there may yet be other grounds for denying K^Pφ → ◇Kφ, and perhaps those other paths would provide a better basis for normality for K^P. We leave it as a challenge to others to find a well motivated package of this sort.

The second line of retreat, which we endorse, involves giving up both components of normality for being in a position to know: (NEC_K^P) and (K_K^P). This approach is easy to motivate once one notices that ‘in a position to know’ is a composition of two operators, ‘in a position to’ and ‘know’.

We begin with the former. We propose that ‘x in a position to F’ is approximately synonymous with ‘x can F’ or ‘x is able to F’. The standard of synonymy we have in mind here is roughly sameness of Kaplanian character. It’s not that these expressions have the same semantic content in a context-independent way, but rather that they are capable of expressing approximately the same range of semantic contents in different contexts—plausibly, including varieties of deontic possibility. It’s hard to imagine contexts in which

You are not in a position to say what she just said

and

You can’t say what she just said

fail to express approximately the same proposition—for example, the proposition that, in view of a’s legal obligations, a can’t say what b just said, where a is the person being addressed and b is the person referred to by ‘she’.²² Thus, ‘one in a position to know that’ has approximately the same context-independent meaning (character) as.

λp.◇Kp,

with ◇ interpreted as expressing the modality determined by the context of speech or writing. When the modality is deontic, axiom (K/K^P) (Kφ → K^Pφ) will not hold, but L is a good enough logic of ‘in a position to know’, since the senses of ‘in a position’ that are at issue in epistemology when ‘in a position’ combines with ‘know’ are never deontic, as far as we can tell.

Note what follows: even in non-deontic senses of ‘in a position to’, being in a position to know is not factive. And indeed it is easy to find examples of its non-factivity. For example, each of us is in a position to thump this table. And each of us is also in a position to thump this table while knowing that he is thumping it. But then, since neither of us in fact thumps this table, each of is in a position to know something (namely, that he is thumping this table) that is actually false.

Why is the view that ‘in a position to know’ is factive so tempting? Note first that ‘can know’ displays the same appearance of factivity. One does not normally say—at least without further elaboration—either that one ‘can know’, ‘could know’ (etc.) or that one ‘cannot know’, ‘could not have known’ (etc.) φ unless one takes φ to be true. Consider:

John could not have known that we were out of cocktail olives.

One does not even normally assert a subjunctive conditional with ‘might/could have known φ’ either in the consequent or the antecedent unless one takes φ to be true:

If you had read the emails, you might have known that the meeting was rescheduled.

If I could have known that the meeting was rescheduled, my lateness would not have been excusable.

We are not looking at a special feature of ‘in a position to know’ but at a special feature of factive verbs, such as ‘realize’, ‘learn’, and ‘acknowledge’. The result of combining any of these with either a possibility modal or ‘in a position to’ is an operator that appears to be factive and moreover ‘projects’ this appearance of factivity out of a variety of constructions when embedded. It’s natural enough to describe this kind of ‘projected’ content as a ‘presupposition’. In fact, the term ‘factive’ was originally introduced for the kind of presupposition triggered by ‘know’ and other factive verbs, and that this class of verbs is the paradigm of the presupposition trigger in the literature.²³

Now we see the solution to the logical mystery: Of course being in a position to know does not have a normal modal logic. Its logic is exactly that of λp.◇Kp (‘one can know’), with ◇ restricted by some condition. For a variety of restricting conditions and a variety of propositions p, one can know p and can know ¬p, but one can never know p ∧ ¬p, as would be required by a normal modal logic.

Philosophers are of course free to use ‘in a position to know’ as a term of art. Indeed it is quite clear that it is integral to the use of ‘in a position to know’ in epistemology that it is supposed to be factive. If our conjecture about the use of ‘in a position to know’ in English is correct, then this means that it is integral to that practice to be using ‘in a position to know’ in a way that is a little deviant vis-à-vis ordinary English. There need be no great shame in that. However, if you do insist on a using ‘in a position to know’ in a way that secures factivity, you will have some uncomfortable choices to make. For it is also the habit of epistemologists to reason as if ‘in a position to know’ has a normal modal logic, that being in a position to know is entailed by knowing, and that it entails the possibility of knowing. So, by the results of this paper, something has to give. If one reasons using ‘in a position to know’ without being clear about the logic of ‘being in a position to know’ and what one means by it, there is a danger that one will be left with an expression that is too vague to be interesting. And without such clarity, there is also the danger that epistemologists will tend to fall back on their understanding of the ordinary English ‘in a position to know’ which, if we are right, is unsuitable as a guide to any factive use of that expression.

Appendix: Proofs of the main results

We begin with

(3) (K_K^P) + (NEC_K^P) + (DIST_K) ⊢ K^Pφ ↔ Kφ.

Proof

Below is an abbreviated derivation of K^Pφ ↔ Kφ in L + (K_K^P) + (NEC_K^P) + (DIST_K), where ‘K’ (boldface) indicates provability using classical logic and (NEC_□) from (K_□), and

α := ∀p(p ↔ @p)

α*  := ¬K(α ∧ φ)

1. α* → □ @α*	(RIG@)
2. α* → □ (∀p(p ↔ @p) → (α* ↔ @α*))	(UI), (NEC□)
3. α* → □((α* ↔ @α*) ↔ α*)	1, K
4. α* → □(∀p(p ↔ @p) → α*)	2, 3, K
5. α* → □(α → α*)	4 abbreviated
6. ¬K(α ∧ φ) → □(α → ¬K(α ∧ φ)),	5, with α* unabbreviated
7. ¬K(α ∧ φ) → □((α ∧ φ) → ¬K(α ∧ φ)),	6, K
8. □(K(α ∧ φ) → (α ∧ φ))	(TK), (NEC□)
9. ¬K(α ∧ φ) → □¬K(α ∧ φ)	7, 8, K
10. ¬K(α ∧ φ) → ¬◇K(α ∧ φ)	9, K
11. ◇K(α ∧ φ) → K(α ∧ φ)	10
12. ◇K(α ∧ φ) → Kφ	11, (DISTK)
13. p ↔ @p	(T□), (T@) (RIG@)
14. ∀p(p ↔ @p)	13, (UG)
15. KP(φ → (α ∧ φ))	14, (NECKP)
16. KPφ → KP(α ∧ φ)	15, (KKP)
17. KP(α ∧ φ) → ◇K(α ∧ φ)	(KP/◇)
18. KPφ → ◇K(α ∧ φ)	16, 17
19. KPφ → Kφ	12, 18
20. Kφ → KPφ	(K/KP)
21. KPφ ↔ Kφ	19, 20

(1) (K_K^P) + (NEC_K^P) ⊢ K^Pφ ↔ K^∧φ.

Proof

To show this, replace line 12 in the above with K(α ∧ φ) → ∃pK(p ∧ φ), where p is not free in φ (which is equivalent by contraposition and quantifier duality to an instance of (UI)), and proceed:

11. ◇K(α ∧ φ) → K(α ∧ φ)
12. K(α ∧ φ) → ∃pK(p ∧ φ)	UI
13. p ↔ @p	(T□), (T@) (RIG@)
14. ∀p(p ↔ @p)	13, (UG)
15. α	14 abbreviated
16. φ → (α ∧ φ))	15
17. KP(φ → (α ∧ φ)))	16, (NECKP)
18. KPφ → KP(φ ∧ α)	(KKP)
19. KP(φ ∧ α) → ◇K(φ ∧ α)	(KP/◇)
20. KPφ → ∃pK(p ∧ φ)	11, 12, 18, 19
21. K(p ∧ φ) → KP(p ∧ φ)	(K/KP)
22. KP((p ∧ φ) → φ)	(NECKP)
23. KP((p ∧ φ) → φ) → (KP(p ∧ φ) → KPφ)	(KKP)
24. KP(p ∧ φ) → KPφ	22, 23
25. K(p ∧ φ) → KPφ	21, 24
26. ¬KPφ → ¬K(p ∧ φ)	25
27. ¬KPφ → ∀p¬K(p ∧ φ)	26, (UG)
28. ¬∀p¬K(p ∧ φ) → KPφ	27
29. ∃pK(p ∧ φ) → KPφ	28, definition of ∃p
30.∃pK(p ∧ φ) ↔ KPφ	29, 20

(2) The logic of K^∧ in L + (K_K^P) + (NEC_K^P) is normal.

Proof

Immediate from (1).

(4) The logic of K in L + (K_K^P) + (NEC_K^P) + (DIST_K) is normal.

Proof

Immediate from (3).

(5) L + (NEC_K^P) is closed under (NEC_K^∧).

Proof

To show this, let (NEC_K^P) ⊢ φ and continue from line 11 in the proof of (3) as follows.

11. ◇K(α ∧ φ) → K(α ∧ φ)
12. p ↔ @p	(T□), (T@) (RIG@)
13. ∀p(p ↔ @p)	12, (UG)
14. φ	By hypothesis
15. φ ∧ α	13, 14
16. KP(φ ∧ α)	15, (NECKP)
17. KP(φ ∧ α) → ◇K(φ ∧ α)	(KP/◇)
18. K(α ∧ φ)	11, 16, 17
19. K(α ∧ φ) → ∃pK(p ∧ φ)	UI and quantifier duality
20. ∃pK(p ∧ φ)	18, 19

(6) L + (NEC_K^P) + (DIST_K) is closed under (NEC_K).

Proof

Immediate from the proof of (5).

(7) (K_K^P) ⊢ K^P(φ → ψ) → (K^Pφ → ◇Kψ).

Proof

Immediate from axiom (K^P/◇).