Theorem Provers with Counter Models from xpe

Motohiko Mouri

                   mouri@jaist.ac.jp

JAIST, Tatsunokuti, Ishikawa, 923–1292, Japan

              http://www.jaist.ac.jp/~mouri

Abstract Xpe is a grammar editor for proof figure on TEX. It makes you easier to draw

proof figure. And theorem provers called from xpe help you to research and write papers.

1 Introduction

How do you draw proof figure on TEX? Most of us must use ‘proof.sty’ macros. But we feel confusion to draw and fix one because it has a structural problem that tree structure is expressed by so many brackets. We would desire another method to draw it. To that solution, I produce xpe here.

Xpe (X window system Proof Editor) is a grammar editor for proof figure. It interprets and displays TEXcommand, for example \Gamma ⋯ Γ,\Delta ⋯ Δ,\supset ⋯ ⊃, and so on. It supports cut and paste formulae. The file format for input and output is compatible with proof.sty. And it is easy to transfer from editor to xpe, and opposite. We can get WYSIWYG(What You See Is What You Get) environment to draw proof figure.

In addition, some theorem provers are supported. They are propositional logics:

• classical logic

• intuitionistic logic

• modal logics K, KT, S4, S5

• lambda type assign system

At this time, these theorem provers and proof checker are supported:

• modal logics K, KT with counter models (called K+, KT+)

• modal logics K5, KD5

• cut elimination checker

Most of this paper refers to System K+ and KT+ that are theorem provers of K or KT with counter modes.

By the way, xpe is a free software. Everybody can download from above my homepage.

2 System K+

Modal logic K is defined by adding (□) rule to classical logic LK of sequent calculus system. On decision procedure, it is defined by adding (□) rule including weakening to Wang’s system (see [4],[1]). The rules are shown at figure 1.

{Γ → A \atop □Γ → □A} (□) {Γ → A \atop Δ, □Γ → □A, Σ} (□)

Figure 1: □ rules for LK and Wang’s system

If we generate a counter model for a unprovable sequent, we need take the System K+ (figure 2). We consider both sides of a sequent as multi–sets. It is enough to consider as sets, too. But to make it more easily to understand decision procedure in the theorem prover, both sides of sequent are treated as multi–sets.

Γ, p → p, Δ

\begin{matrix}Γ → Δ, A & Γ, B → Δ \\ Γ, A ⊃ B → Δ \end{matrix} (⊃ L)  {Γ, A → Δ, B \atop Γ → Δ, A ⊃ B} (⊃ R)

{Γ, A, B → Δ \atop Γ, A ∧ B → Δ} (∧L)  \begin{matrix}Γ → Δ, A & Γ → Δ, B \\ Γ → Δ, A ∧ B \end{matrix} (∧R)

\begin{matrix}Γ, A → Δ & Γ, B → Δ \\ Γ, A ∨ B → Δ \end{matrix} (∨L)  {Γ → Δ, A, B \atop Γ → Δ, A ∨ B} (∨R)

{Γ, A → Δ \atop Γ → Δ, ¬A} (¬R)  {Γ, A → Δ \atop Γ → Δ, ¬A} (¬R)

\begin{matrix}Γ → A_{1} & ⋯ & Γ → A_{m} \\ p_{1}, ⋯, p_{n}, □Γ → □A_{1}, ⋯, □A_{m}, q_{1}, ⋯ q_{l} \end{matrix} (□)

Figure 2: System K+

I am explaining the procedure to generate a counter model for an unprovable sequent. Here, consider □C ∨ □B ∧ D → □(¬A ∨ □C) ∨ □B. The theorem prover of K+ outputs a decision tree and a counter modes as follows:

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}{→ C \atop C, A → □C} & (□) \\ C → ¬A, □C \end{matrix} ; (¬R) ; C → ¬A ∨ □C ; (∨R) & C → B \\ □C, D → □(¬A ∨ □C), □B \end{matrix} (□) & □B, D → □(¬A ∨ □C), □B \\ □C ∨ □B, D → □(¬A ∨ □C), □B \end{matrix} & (∨L) \\ □C ∨ □B, D → □(¬A ∨ □C) ∨ □B \end{matrix} ; (∨R) ; □C ∨ □B ∧ D → □(¬A ∨ □C) ∨ □B ; (∧L) \{\} ; ⋮ . ; \{C, A\} \{C\} ; ⋮ . ; \{D\}

Figure 3: Decision tree and counter model by K+

At first, the procedure reduces logical connectives ∧, ∨, ∧ and ⊃ to easier formulae, and determines that each consequence is an initial sequents or not. If no more rule is applied, it tries to apply (□) rule. Finally each top sequent is a form like p_{1}, ⋯, p_{n}, □Γ → q_{1}, ⋯, q_{n}. The sequent corresponds to the formulae set {p_{1}, ⋯, p_{n}}.

And (□) rule corresponds a frame \begin{matrix}\{Γ, ¬A_{1}\} ⋯ \{Γ, ¬A_{m}\} \\ ↖ ↗ \\ \{p_{1}, ⋯, p_{n}\} \end{matrix} . In the system K+, it is

expressed as {Γ, ¬A_{1}} ⋯ {Γ, ¬A_{m}} ; ⋮ . ; {p_{1}, ⋯, p_{n}} by expression restriction on proof.sty.

