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

[ctchou]

You have the notion of a HeytingModel above. Is there a corresponding notion for classical logic?

Conversely, is HeytingModel really necessary? Would an abbreviation for Atom → H, where H is a GeneralizedHeytingAlgebra, suffice?

I'm basically asking for a consistent treatment of the two.

[thomaskwaring]

I bundled the algebra H into the type because I wanted a single type HeytingModel Atom to capture possibly varying Heyting algebras — eg we might want a theorem saying semantics in finite Heyting algebras are complete, which is not true if you restrict to a single algebra (different to classical logic, where the single Boolean algebra Prop / Bool is enough).

In any case, these are mostly there as examples to illustrate the general design, a full treatment of semantics for propositional logic will be it's own development & certainly these questions require discussion.

[ctchou]

Two questions/comments:
(1) What is the distinction between Models and InterpModels? I know the latter is a special case of the former. But is there an example of the former which is not in the form of the latter?
(2) There is still no concrete example of how ParamModels is actually used.