Experimental repo to teach myself --- and, hopefully, other people --- about Kripke semantics for various non-classical logics.

Beware of bugs in the code; to mangle Knuth, I have only typechecked it, not tried it.

There is a frontend on gh-pages but it should be considered highly unstable.

Basic data types are found in the Data.Kripke.Kripke module. A Node represents a possible world; a KripkeFrame is a record containing an array worlds of Nodes and an array relation of pairs of Nodes; if (w, x) is an element of relation we say that x is accessible from w.

An Atom is a variable; a Model is a record with a Kripke frame; an array valuation of pairs of Atoms and Nodes representing the atoms that are true in a given world; and an array domain of pairs of Atoms and Nodes.

An Evaluation err expr is a wrapper for a function Model -> Either err (Node -> expr -> Boolean), that checks that a model is consistent with the axioms of a given logic and, if it is, evaluates whether a given expression is true in a given world. The runEvaluation unwrapper alters the type to Model -> Node -> expr -> Either err Boolean; the checkModel unwrapper alters it to Model -> Either err Unit.

For a Model to be a valid Kripke model for a given logic it typically must satisfy some axioms (depending on the logic), for instance the frame relation must be reflexive or transitive. Primitives for checking that a model conforms to certain rules are in Data.Kripke.Validation; these return applicatives whose error messages can be combined.

Intuitionistic logic is a subset of classical logic that more accurately represents notions of constructive proof and of programming (especially typed functional programming).

Propositional logic is the study of the truth or falsity of propositions formed by other propositions, such as "a and b", "a or b", or "a and b implies b". Intuitionistic propositional logic is the intuitionistic form of propositional logic.

An evaluation for intuitionistic propositional logic can be found in the Logics.Intuitionistic.Propositional module.

Much more to come here...

Modal logics extend the expressions of classical logic to encompass various modalities such as necessity, belief, obligation, and time.

Alethic modal logic, often simply called "modal logic", deals with necessity and possibility. An evaluation for the propositional fragment of alethic modal logic can be found in the Logics.Modal.Alethic.Propositional module.