Defining Kripke models and the canonical model for $S4$ modal logic

Question

I have defined the syntax of modal logic in Coq and now I'm having trouble with the semantics. This is how I defined the Kripke model:

Parameter x : Type.
Definition world : Type := x.
Class KripkeModel : Type := 
{
    Worlds : world -> Prop;
    Access : world -> world -> Prop;
    Int : world -> prop_atom -> Prop;

    (* Reflexivity & Transitivity *)
    Acc_refl (w : world) : Access w w;
    Acc_trans (w u v : world) : Access w u -> Access u v -> Access w v;
}.

But now every time I want to check $\mathfrak{M}, w \vDash \phi$, I need a proof for M.(Access) w first to show that the node is actually in the model. I think there are quite many issues with this definition and I need to change many things, including the definition of my interpretation function.
I'm also having trouble defining canonical models. (I want to prove Completeness)

I have defined a context as follows: Definition Context : Type := list S4_props. Where S4_Props is the type of the possible propositions of $S4$. For my canonical model, I need to have contexts as nodes. We also know the accessibility relation is defined via inclusion. I don't know how to define the accessibility relation or the interpretation function of the canonical model with my current definition.

Answer 1

You define world as a parameter and then Worlds as a function world -> Prop, so it's an implementation of a subset of world without a decidable membership notion. That seems very annoying, as you note.

I would set up the set of worlds such that membership in that set is clearly decidable. A way to do this is to postulate that the set of worlds is always finite and use some Coq implementation of finite sets (I like MathComp's finmap). If you want to be able to describe infinite models you need to use some other version of set, but one that is decidable would be preferable.

Things also become easier if you don't include so many restrictions on your models all at once (i.e., exclude reflexivity and transitivity to a first approximation and define a second version with those assumptions). You don't need them to define satisfiability, so it would be annoying to have to prove them every time you want to check the satisfiability of a model!

It's also easier if you let accessibility and Int be obviously-decidable notions (i.e., ending in bool instead of Prop).

Here is what I would do (using MathComp because I'm not really familiar with the Standard Library):

From mathcomp Require Import all_ssreflect finmap.

Parameter prop_atom : Type.
Parameter WType : choiceType.

Record rawModel := RawModel {
  World :> {fset WType};
  Access : World -> World -> bool;
  Int : World -> prop_atom -> bool;
}.

Definition refl (M : rawModel) := reflexive (Access M).
Definition trans (M : rawModel) := transitive (Access M).

Record model := Model {
  rawModel_of_model :> rawModel;
  _ : refl rawModel_of_model;
  _ : trans rawModel_of_model;
}.

Fixpoint sat (M : rawModel) : Prop. Admitted.
(* note how the input is rawModel and not model *)
(* you can also define sat : rawModel -> bool if you prefer *)

I have done something very similar for a quantified modal logic, and my suggestions above are informed by that experience. Here are links to the definition of Kripke semantics, the proof of Kripke soundness, and the proof of Kripke completeness.