MOLTAP

• Overview
• The prover
• Examples
• Users guide
• Syntax reference
• Download

Theory

• Introduction
• Propositional tableaux
• Modal tableaux
• KD, S4, S5, etc.
• Soundness
• Completeness
• Knowledge in groups
• Common knowledge

Implementation

• The basics
• Representing tableaux
• Working with models

Conclusion

• Conclusions
• Related work
• References

Generating a model

Maximal sets

When the proof search fails we have a sequent to which no further rules can be applied. We call the resulting sequents maximal sequents.

Definition: We say that a set Γ is maximal when

• ⊢ Γ is not an axiom.
• ⊢ Γ is not the consequence of a rule whose principal formulas have not been used before.

Two important properties of maximal sets Γ are

• Because of the "deep" meta-rules, for all [Δ]_i ∈ Γ, Δ is also maximal.
• A maximal set can not contain both p⁺ and p^-.

Building the model

From a maximal set Φ we can generate a model. A maximal set represents a failed search for a proof, if one of the elements of the set were true we would be done. So the idea is to generate a model where everything in the maximal set is false.

We define our counter model M_Φ = ⟨S_Φ,R,V⟩ by

So there is a world for the maximal set Φ itself, and for all [Δ]_i in Φ there is world s_Δ that is accessible from s_Φ by agent i. We then choose the valuation such that precisely those propositions are true that occur negatively in the set.

Completeness

Truth lemma

The next step in the completeness proof is

The proof proceeds by induction over the structure of the formula χ and the relations R_i.

Assume the induction hypothesis; that given a signed formula χ^± the truth lemma holds for

1. all subformulas of χ, and
2. all sets Δ where [Δ]_i ∈ Γ.

Then to show that the truth lemma holds for χ^± there is a case to consider for each type of signed formula:

1. p^- ∈ Γ
   then by definition p ∉ V(s_Γ). So M,s_G ⊨ p and M,s_G ⊭ p^-.
2. p⁺ ∈ Γ
   then because Φ is maximal, p^- ∉ Γ and hence by definition p ∉ V(s_Γ). So M,s_G ⊭ p⁺
3. ψ ∧ χ⁺ ∈ Γ
   then because of maximality either ψ⁺ ∈ Γ or χ⁺ ∈ Γ; otherwise the ∧⁺ rule could be applied to the sequent and it would not have been maximal. Let's say that ψ⁺ ∈ Γ. By the induction hypothesis we may assume that M,s_G ⊭ ψ⁺, so also M,s_G ⊭ ψ ∧ χ⁺
4. ψ ∨ χ⁺ ∈ Γ
   then because of maximality either ψ⁺ ∈ Γ and χ⁺ ∈ Γ; otherwise the ∧⁺ rule could be applied to the sequent and it would not have been maximal. By the induction hypothesis we may assume that M,s_G ⊭ ψ⁺ and M,s_G ⊭ χ⁺. So also M,s_G ⊭ ψ ∨ χ⁺.
5. □_i ψ⁺ ∈ Γ
   then there exists a [Δ]_i ∈ Γ with ψ⁺ ∈ Δ. By the induction hypothesis we have M,s_D ⊭ psi⁺. Since [Δ]_i ∈ Γ we have that s_GR_is_D, so M,s_D ⊭ □_i psi⁺.
6. □_i ψ^- ∈ Γ.
   Let Δ be an arbitrary sequent such that s_GR_is_D, so [Δ]_i ∈ Γ. Then because of maximality it must be the case that ψ^- ∈ Δ, otherwise rule □^- could be applied to Γ. By the induction hypothesis we have M,s_D ⊭ psi^-. Because the choice of Δ was arbitrary this holds for all such Δ and hence M,s_G ⊭ □_i ψ^-.
7. The other cases for duals of the above formulas are analogous.

So by induction the truth lemma holds for all χ^± ∈ Γ for all Γ with s_G ∈ S_Φ.

Termination

One final piece of the completeness puzzle remains. It must be possible to construct either a maximal set or a valid derivation for all formulas.

This derivation is constructed with a proof search, as described previously. In the proof search rules are applied bottom up for as long as possible.

All logical rules, when used from the bottom to the top, either

• add subformulas of the current formula to the sequent (all propositional rules and the □^- rule), or
• add a nested sequent containing subformulas (the □⁺ rule), or
• move formulas out of nested sequents (the 4 and 5 rules).

In the first two cases only smaller things are added. Formulas of the third type can only be used a finite number of times, since

The input formula is finite, so eventually no more subformulas can be added. Therefore, the proof search always terminates.

Completeness

We apply the above proof search algorithm to a formula φ⁺ that is not valid (⊭ φ⁺). Because of soundness the proof search must fail, so we end up with a maximal set Φ. From this set a counter model M_Φ is then generated.

With the copying meta-rule we have ensured that φ⁺ ∈ Φ. By the truth lemma then M,s_Γ ⊭ ψ. We have found our counter model.

So if the search for a proof of φ fails, it must be the case that φ is not valid. And since the proof search always terminates the proof search for all valid formulas must succeed; our logic is complete, ⊨ φ⁺ ⇒ ⊢ φ⁺.

Simplifying the model

Counter models are not just interesting from a theoretical point of view, they can also be interesting to the user of a theorem prover. For example, when entering a → K₁ K₁ a the (S5) proof search will terminate with the maximal set

The model generated from this set will contain three worlds, one for Φ, one for [K₁ a⁺]₁ and one for [a⁺]₁. To ensure that what we end up with is an S5 model reflexive, transitive and symmetric arrows are added. Graphically the resulting model will look like:

Clearly the world s_{K1 a⁺} in the bottom right is superfluous and can be removed. The program therefore contains a very simple algorithm to minimize models:

1. For each world in M, construct a model M' with that world removed.
2. For each pair of world in M, construct a model M' with those two worlds merged. That is, the union taken of the valuation and of the outgoing and incoming relations.
3. If such an M' is sill a counter model to φ, then repeat.

After minimizing the model becomes simply