Let us denote $C$ the modal system obtained by adding the axiom $ \alpha \rightarrow \lozenge \square \alpha$ to the axiom $K$ and all the propositional tautologies.
As said in the title, I'm looking for a K-proof for $$ \vdash_C (\square p \rightarrow \lozenge p),$$ but also for $$\vdash_C (\lozenge p \rightarrow \square p).$$
I know these proofs should exist since a Kripke frame verifies the formula $p \rightarrow \lozenge \square p$ if and only if it verifies $$ (1) \ \ \forall x ( \exists y : (x \mathrel{R} y) \text{ and } (y \mathrel{R} z \Rightarrow z = x) ).$$
It particular $(1)$ implies that the frame is serial ( i.e. $\forall x (\exists y : x \mathrel{R} y)$), that is $ \square p \rightarrow \lozenge p$ is true, and that the frame is functional ( i.e. ($x \mathrel{R} y \text{ and } x \mathrel{R} z) \Rightarrow y =z$), that is $\lozenge p \rightarrow \square p$ is true.
Thank you for any answer !
(For the first): Consider the set up where $\neg p$ holds at the actual world and where no world is accessible from that world. Then the lhs of your sequent evaluates as true, and the right false ... (since $\Box p$ is vacuously true, and $\Diamond p$ is false).
(For the second): Consider the two-world set-up where in the actual self-accessible world $\neg p$, and there is one other accessible world where $p$. The lhs of your sequent evaluates as true, and the right false ...
So something is amiss there? Neither is a valid K-sequent so neither is K-provable.