Roughly speaking, the sequent p_{1}, ⋯, p_{n}, □Γ → □A_{1}, ⋯, □A_{m}, q_{1}, ⋯ q_{l} corresponds to the formulae set {p_{1}, ⋯, p_{n}}. On this view, each decision tree from lower to upper

corresponds to a propositional symbol set. The correspondence bitween trees and sets for that decision tree follows:

\begin{matrix}→ C & ⋯ \{\} \\ C → B & ⋯ \{C\} \\ \begin{matrix}{C, A → □C \atop C → ¬A, □C} & (¬R) \\ C → ¬A ∨ □C \end{matrix} ; (∨R) & ⋯ \{C, A\} \\ \begin{matrix}\begin{matrix}□C, D → □(¬A ∨ □C), □B & [□B, D → □(¬A ∨ □C), □B] \\ □C ∨ □B, D → □(¬A ∨ □C), □B \end{matrix} & (∨L) \\ □C ∨ □B, D → □(¬A ∨ □C) ∨ □B \end{matrix} ; (∨R) ; □C ∨ □B ∧ D → □(¬A ∨ □C) ∨ □B ; (∧L) & ⋯ \{D\} \end{matrix}

Figure 4: Relationship between tree and set

Because the sequent □B, D → □(¬A ∨ □C), □B is provable, the procedure makes {D} from □C, D → □(¬A ∨ □C), □B.

3 System KT+

Modal logic KT is defined by adding (T) rule to K. On decision procedure, it is defined by adding (T) rule including contraction to K+ system. However, we adopt a black marked (T) rule, because (T) rule including contraction has loop. If we mark to □ whenever we apply (T), it has no loop.

{A, Γ → Δ \atop □A, Γ → Δ} (T) {□A, A, Γ → Δ \atop □A, Γ → Δ} (T) {■A, A, Γ → Δ \atop □A, Γ → Δ} (T)

Figure 5: T rules for KT and KT+

Generaging a counter model for a unprovable sequent for KT+ is similar to K+. At first, the procedure reduces logical connectives ∧, ∨, ∧ and ⊃ to easier formulae, and transfers from □ formulae to ■ formulae by (T) rule. And then it determines that each consequence is an initial sequents or not. If no more rule is applied, it tries to apply following (□) rule. Finally each top sequent is a form like p_{1}, ⋯, p_{n}, ■Γ → q_{1}, ⋯, q_{n}. The sequent corresponds to the formulae set {p_{1}, ⋯, p_{n}}.

\begin{matrix}Γ → A_{1} & ⋯ & Γ → A_{m} \\ p_{1}, ⋯, p_{n}, ■Γ → □A_{1}, ⋯, □A_{m}, q_{1}, ⋯ q_{l} \end{matrix} (□)

Figure 6: □ rule for KT+

And (□) rule corresponds a frame \begin{matrix}{↷ \atop \{Γ, ¬A_{1}\}} & ⋯ & {↷ \atop \{Γ, ¬A_{m}\}} \\ ↖ ↷ ↗ \\ \{p_{1}, ⋯, p_{n}\} \end{matrix} .

Now, consider the formula □□B, C → □(¬A∨□C). The theorem prover KT+ outputs a decision tree and a counter model as follows:

\begin{matrix}\begin{matrix}{B → C \atop ■B, B, B, A → □C} & (□) \\ □B, B, A → □C \end{matrix} ; (T) ; □B, B → ¬A, □C ; (¬R) ; □B, B → ¬A ∨ □C ; (∨R) ; ■□B, ■B, B, C → □(¬A ∨ □C) & (□) \\ ■□B, □B, C → □(¬A ∨ □C) \end{matrix} ; (T) ; □□B, C → □(¬A ∨ □C) ; (T) \{B\} ; ⋮ . ; \{B, B, A\} ; ⋮ . ; \{B, C\}

Figure 7: Decision tree and counter model by KT+

Similarly to K+, we can find correspondence between decision trees and formula sets as follows:

\begin{matrix}B → C & ⋯ \{B\} \\ \begin{matrix}{■B, B, B, A → □C \atop □B, B, A → □C} & (T) \\ □B, B → ¬A, □C \end{matrix} ; (¬R) ; □B, B → ¬A ∨ □C ; (∨R) & ⋯ \{B, B, A\} \\ \begin{matrix}{■□B, ■B, B, C → □(¬A ∨ □C) \atop ■□B, □B, C → □(¬A ∨ □C)} & (T) \\ □□B, C → □(¬A ∨ □C) \end{matrix} ; (T) & ⋯ \{C, B\} \end{matrix}

Figure 8: Relationship between tree and set

4 Conclusion

Most of theorem provers in the world reply only whether a formula is valid or not. However, I want a proof if it is provable, and a counter model if it is unprovable. And it is hard to learn how to use a theorem prover. So I take TEX style as user interface. Because most of logicians know TEX, it is easy to learn how to use xpe. Especially, as they usually use xpe to draw proof figure, they will become familiar to xpe. My primary motivation to create xpe is the easy use.

References

[1] E Kiriyama, Ono H: The contraction rule and decision problems for logics without substractural rules, Studia Logica 50 (1991), 299–319.

[2] Chris D.Peterson: Athena Widget Set – C Language Interface MIT X Consortium.

[3] Lincoln A. Wallen: Automated Proof Search in Non-Classical Logics, : Efficient Matrix Proof Methods for Modal and Intuitionistic Logics MIT Press, 1990.

[4] H Wang:: A survey of mathematical logic Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1963.