We specialise Aronszajn trees by an ωω-bounding forcing that adds reals. We work with creature forcings on uncountable spaces.

As an application of these notions of forcing, we answer a question of Moore, Hrušák and Džamonja whether implies the existence of a Souslin tree in a negative way by showing that “ and every Aronszajn tree is special” is consistent relative to ZFC.

It is generally known that infinite symmetric groups have few nontrivial normal subgroups (typically only the subgroups of bounded support) and none of small index. (We will explain later exactly what we mean by small). However the standard analysis relies heavily on the axiom of choice. By dint of a lot of combinatorics we have been able to dispense—largely—with the axiom of choice. Largely, but not entirely: our result is that if X is an infinite set with ∣X∣ = ∣X × X∣ then Symm(X) has no nontrivial normal subgroups of small index. Some condition like this is needed because of the work of Sam Tarzi who showed [4] that, for any finite group G, there is a model of ZF without AC in which there is a set X with Symm(X)/FSymm(X) isomorphic to G.

The proof proceeds in two stages. We consider a particularly useful class of permutations, which we call the class of flexible permutations. A permutation of X is flexible if it fixes at least ∣X∣-many points. First we show that every normal subgroup of Symm(X) (of small index) must contain every flexible permutation. This will be theorem 4. Then we show (theorem 7) that the flexible permutations generate Symm(X).

We show that if ℱ is any “well-behaved” subset of the Borel functions and we assume the Axiom of Determinacy then the hierarchy of degrees on (ωω) induced by ℱ turns out to look like the Wadge hierarchy (which is the special case where ℱ is the set of continuous functions).

We interpret the basic notions of topological dynamics in the model-theoretic setting, relating them to generic types of definable group actions and their generalizations.

For f, g ∈ ωω let be the minimal number of uniform g-splitting trees (or: Slaloms) to cover the uniform f-splitting tree, i.e., for every branch v of the f-tree, one of the g-trees contains v. is the dual notion: For every branch v, one of the g-trees guesses v(m) infinitely often.

It is consistent that for ℵ1 many pairwise different cardinals κ∊ and suitable pairs (f∊, g∊).

For the proof we use creatures with sufficient bigness and halving. We show that the lim-inf creature forcing satisfies fusion and pure decision. We introduce decisiveness and use it to construct a variant of the countable support iteration of such forcings, which still satisfies fusion and pure decision.

§1. Introduction. A logic ℒ has a limit law, if the asymptotic probability of every query definable in ℒ converges. It has a 0–1-law if the probability converges to 0 or 1. The 0–1-law for first-order logic on relational vocabularies was independently found by Glebski et al. [6] and Fagin [5]. Later it has been shown for many other logics, for instance for fragments of second order logic [12], for finite variable logic [13] and for FO extended with the rigidity quantifier [3]. Lynch [14] has shown a limit law for first-order logic on vocabularies with unary functions.

We say that two formulas or two logics are almost everywhere equivalent, if they are equivalent on a class of structures whose asymptotic probability measure is one [7]. A 0–1-law is usually proved by showing that every quantifier of the logic has almost everywhere quantifier elimination, i.e., every formula with just one quantifier in front of it is almost everywhere equivalent to a quantifier-free formula. Besides proving 0–1-law, this implies that the logic is (weakly) almost everywhere equivalent to first-order logic.

The aim of this paper is to study, whether a logic with a 0–1-law can have greater expressive power than FO in the almost everywhere sense and to what extent. In particular, we are interested on the definability of linear order. Because a 0–1-law determines the almost everywhere expressive power of the sentences of the logic completely, but does not say anything about formulas explicitly, we have to assume some regularity on logics. We will therefore mostly consider extensions of first-order logic with generalized quantifiers.

We obtain a large class of significant examples of n-random reals (i.e., Martin-Löf random in oracle ∅(n−1)) à la Chaitin. Any such real is defined as the probability that a universal monotone Turing machine performing possibly infinite computations on infinite (resp. finite large enough, resp. finite self-delimited) inputs produces an output in a given set . In particular, we develop methods to transfer many-one completeness results of index sets to n-randomness of associated probabilities.

