There's an interesting subtlety here. The statement
(1): ◇A is defined to mean ~◻~A,
is extremely strong. For example, thinking in terms of a sequent calculus with both ◇ and ◻ included as primitives, this corresponds to having available the following (hypothesis-free) inference rule:
(A): For every sentence p, if q is a sentence gotten from p by ...
First of all, you can just define things it were a game, because you can Esasy create a inconsistent system of axioms, you had to justify and if possible just prove the stament form the other axioms.
◇(◇A) = ~◻~(◇A) By application of the definition of ◇x
~◻~(◇A) = ~◻~~◻~A By a second application of the definition of ◇x
Hence has been proved that ◇◇A ...
Am I on the right track, or is this not a provable statement?
I'm going to go further than that. Not only is this statement not provable in K, but in fact there is no reasonable set of axioms under which a proof should exist.
We can see this by taking the contrapositive. If you can prove ~◻p → ~p, then you can also prove p → ◻p. And since we know nothing at ...
Consider the phrase "I know that I know nothing." This would be a logical contradiction so you must be certain of something. Now that we dispelled global skepticism (the idea that we cannot be certain about anything) we can analyze how we came to this notion.
If you are not a mystic, there are only two ways for gaining knowledge: the senses and ...