Definition:Divide (Model Theory)

This page has been identified as a candidate for refactoring of advanced complexity. In particular: Extract notes and examples into their own pages. Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Definition

Let $T$ be a complete $\LL$-theory.

Let $\mathfrak C$ be a monster model for $T$.

Let $A$ be a subset of the universe of $\mathfrak C$.

Let $\map \phi {\bar x, \bar b}$ be an $\LL$-formula with free variables $\bar x$ and parameters $\bar b$ from the universe of $\mathfrak C$.

Let $\map {\operatorname{tp} } {\bar b / A}$ denote the type of $\bar b$ over $A$.

Then $\map \phi {\bar x, \bar b}$ $k$-divides in $\mathfrak C$ over $A$ if and only if:

there exists a sequence $\sequence {\bar b_i}_{i \mathop \in \N}$ such that $\map {\operatorname{tp} } {\bar b_i / A} = \map {\operatorname{tp} } {\bar b / A}$ for each $i \in \N$

and:

for any distinct $k$-many terms $\bar b_{i_1}, \ldots, \bar b_{i_k}$ of the sequence, the set $\set {\map \phi {\bar x, \bar b_{i_1} }, \ldots, \map \phi {\bar x, \bar b_{i_k} } }$ is not satisfiable in $\mathfrak C$.

Let $\map \pi {\bar x, \bar b}$ be a set of formulas with parameters $\bar b$.

$\map \pi {\bar x, \bar b}$ $k$-divides over $A$ if it implies a formula $\map \phi {x, \bar c}$ which $k$-divides over $A$.

Formulas and sets of formulas are said to divide if they $k$-divide for some $k$.

Note

To help understand the definition, consider the following informal discussion.

We can think of $\map \phi {x, y}$ as a description of $x$ in terms of $y$.

If $b$ and $b'$ have the same type over $A$, then as far as $A$ can tell, $b$ and $b'$ are the same thing, in the sense that they both satisfy the same formulas with parameters from $A$.

So $\map \phi {x, b}$ $k$-dividing over $A$ means that we can find an infinite sequence of parameters $b_i$ that $A$ can't tell apart, but nevertheless, no $x$ can satisfy any $k$ of the descriptions $\map \phi {x, b_i}$ at the same time.

Example

Consider the language $\LL = \set \sim$ with one binary relation symbol $\sim$.

Let $\MM = \struct {\R^2, P}$ be the $\LL$-structure where $P$ is the equivalence relation defined by $\tuple {x_1, y_1} \mathrel P \tuple {x_2, y_2}$ if and only if $x_1 = x_2$.

That is, $P$ identifies points in the plane which project vertically to the same value on the $x$-axis.

Let $\mathfrak C$ be some monster model for $\MM$.

The formula $x \sim \tuple {0, 0}$ $2$-divides over $\O$, which can be seen by considering the sequence $\tuple {\tuple {0, 0}, \tuple {1, 0}, \tuple {2, 0}, \tuple {3, 0}, \ldots}$.

The language is not very complicated; every $\tuple {n, m}$ has the same type over $\O$, so in particular each term in this sequence has the same type as $\tuple {0, 0}$.

However, $x \sim \tuple {n, 0}$ and $x \sim \tuple {m, 0}$ cannot be simultaneously satisfied for $n \ne m$, since this would imply $\tuple {n, 0} \mathrel P \tuple {m, 0}$, which is impossible.

The formula $x \sim \tuple {0, 0}$ does not $k$-divide over $A = \set {\tuple {0, y}: y \in \R}$ for any $k$ however, since only points of the form $\tuple {0, y}$ are of the same type as $\tuple {0, 0}$ over $A$.

This article needs to be linked to other articles. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

There are no source works cited for this page. Source citations are highly desirable, and mandatory for all definition pages. Definition pages whose content is wholly or partly unsourced are in danger of having such content deleted. To discuss this page in more detail, feel free to use the talk page.