We examine second order intuitionistic propositional logic, IPC2. Let ℱ∃ a be the set of formulas with no universal quantification. We prove Glivenko's theorem for formulas in ℱ∃ that is, for φ ∈ ℱ∃, φ is a classical tautology if and only if ┐┐φ is a tautology of IPC2. We show that for each sentence φ ∈ ℱ∃ (without free variables), φ is a classical tautology if and only if φ is an intuitionistic tautology. As a corollary we obtain a semantic argument that the quantifier ∀ is not definable in IPC2 from ⊥, ⋁, ⋀, →, ∃.

This work deals with the expressive power of logics on finite graphs with access to an additional “arbitrary” linear order. The queries that can be expressed this way are the order-invariant queries for the logic. For the standard logics used in computer science, such as first-order logic, it is known that access to an arbitrary linear order increases the expressiveness of the logic. However, when we look at the separating examples, we find that they have satisfying models whose Gaifman Graph is complex – unbounded in valence and in treewidth. We thus explore the expressiveness of order-invariant queries over well-behaved graphs. We prove that first-order order-invariant queries over strings and trees have no additional expressiveness over first-order logic in the original signature. We also prove new upper bounds on order-invariant queries over bounded treewidth and bounded valence graphs. Our results make use of a new technique of independent interest: the application of algebraic characterizations of definability to show collapse results.

We show that if I is a precipitous ideal on ω1 and if θ > ω1 is a regular cardinal, then there is a forcing ℙ = ℙ(I, θ) which preserves the stationarity of all I-positive sets such that in Vℙ, ⟨Hθ; ∈, I⟩ is a generic iterate of a countable structure ⟨M; ∈, Ī⟩. This shows that if the nonstationary ideal on ω1 is precipitous and exists, then there is a stationary set preserving forcing which increases . Moreover, if Bounded Martin's Maximum holds and the nonstationary ideal on ω1 is precipitous, then .

We examine the reverse mathematics and computability theory of a form of Ramsey's theorem in which the linear n-tuples of a binary tree are colored.

We develop the theory of generically stable types, independence relation based on nonforking and stable weight in the context of dependent theories.

In this paper it is shown that the global statement that the dominating number for κ is less than 2κ for all regular κ, is internally consistent, given the existence of 0#. The possible range of values for the dominating number for κ and 2κ which may be simultaneously true in an inner model is also explored.

Relations between some theories of semigroups (also known as theories of strings or theories of concatenation) and arithmetic are surveyed. In particular Robinson's arithmetic Q is shown to be mutually interpretable with TC, a weak theory of concatenation introduced by Grzegorczyk. Furthermore, TC is shown to be interpretable in the theory F studied by Tarski and Szmielewa, thus confirming their claim that F is essentially undecidable.

We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2ΕΧΡΤΙΜΕ, thus 2ΕΧΡΤΙΜΕ-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2ΕΧΡΤΙΜΕ-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2ΕΧΡΤΙΜΕ. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines.

We show that either of the following hypotheses imply that there is an inner model with a proper class of strong cardinals and a proper class of Woodin cardinals. 1) There is a countably closed cardinal κ ≥ ℵ such that □κ and □(κ) fail. 2) There is a cardinal κ such that κ is weakly compact in the generic extension by Col(κ, κ+). Of special interest is 1) with κ = ℵ3 since it follows from PFA by theorems of Todorcevic and Velickovic. Our main new technical result, which is due to the first author, is a weak covering theorem for the model obtained by stacking mice over Kc∥κ.

We study the following open question in computable model theory: does there exist a structure of computable dimension two which is the prime model of its first-order theory? We construct an example of such a structure by coding a certain family of c.e. sets with exactly two one-to-one computable enumerations into a directed graph. We also show that there are examples of such structures in the classes of undirected graphs, partial orders, lattices, and integral domains.

We consider two axioms of second-order arithmetic. These axioms assert, in two different ways, that infinite but narrow binary trees always have infinite paths. We show that both axioms are strictly weaker than Weak König's Lemma, and incomparable in strength to the dual statement (WWKL) that wide binary trees have paths.