On topological modal logic of real line with difference modality
by
Andrey Kudinov
Moscow State University

We consider proposition modal logics in the language ML(^[¯], [ ≠ ]) with two modal operators ^[¯] and [ ≠ ].

Definition A topological model over a topological space X is a pair M=(X, q), where q is a function from the set of proposition variables to the set of all subsets of X. The truth value of a formula is defined as usual by induction, in particular

M, x\models [¯] A ⇔ ∃U(x) ∀y ∈ U(x) (M, y\models A), M, x\models [ ≠ ] A ⇔ ∀y ( x ≠ y ⇒ M, y\models A),

where U(x) is a neighbourhood of x. A formula is called valid in X iff it is true at all points in all models of X.

Definition The logic of a topological space X is the set of all valid formulas in X. It is denoted by L_{^[¯], [ ≠ ]}(X).

The logics L_{^[¯], [ ≠ ]}(C) (where C is Cantor space) and L_{^[¯], [ ≠ ]}(Rⁿ), n ≥ 2 are known from [2]. They are finitely axiomatizable and decidable.

Theorem L_{^[¯], [ ≠ ]}(R) is not axiomatizable in finitely many propositional variables, hence it is not finitely axiomatizable.

The decidability of L_{^[¯], [ ≠ ]}(R) follows from the decidability of the monadic second order theory of (R, ≤ ) proved by M. O. Rabin [1].

[1] M.O.Rabin Decidability of second order theories and automata on infinite trees. Transactions of American Mathematical Society, v.141, 1969, 1-35.

[2] A. Kudinov Topological Modal Logics with Difference Modality. Advances in Modal Logic, v.6, College Publications, London 2006, 319-332.

PDF

Date received: April 29, 2007