We try to understand complete types over a somewhat saturated model of a complete first order theory which is dependent (previously called NIP), by "decomposition theorems for such types". Our thesis is that the picture of dependent theory is the combination of the one for stable theories and the one for the theory of dense linear order or trees (and first we should try to understand the quite saturated case). As a measure of our progress, we give several applications considering some test questions; in particular we try to prove the generic pair conjecture and do it for measurable cardinals.
The paper proves a conjecture of Solomon Feferman concerning the indefiniteness of the continuum hypothesis relative to a semi-intuitionistic set theory.
We conjecture that for a strongly minimal theory T in a finite signature satisfying the Zilber Trichotomy, there are only three possibilities for the recursive spectrum of T: all countable models of T are recursively presentable; none of them are recursively presentable; or only the zero-dimensional model of T is recursively presentable. We prove this conjecture for disintegrated (formerly, trivial) theories and for modular groups. The conjecture also holds via known results for fields. The conjecture remains open for finite covers of groups and fields.
A complete first order theory of a relational signature is called monomorphic iff all its models are monomorphic (i.e. have all the $n$-element substructures isomorphic, for each positive integer $n$). We show that a complete theory ${\mathcal T}$ having infinite models is monomorphic iff it has a countable monomorphic model and confirm the Vaught conjecture for monomorphic theories. More precisely, we prove that if ${\mathcal T}$ is a complete monomorphic theory having infinite models, then the number of its non-isomorphic countable models, $I({\mathcal T},ω)$, is either equal to $1$ or to ${…
We develop the theory of generically stable types, independence relation based on nonforking and stable weight in the context of dependent (NIP) theories.
Let $T$ be a (first order complete) dependent theory, ${\mathfrak{C}}$ a $\barκ$-saturated model of $T$ and $G$ a definable subgroup which is abelian. Among subgroups of bounded index which are the union of $<\barκ$ type definable subsets there is a minimal one, i.e. their intersection has bounded index. In fact, the bound is $\leq 2^{|T|}$. We then deal with 2-dependent theories, a wider class of first order theories.
For a dependent theory T, in C_T for every type definable group G, the intersection of type definable subgroups with bounded index is a type definable subgroup with bounded index.
We further investigate the class of models of a strongly dependent (first order complete) theory T, continuing math.LO/0406440. If |A|+|T|<= mu, I subseteq C, |I| >=beth_{|T|^+}(mu) then some J subseteq I of cardinality mu^+ is an indiscernible sequence over A .
This paper generalizes Shelah's generic pair conjecture (now theorem) for the measurable cardinal case from first order theories to finite diagrams. We use homogeneous models in the place of saturated models.
Reinhardt's conjecture, a formalization of the statement that a truthful knowing machine can know its own truthfulness and mechanicalness, was proved by Carlson using sophisticated structural results about the ordinals and transfinite induction just beyond the first epsilon number. We prove a weaker version of the conjecture, by elementary methods and transfinite induction up to a smaller ordinal.
A structure ${\mathbb Y}$ of a relational language $L$ is called almost chainable iff there are a finite set $F \subset Y$ and a linear order $<$ on the set $Y\setminus F$ such that for each partial automorphism $φ$ (i.e., local automorphism, in Fra\"ıssé's terminology) of the linear order $\langle Y\setminus F, < \rangle$ the mapping ${\mathrm{id}} _F \cup φ$ is a partial automorphism of ${\mathbb Y}$. By a theorem of Fra\"ıssé, if $|L|<ω$, then ${\mathbb Y}$ is almost chainable iff the profile of ${\mathbb Y}$ is bounded; namely, iff there is a positive integer $m$ such that ${\mathbb Y}$ ha…
We characterize nonforking (Morley) sequences in dependent theories in terms of a generalization of Poizat's special sequences and show that average types of Morley sequences are stationary over their domains. We characterize generically stable types in terms of the structure of the "eventual" type. We then study basic properties of "strict Morley sequences", based on Shelah's notion of strict nonforking. In particular we prove "Kim's lemma" for such sequences, and a weak version of local character.
We give necessary and sufficient geometric conditions for a theory definable in an o-minimal structure to interpret a real closed field. The proof goes through an analysis of thorn-minimal types in super-rosy dependent theories of finite rank. We prove that such theories are coordinatised by thorn-minimal types and that such a type is unstable if an only if every non-algebraic extension thereof is. We conclude that a type is stable if and only if it admits a coordinatisation in thorn-minimal stable types. We also show that non-trivial thorn-minimal stable types extend stable sets.
In this short note we show that if we add predicate for a dense complete indiscernible sequence in a dependent theory then the result is still dependent. This answers a question of Baldwin and Benedikt and implies that every unstable dependent theory has a dependent expansion interpreting linear order.
There is much more known about the family of superstable theories when compared to stable theories. This calls for a search of an analogous "super-dependent" characterization in the context of dependent theories. This problem has been treated in \cite{Sh:783,Sh:863}, where the candidates "Strongly dependent", "Strongly dependent^2" and others were considered. These families generated new families when we are considering intersections with the stable family. Here, continuing \cite[§2, §5E,F,G]{Sh:863}, we deal with several candidates, defined using dividing properties and related ranks of types…
A dependent theory is a (first order complete theory) T which does not have the independence property. A main result here is: if we expand a model of T by the traces on it of sets definable in a bigger model then we preserve its being dependent. Another one justifies the cofinality restriction in the theorem (from a previous work) saying that pairwise perpendicular indiscernible sequences, can have arbitrary dual-cofinalities in some models containing them.
In the first part we show a counterexample to a conjecture by Shelah regarding the existence of indiscernible sequences in dependent theories (up to the first inaccessible cardinal). In the second part we discuss generic pairs, and give an example where the pair is not dependent. Then we define the notion of directionality which deals with counting the number of coheirs of a type and we give examples of the different possibilities. Then we discuss non-splintering, an interesting notion that appears in the work of Rami Grossberg, Andrés Villaveces and Monica VanDieren, and we show that it is no…
We study semantic and syntactic properties of spherical orders and their elementary theories, including finite and dense orders and their theories. It is shown that theories of dense $n$-spherical orders are countably categorical and decidable. The values for spectra of countable models of unary expansions of $n$-spherical theories are described. The Vaught conjecture is confirmed for countable constant expansions of dense $n$-spherical theories.
In this paper, we propose an abstract definition of dependent type theories as essentially algebraic theories. One of the main advantages of this definition is its composability: simple theories can be combined into more complex ones, and different properties of the resulting theory may be deduced from properties of the basic ones. We define a category of algebraic dependent type theories which allows us not only to combine theories but also to consider equivalences between them. We also study models of such theories and show that one can think of them as contextual categories with additional …
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive reading of syntax, yielding the traditional presentations of specific theories as closely as possible. Specifically, we give three main definitions: raw type theories, a minimal setup for discussing depe…
We define a notion of equivalence between algebraic dependent type theories which we call Morita equivalence. This notion has a simple syntactic description and an equivalent description in terms of models of the theories. The category of models of a type theory often carries a natural structure of a model category. If this holds for the categories of models of two theories, then a map between them is a Morita equivalence if and only if the adjunction generated by it is a Quillen equivalence.
We study the coherence and conservativity of extensions of dependent type theories by additional strict equalities. By considering notions of congruences and quotients of models of type theory, we reconstruct Hofmann's proof of the conservativity of Extensional Type Theory over Intensional Type Theory. We generalize these methods to type theories without the Uniqueness of Identity Proofs principle, such as variants of Homotopy Type Theory, by introducing a notion of higher congruence over models of type theory. Our definition of higher congruence is inspired by Brunerie's type-theoretic defini…
For an infinite cardinal $κ$, let $dedκ$ denote the supremum of the number of Dedekind cuts in linear orders of size $κ$. It is known that $κ<dedκ\leq 2^κ$ for all $κ$ and that $dedκ<2^κ$ is consistent for any $κ$ of uncountable cofinality. We prove however that $2^κ\leq ded ( ded ( ded ( dedκ)))$ always holds. Using this result we calculate the Hanf numbers for the existence of two-cardinal models with arbitrarily large gaps and for the existence of arbitrarily large models omitting a type in the class of countable dependent first-order theories. Specifically, we show that these bounds are as…
We survey the history of Shelah's conjecture on strongly dependent fields, give an equivalent formulation in terms of a classification of strongly dependent fields and prove that the conjecture implies that every strongly dependent field has finite dp-rank.
Can a problem undecidable with classical resources be decidable with quantum ones? The answer expected is no; as both being Turing theories, they should not solve the Halting problem - a problem unsolvable by any Turing machine. Yet, we provide an affirmative answer to the aforesaid question. We come up with a novel logical structure to formulate infinitely many such problems for any pair of distinct Turing theories, including but not limited to the classical and quantum theories. Importantly, a class of other decision problems, such as the Halting one, remains unsolvable in all those theories…
