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.

[benbrastmckie]

Hi @thomaskwaring — following our Zulip discussion in the Propositional Logic thread:

I noticed this PR creates Foundations/Logic/Connectives.lean with semantic typeclasses (Models, ParamModels, InterpModels), where PR #648 creates the same file path with syntactic connective typeclasses (HasBot, HasImp, etc.). PR #648's description already flags this.

The content is complementary rather than conflicting — yours addresses the semantic/model side, ours addresses the syntactic/connective side. They could coexist in the same file or be split into Connectives.lean (syntax) and Models.lean (semantics). Happy to coordinate on the file organization.

Your algebraic completeness theorem over GeneralizedHeytingAlgebra with the v |= T framing is exactly the right generalization — as I mentioned on Zulip, that architecture is orthogonal to the formula type design and we should adopt it. I'd be happy to collaborate on integrating the algebraic semantics layer.