feat(Foundations/Logic): Notation typeclasses and models

[thomaskwaring]

A proposal for typeclasses expressing that a type of "propositions" has semantics in a type of "models".

Main definitions

• Models α β : objects of type β carry a predicate Satisfies on objects of type α.
• ParamModels α β : objects M : β carry a satisfaction relation parametrised over some auxiliary Param M : Type*
• InterpModels α β : each M : β has an associated ground type Ground M, an interpretation interp : α → Ground M and a filter : Set (Ground β), which induces a forcing relation as Satisfies M a := interp a ∈ filter M.
• Soundness and completeness wrt an inference system

I've tried to add enough examples to show how this might be used, but the design ought to be discussed before we settle on anything this general.

[ctchou]

I still find this notation unintuitive: w depends on b and yet it appears to the left of b.

For that matter, why does the model b appear in a bracket to the right of the turnstile ⊨ in this and the notation for Models/Satisfies? It seems to me standard for the model to appear to the left of the ⊨.