canonical model


Recall that a logic is a set of wff’s containing all tautologiesMathworldPlanetmath and closed underPlanetmathPlanetmath modus ponensMathworldPlanetmath. Given a logic Λ, a set Δ of wff’s is Λ-consistent if can not be deduced from Δ given Λ. Λ itself is said to be Λ-consistent if can not be deduced from the empty setMathworldPlanetmath. Let Λ be a consistent normal modal logic. The canonical frame for Λ is the Kripke frame Λ:=(WΛ,RΛ), where

  1. 1.

    WΛ is the set of all maximally consistent sets, and

  2. 2.

    wRΛu iff Aw implies Au for any wff A.

If we define Δw:={BBw}, then the second condition above reads wRΛu iff Δwu.

The canonical model of Λ based on Λ is the pair MΛ:=(Λ,VΛ), where

  • V(p):={wWΛpw}.

The main result regarding the canonical model of Λ is:

Theorem 1.

MΛA iff ΛA, where A is any wff.

Since the logic Λ is the intersectionMathworldPlanetmath of all maximally consistent sets (see here (http://planetmath.org/LindenbaumsLemma)), the theorem is the result of the following:

Proposition 1.

MΛwA iff Aw.

which is the result of the following:

Lemma 1.

For any world w in MΛ, Aw iff Au for all worlds u such that wRΛu.

Proof.

Suppose Aw and wRΛu. Then Au by the definition of RΛ. Conversely, suppose Au for all u such that wRΛu. In other words, Au for all u such that Δwu, or A{uΔwu}. But {uΔwu}=Ded(Δw), the deductive closure of Δw, so ΔwA, and therefore ΔwA (see here (http://planetmath.org/SyntacticPropertiesOfANormalModalLogic)), or wA (since Δww), or Aw (since w is maximally consistent). ∎

Proof of PropositionPlanetmathPlanetmath 1. We do inductionMathworldPlanetmath on the number n of logical connectives in A. If n=0, then A is either a propositional variable or . The former is just the definition of VΛ. The later case is just the definition of Λ-consistency. Next, if A is BC, then MΛwA iff either MΛ⊧̸wB or MΛwC iff Bw or Cw iff ¬Bw or Cw iff ¬BCw iff Aw. Finally, if A is B, then MΛwB iff Bw iff Bu for all u such that wRΛu iff MΛuB for all u such that wRΛu.

Recall that a logic is completePlanetmathPlanetmathPlanetmathPlanetmath in a frame if it is complete in every model based on the frame. As a corollary to Theorem 1, we have

Corollary 1.

Λ is complete in its canonical frame FΛ.

Proof.

Any wff valid in every model based on Λ is valid in MΛ in particular, and therefore a theorem of Λ by Theorem 1. ∎

The converse is not true. There are in fact normal modal logics that are sound in no frames at all.

Canonical models are useful in proving the completeness theorems for many common normal modal logics. To prove that a logic is complete in a class of frames, by the corollary above, it is enough to show that the canonical frame is in the class. Here are two examples:

  1. 1.

    Let Λ be the smallest normal logic containing the schema A. Then Λ is complete in the class of null frames.

    Proof.

    By the discussion above, it is enough to show that Λ is a null frame: the assumptionPlanetmathPlanetmath wu(wRΛu) leads to a contradictionMathworldPlanetmathPlanetmath. Suppose wRΛu. Then Δwu. This means that if Aw, then Au. But A is a theorem (in Λ), Aw for any wff A. This means that Au for any wff A, or that u is inconsistent, a contradiction. ∎

  2. 2.

    Let Λ be the smallest normal logic containing the schema AA. Then Λ is complete in the class of weak identityPlanetmathPlanetmathPlanetmathPlanetmath frames (a binary relationMathworldPlanetmath R is weak identity it is satisfies the condition xy(xRyx=y)).

    Proof.

    Again, we show that RΛ is weak identity. Suppose wRΛu. Then for any A, Aw implies that Au. Now, if Aw, then applying modus ponens to AA, we get that Aw since w is closed under modus ponens. But this means that Au. So wu. But since both w and u are maximal, they are the same. ∎

Title canonical model
Canonical name CanonicalModel
Date of creation 2013-03-22 19:35:01
Last modified on 2013-03-22 19:35:01
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 15
Author CWoo (3771)
Entry type Definition
Classification msc 03B45
Defines canonical frame
\@unrecurse