2
$\begingroup$

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 !

$\endgroup$
2
$\begingroup$

(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.

$\endgroup$
  • $\begingroup$ I might be mistaken, but I think we can't deduct $p$ from $\square p$ unless we are working with reflexive Kripke frames, which is not the case in general. $\endgroup$ – L.DeR Dec 13 '18 at 16:15
  • $\begingroup$ Oops, getting my K's and T's entangled! $\endgroup$ – Peter Smith Dec 13 '18 at 16:58
  • 2
    $\begingroup$ But I've given you, in each case, a K-model where the l.h. wff is true and the r.h. wff false. So (by soundness for the K proof system) the l.h. doesn't K-prove the r.h. wff. The implications aren't true. $\endgroup$ – Peter Smith Dec 13 '18 at 20:32
  • 2
    $\begingroup$ Agree on nomenclature of en.wikipedia.org/wiki/Kripke_semantics Then K is sound w.r.t. the inferences valid in every K frame, so in particular if $\alpha \vdash_K \beta$, then given any K frame, and any valuation of the relevant atoms in that frame, if $\alpha$ comes out true, so does $\beta$. So it suffices to refute $\alpha \vdash_K \beta$ to find one K frame and one valuation on that frame which makes $\alpha$ true and $\beta$ false. No? $\endgroup$ – Peter Smith Dec 13 '18 at 23:14
  • 1
    $\begingroup$ I'd have said "Let C be the modal system you get by adding to K all axioms of the form $\alpha \to \Diamond\Box\alpha$. Then how do we show $\vdash_C \Box p \to \Diamond p$, etc." [I've plucked the label "C" out of the air -- I don't know off-hand if there is a label already in use.] $\endgroup$ – Peter Smith Dec 14 '18 at 10:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.