A sequent calculus for logic of knowledge and past time: Completeness and decidability

We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving. The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this logic with other semantical constraints as well. Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006.     

Dual‐Context Sequent Calculus and Strict Implication

We introduce a dual‐context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut‐elimination theorem for this calculus is proved by a variant of Gentzen's method.     

On a logic of involutive quantales

The logic just corresponding to (non‐commutative) involutive quantales, which was introduced by Wendy MacCaull, is reconsidered in order to obtain a cut‐free sequent calculus formulation, and the completeness theorem (with respect to the involutive quantale model ) for this logic is proved using a new admissible rule. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Weak Arithmetics and Kripke Models

In the first section of this paper we show that i Π₁ ≡ W⌝⌝lΠ₁ and that a Kripke model which decides bounded formulas forces iΠ₁ if and only if the union of the worlds in any (complete) path in it satisflies IΠ₁. In particular, the union of the worlds in any path of a Kripke model of HA models IΠ₁. In the second section of the paper, we show that for equivalence of forcing and satisfaction of Π_m‐formulas in a linear Kripke model deciding Δ₀‐formulas it is necessary and sufficient that the model be Σ_m‐elementary. This implies that if a linear Kripke model forces PEM_prenex, then it forces PEM. We also show that, for each n ≥ 1, iΦ_n does not prove ℋ︁(IΠ_n's are Burr's fragments of HA.     

A probabilistic extension of intuitionistic logic

We introduce a probabilistic extension of propositional intuitionistic logic. The logic allows making statements such as P_≥sα, with the intended meaning “the probability of truthfulness of α is at least s”. We describe the corresponding class of models, which are Kripke models with a naturally arising notion of probability, and give a sound and complete infinitary axiomatic system. We prove that the logic is decidable.     

A Modeltheoretic Solution to a Problem of Tarski

Let 1 < n < ω and β > n. We show that the class Nr_nCA_β of n‐dimensional neat reducts of β‐dimensional cylindric algebras is not closed under forming elementary subalgebras. This solves a long‐standing open problem of Tarski and his co‐authors Andréka, Henkin, Monk and Németi. The proof uses genuine model‐theoretic arguments.     

On neat embeddings of cylindric algebras

We show that certain properties of dimension complemented cylindric algebras, concerning neat embeddings, do not generalize much further. Let α ≥ ω. There are non‐isomorphic representable cylindric algebras of dimension α each of which is a generating subreduct of the same β dimensional cylindric algebra. We also show that there exists a representable cylindric algebra ?? of dimension α, such that ?? is a generating subreduct of ?? and ??′, both in CA_{α +ω} , however ?? and ??′ are not isomorphic. This settle questions raised by Henkin, Monk and Tarski (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Preservation theorems for Kripke models

There are several ways for defining the notion submodel for Kripke models of intuitionistic first‐order logic. In our approach a Kripke model A is a submodel of a Kripke model B if they have the same frame and for each two corresponding worlds A^α and B^α of them, A^α is a subset of B^α and forcing of atomic formulas with parameters in the smaller one, in A and B, are the same. In this case, B is called an extension of A. We characterize theories that are preserved under taking submodels and also those that are preserved under taking extensions as universal and existential theories, respectively. We also study the notion elementary submodel defined in the same style and give some results concerning this notion. In particular, we prove that the relation between each two corresponding worlds of finite Kripke models A ≤ B is elementary extension (in the classical sense) (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Sémantique de type Kripke d'un système logique basé sur un ensemble ordonné fini

In order to modelize the reasoning of intelligent agents represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems the use of a set of constants constitutes a fundamental tool. We have introduced in [8] a logic system called without this kind of constants but limited to the case that T is a finite poset. We have proved a completeness result for this system w.r.t. an algebraic semantics. We introduce in this paper a Kripke‐style semantics for a subsystem of for which there existes a deduction theorem. The set of “possible worldsr is enriched by a family of functions indexed by the elements of T and satisfying some conditions. We prove a completeness result for system with respect to this Kripke semantics and define a finite Kripke structure that characterizes the propositional fragment of logic . We introduce a reational semantics (found by E. Orlowska) which has the advantage to allow an interpretation of the propositionnal logic using only binary relations. We treat also the computational complexity of the satisfiability problem of the propositional fragment of logic .     

PSPACE complexity of modal logic <Emphasis Type="Italic">K D</Emphasis>45<Subscript>n</Subscript>

We study sequent calculus for multi-modal logic K D45_n and its complexity. We introduce a loop-check free sequent calculus. Loop-check is eliminated by using the marked modal operator □_i^•, which is used as an alternative to sequents with histories ([8], [3], [5]). All inference rules are invertible or semi-invertible. To get this, we use or branches beside common and branches. We prove the equivalence between known sequent calculus and our newly introduced efficient sequent calculus. We concentrate on the complexity analysis of the introduced sequent calculus for multi-modal logic K D45_n. We prove that the space complexity of the given calculus is polynomial (O(l ³)). We show the maximum height of the constructed derivation tree that leads to the reduction of the time and space complexity. We present a decision algorithm for multi-modal logic K D45_n and some nontrivial examples to improve the introduced loop-check free sequent calculus.     

Reflection of Long Game Formulas

We study game formulas the truth of which is determined by a semantical game of uncountable length. The main theme is the study of principles stating reflection of these formulas in various admissible sets. This investigation leads to two weak forms of strict-II¹₁ reflection (or ∑₁-compactness). We show that admissible sets such as H(ω₂) and L_ω2 which fail to have strict-II¹₁ reflection, may or may not, depending on set-theoretic hypotheses satisfy one or both of these weaker forms. Mathematics Subject Classification : 03C70, 03C75.     

Fragments of Martin's Maximum in generic extensions

We show that large fragments of MM, e. g. the tree property and stationary reflection, are preserved by strongly (ω₁ + 1)‐game‐closed forcings. PFA can be destroyed by a strongly (ω₁ + 1)‐game‐closed forcing but not by an ω₂‐closed. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A spatial modal logic with a location interpretation

A spatial modal logic (SML) is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space (or location) interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut‐elimination theorem for a modified subsystem of SML are also presented. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

On non‐compact logics in NEXT(KTB)

In this paper we construct a continuum of logics, extensions of the modal logic T₂ = KTB ⊕ □²p → □³p, which are non‐compact (relative to Kripke frames) and hence Kripke incomplete. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Independence results for weak systems of intuitionistic arithmetic

This paper proves some independence results for weak fragments of Heyting arithmetic by using Kripke models. We present a necessary condition for linear Kripke models of arithmetical theories which are closed under the negative translation and use it to show that the union of the worlds in any linear Kripke model of HA satisfies PA. We construct a two‐node PA‐normal Kripke structure which does not force iΣ₂. We prove i?₁ ? i?₁, i?₁ ? i?₁, iΠ₂ ? iΣ₂ and iΣ₂ ? iΠ₂. We use Smorynski's operation Σ′ to show HA ? lΠ₁.     

Sperner spaces and first‐order logic

We study the class of Sperner spaces, a generalized version of affine spaces, as defined in the language of pointline incidence and line parallelity. We show that, although the class of Sperner spaces is a pseudo‐elementary class, it is not elementary nor even ??_∞ω‐axiomatizable. We also axiomatize the first‐order theory of this class.     

Basic Propositional Calculus I

We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E₁, a theory axiomatized by T → ⊥. The intersection CPC ∩ E₁ is axiomatizable by the Principle of the Excluded Middle A V ∨ ?A. If B is a formula such that (T → B) → B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula (T → B) → B is derivable exactly when B is provably equivalent to a formula of the form ((T → A) → A) → (T → A).     

Deep sequent systems for modal logic

We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening and contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure.      

Eigenvalues and eigenvectors of banded Toeplitz matrices and the related symbols

It is known that for a tridiagonal Toeplitz matrix, having on the main diagonal the constant a₀ and on the two first off‐diagonals the constants a₁(lower) and a₋₁(upper), which are all complex values, there exist closed form formulas, giving the eigenvalues of the matrix and a set of associated eigenvectors. For example, for the 1D discrete Laplacian, this triple is (a₀,a₁,a₋₁)=(2,−1,−1). In the first part of this article, we consider a tridiagonal Toeplitz matrix of the same form (a₀,a_ω,a_−ω), but where the two off‐diagonals are positioned ω steps from the main diagonal instead of only one. We show that its eigenvalues and eigenvectors can also be identified in closed form and that interesting connections with the standard Toeplitz symbol are identified. Furthermore, as numerical evidences clearly suggest, it turns out that the eigenvalue behavior of a general banded symmetric Toeplitz matrix with real entries can be described qualitatively in terms of the symmetrically sparse tridiagonal case with real a₀, a_ω=a_−ω, ω=2,3,…, and also quantitatively in terms of those having monotone symbols. A discussion on the use of such results and on possible extensions complements the paper.     

The stationary set splitting game

The stationary set splitting game is a game of perfect information of length ω₁ between two players, unsplit and split, in which unsplit chooses stationarily many countable ordinals and split tries to continuously divide them into two stationary pieces. We show that it is possible in ZFC to force a winning strategy for either player, or for neither. This gives a new counterexample to Σ²₂ maximality with a predicate for the nonstationary ideal on ω₁, and an example of a consistently undetermined game of length ω₁ with payoff de.nable in the second‐order monadic logic of order. We also show that the determinacy of the game is consistent with Martin's Axiom but not Martin's Maximum. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)