We develop game-theoretic semantics (GTS) for the fragment ATL+ of the full Alternating-time Temporal Logic ATL*, essentially extending a recently introduced GTS for ATL. We first show that the new game-theoretic semantics is equivalent to the standard semantics of ATL+ (based on perfect recall strategies). We then provide an analysis, based on the new semantics, of the memory and time resources needed for model checking ATL+. Based on that, we establish that strategies that use only a very limited amount of memory suffice for ATL+. Furthermore, using the GTS we provide a new algorithm for model checking of ATL+ and identify a natural hierarchy of tractable fragments of ATL+ that extend ATL.

In unpublished notes, Pila discussed some theory surrounding the modular function $j$ and its derivatives. A focal point of these notes was the statement of two conjectures regarding $j$, $j'$ and $j''$: a Zilber-Pink type statement incorporating $j$, $j'$ and $j''$, which was an extension of an apparently weaker conjecture of Andre-Oort type. In this paper, I cover some background regarding $j$, $j'$ and $j''$ - mostly covering the work already done by Pila - and then prove Pila's "Modular Andre-Oort with Derivatives" conjecture. The proof uses ideas of o-minimality, adapting the usual Pila-Zannier strategy for diophantine problems of this type.

Feb 28 2017

math.LO arXiv:1702.08352v1

The variety of Brouwerian semilattices is amalgamable and locally finite, hence by well-known results due to W. H. Wheeler, it has a model completion (whose models are the existentially closed structures). In this paper, we supply for such a model completion a finite and rather simple axiomatization.

Feb 28 2017

math.LO arXiv:1702.08350v1

We prove various extensions of the Tennenbaum phenomenon to the case of computable quotient presentations of models of arithmetic and set theory. Specifically, no nonstandard model of arithmetic has a computable quotient presentation by a c.e. equivalence relation. No $\Sigma_1$-sound nonstandard model of arithmetic has a computable quotient presentation by a co-c.e. equivalence relation. No nonstandard model of arithmetic in the language $\{+,\cdot,\leq\}$ has a computably enumerable quotient presentation by any equivalence relation of any complexity. No model of ZFC or even much weaker set theories has a computable quotient presentation by any equivalence relation of any complexity. And similarly no nonstandard model of finite set theory has a computable quotient presentation.

Feb 28 2017

math.LO arXiv:1702.08281v1

We study abstract elementary classes (AECs) that, in $\aleph_0$, have amalgamation, joint embedding, no maximal models and are stable (in terms of the number of orbital types). We prove that such classes exhibit superstable-like behavior at $\aleph_0$. More precisely, there is a superlimit model of cardinality $\aleph_0$ and the class generated by this superlimit has a type-full good $\aleph_0$-frame (a local notion of nonforking independence) and a superlimit model of cardinality $\aleph_1$. This extends the first author's earlier study of $\operatorname{PC}_{\aleph_0}$-representable AECs and also improves results of Hyttinen-Kesälä and Baldwin-Kueker-VanDieren.

In this work we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics. By proposing local versions to ordinary sequent rules we obtain linear nested sequent calculi for a number of logics, including to our knowledge the first nested sequent calculi for a large class of simply dependent multimodal logics, and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities, which makes them amenable to specification as linear logic clauses. While this granulation of the sequent rules introduces more choices for proof search, we show how linear nested sequent calculi can be restricted to blocked derivations, which directly correspond to ordinary sequent derivations.

The role of finite centralizers of involutions in pseudo-finite groups is analyzed. Using basic techniques from infinite group theory, it is shown that a pseudo-finite group admitting a definable involutory automorphism fixing only finitely many elements is finite-by-abelian-by-finite. As a consequence, an alternative proof of the corresponding result for periodic groups due to Hartley and Meixner is given, as well as a gently improvement regarding definable properties. Furthermore, it is shown that any pseudo-finite group has an infinite abelian subgroup, and that in any pseudo-finite group in which the centralizer of any element is finite or has finite index, the FC-center is a finite index definable subgroup.

Feb 28 2017

math.LO arXiv:1702.07947v1

We answer several questions posed by Hamkins and Leahy concerning the implicitly constructible universe, Imp. Specifically, we show that it is relatively consistent with ZFC that Imp satisfies the negation of CH, that Imp is not HOD, and that Imp satisfies V $\neq$ Imp, or in other words, that $(Imp)^{Imp}\neq Imp$.

We prove a Structure Identity Principle for theories defined on types of $h$-level 3 by defining a general notion of saturation for a large class of structures definable in the Univalent Foundations.