0
$\begingroup$

An intuitionistic Kripke model is a triple $\langle W,\leq, \Vdash \rangle$, where $\langle W,\leq \rangle$ is a preordered Kripke frame, and $\Vdash$ satisfies the following condition of hereditariness (or monotonicity):

if $P$ is a propositional variable, $w\leq u$, and $w\Vdash P$, then $u\Vdash P$.

  • Are there intermediate logics (excluding classical logic), including intermediate modal logics (i.e intermediate logics which contain modalities) for which there are no Kripke models in the above sense?

  • (If so,) what is the smallest such intermediate logic?

  • If there are no such intermediate logics, what is the proof of this claim?

I was thinking particularly of intuitionistic logics to which is adjoined some modality $\bigcirc$ which does not obey hereditariness. I.e, for which we have:

$P$ is a propositional variable, $w\leq u$, $w\Vdash \bigcirc P$ and $u\not\Vdash \bigcirc P$.


Edit

It has been observed below that classical logic can be given a Kripke model in the above sense. Does this entail that any intermediate logic can be given a Kripke model?

$\endgroup$
  • 1
    $\begingroup$ It is not clear what you are asking. The term "Kripke model" means a certain interpretation of propositional calculus, namely in the Heyting algebra generated as the upper sets of a partial order (or a preorder). Every such interpretation will satisfy monotonicity by design. If you are looking for something that is not a Kripke model, then it's not clear what monotonicity means (ok, as long as it's a sheaf model we'll be able to guess). In other words, it sounds like your question is a terminological question masquerading as a mathematical question. $\endgroup$ – Andrej Bauer Dec 17 '18 at 13:50
  • 1
    $\begingroup$ I can put it in another way: monotonicity is a property of semantics of propositional logic. It therefore makes no sense to ask whether there are logics which violate it. Even classical logic satisfies the monotonicity requirement, trivially so because there aren't any interesting Kripke models of classical logic. (But there are Kripke models of classical logic!) $\endgroup$ – Andrej Bauer Dec 17 '18 at 13:56
  • $\begingroup$ I am asking whether there are intermediate logic for which there are no standard Kripke models. There are modal logics for which there is no Kripke model. $\endgroup$ – user65526 Dec 17 '18 at 14:02
  • $\begingroup$ I have edited my question $\endgroup$ – user65526 Dec 17 '18 at 14:03
  • $\begingroup$ But even classical logics have Kripke models (consider the discrete preorder), so what are you asking? $\endgroup$ – Andrej Bauer Dec 17 '18 at 14:13
2
$\begingroup$

Every propositional logic $L$ weaker than classical logic (i.e., any logic whose provable propositions are a subset of classically provable propositions) has a Kripke model. Just take $W = \{\star\}$, the frame with a single element, and the trivial preorder. The model is equivalent to the boolean algebra $\{\bot, \top\}$, therefore it validates all classically provable propositions and is a model of $L$.

I should also note that monotonicity is a property of Kripke models, not of logics. A Kripke model is just the Heyting algebra of the upper sets of a preorder, by design. Of course the upper sets are upward closed.

You mention modal logics, but for those we need to augment Kripke models with an accessibility relation, and in any case, monotonicity still holds by virtue of what a Kripke model is.

$\endgroup$
  • $\begingroup$ Thank you. :) But I did not mean to exclude predicate logics. Is this the case also for intermediate predicate logics? $\endgroup$ – user65526 Dec 17 '18 at 14:48
  • 3
    $\begingroup$ Everything I said applies to predicate logics as well. In fact, we can generalize to higher-order intuitionistic logic by expanding Kripke models to presheaf toposes on preorders. $\endgroup$ – Andrej Bauer Dec 17 '18 at 14:53
  • $\begingroup$ The reason I asked the question was because I found a logic with a modal operator which was not hereditary. It was suggested to me that this showed that we could not define the operator intuitionistically. But is this line of thought therefore mistaken? $\endgroup$ – user65526 Dec 17 '18 at 15:33
  • 2
    $\begingroup$ That depends on pesky details. $\endgroup$ – Andrej Bauer Dec 17 '18 at 15:47

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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