ABSTRACT. In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words.

ABSTRACT. Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(E); in 2TC, the TC operator binds only tuples of relation variables. We establish that, with respect to expressive power, SO(2TC)(E) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO.

ABSTRACT. Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions.

In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.

ABSTRACT. Buchholz' Omega-rule is a way to give a syntactic, possibly ordinal-free proof of cut elimination for various impredicative systems of logic and arithmetic. Our goal is to understand it from an algebraic perspective. Among many proofs of cut elimination for higher order logics, Maehara and Okada's algebraic proofs are of particular interest. The algebraic essense of their arguments can be described as the (Dedekind-)MacNeille completion. Interestingly, it turns out that the Omega-rule finds its algebraic foundation in the MacNeille completion. This observation leads to an algebraic form of the Omega-rule that we call the Omega-valuation. Combining the two, we obtain an algebraic proof of cut elimination for the parameter-free fragment of second order intuitionistic logic, which does not rely on reducibility candidates and is formalizable in theories of finitely iterated inductive definitions.