It is customary nowadays to have the introduction rule for the possibility operator "◊" be a two-edged negation of the necessity operator "□": ◊A = ~□~A. It is also possible (haha!) but less common, if I understand things correctly, to go the other direction and say that □A = ~◊~A. I have no direct objection to either equation and could even persuade myself of the plausibility of both on the basis of at least two arguments, one on behalf of each equation.
On the other hand, I remember that when I read the Critique of Pure Reason the second (or maybe third†) time that I agreed with the following passage:
...necessity is nothing but existence, which is given through the possibility itself. Let it not be supposed, however, that the third category is merely a deduced, and not a primitive conception of the pure understanding. For the conjunction of the first and second, in order to produce the third conception, requires a particular function of the understanding, which is by no means identical with those which are exercised in the first and second.
Taken altogether, the passage suggests (in modern terms) having both "◊" and "□" as primitives, even if there is otherwise a way to define necessity in terms of not only possibility, as it turns out, but actuality. So let's focus on that "otherwise," though. My first thought was something like □A = (◊A → A). However, I wanted to merge the modern sensibilities regarding this topic with Kant's, and thought that if □A = ~◊~A, then we could say something like (◊A → A) → ~◊~A, and avoid having an equation, to some extent.
Besides being a somewhat anachronistic option in Kant exegesis, what place does such a conditional have modulo up-to-date modal logic? I feel like I've seen a similar string of symbols before. Admittedly, especially when reading about modal logics broadly and they use the same operator symbols for each modal subsystem, just with the in-text caveat that the section in which the symbols are used determines which modality is at work, it is not always clear to me how different two strings of symbols actually are, so maybe I'm not remembering things clearly. The closest thing I could find in the SEP article on modal logic was something named after Brouwer about actuality implying necessary possibility, but that proposed implication is not really the one I'm thinking of.
Or is it? I don't really know. I don't know enough of the technical details of the different systems of modal logic. So my question is: is (◊A → A) → ~◊~A a known implication of at least one of the established systems of modal logic?
†I don't really know what happened the first time I read that book, because when I read it the second time, I was not only confused by the text, but by the fact that I didn't remember anything from the first time I read it. Like, my mind did not retain or even seem to take in any of the text, that first time through.
