ファイル置き場 Sendai Logic Homepage 100625ambo

A note on lowness in the category of existentially closed

models

安保 勇希

筑波大学

2010^年6^月25^日

[P] A. Pillay, Forking in the category of existentially closed structures. Connections between model theory and algebraic and analytic geometry, 23–42, Quad. Mat., 6, Dept. Math., Seconda Univ. Napoli, Caserta, 2000.

”Simplicity theory in non-elementary classes”

Let T be a universal theory. Definition

M |= T is an existentially closed model (e.c.m.) for T

⇐⇒

∀φ(x) : existentiall formula, ∀a ∈ M,

∃N s.t. N |= T , N ⊃ M, N |= φ(a) =⇒ M |= φ(a)

”complete theory T ^のmodel ^全体” ^ではなく”universal theory T ^の existentially closed model ^全体”^{を対象とする}

Example

EC(T) = {M : e.c.m. for T }.

1 _T = the theory of fields,

M is e.c.m. for T ⇔ M is an algebraically closed field EC(T) is an elementary class

2 _T = the theory of linear orders,

M is e.c.m. for T ⇔ M is a dense linear order without endpoints EC(T) is an elementary class

3 _T = the theory of rings, (cf. Hodges, Model Theory) M is e.c.m. for T ⇒ ”x is nilpotent” is definable EC(T) is Non-elementary class

歴史 ₍ どんどん一般化されてます ₎

1970^年代から, A. Robinson ^らが non-elementary class ^での model theory ^を始めた

1976^年, Shelah ^がnon-elementary class^での stability theory ^を, type の数を数えるという方針で行った

同時に_{, Shelah} はそのようなクラスで_{, forking} の理論を展開できる

か？という問題を提示した

1998^年, Hrushovski ^がRobinson theory ^を定義し,^そこで simple theory ^を展開

2000^年, Pillay ^が一般のuniversal theory ^でforking/dividing^の理論 を展開

2002^年以降, Ben-Yaacov^{が更に一般的な} positive Robinson theory を定義し_,そこで _dividingの理論を展開

Definition

M is κ-existentially universal domain (e.u.domain)

⇐⇒

Σ(x) : partial existential type over A (|A| < κ) which is finitely satisfiable in M ⇒ Σ is satisfiable in M, and

A, B ⊂ M where |A|, |B| < κ, f : A → B : a bijection such that etp(a) ⊂ etp(f (a)) for all tuples a from A ⇒ f extends to an automorphism of M.

We consider

(complete) universal theory T instead of complete theory T e.c.m. for T instead of models of T

κ-e.u.domain for T instesd of κ-saturated model of T

”complete universal theory” means that T = Th_∀(M) for some M κ-e.u.domain for T means that T = Th_∀(M).

We consider

(complete) universal theory T instead of complete theory T e.c.m. for T instead of models of T

κ-e.u.domain for T instesd of κ-saturated model of T

”complete universal theory” means that T = Th_∀(M) for some M κ-e.u.domain for T means that T = Th_∀(M).

Notation:

M : κ-e.u.domain, T = Th∀(M), M, N, . . . : e.c.m. for T , a, b, . . . : finite tuples in M, A, B, . . . : small subsets of M

Problem 1 [P] For M : e.u.domain,

Local character of forking = Local character of dividing ? Problem 2 [P]

For M : simplee.u.domain, A ⊂ M,

Is ”Lstp(x/A) = Lstp(y /A)” definable by an existential type over A? Problem 3

For M : lowe.u.domain, A ⊂ M, a ∈ M, Lstp(a/A) = stp(a/A)?

答えパターン１ (Hrushovski’s Robinson theories) Fact (A partial answer to Problem 1)

For Hrushovski’s Robinson theories, YES, that is, Local character of forking = Local character of dividing. Fact (A partial answer to Problem 2)

For simpleHrushovski’s Robinson theories, YES, that is,

”Lstp(x/A) = Lstp(y /A)” is definable by an existential type over A. A partial answer to Problem 3

For lowHrushovski’s Robinson theories, YES, that is, Lstp(a/A) = stp(a/A)

これらは比較的簡単にできる

答えパターン２ (Pillay’s condition)

d(a, b/A) ≤ 1 ⇔ ∃I : existentially indiscernible sequence over A s.t. a, b ∈ I .

定義 (Ben-Yaacov)

”d(x, y /A) ≤ 1” ^がexistential type over A ^によってtype-definable ^のと き_{, M}は_thickであるという

Another partial answer to Problem 2 (Ben-Yaacov) for M : thicksimplee.u.domain, A ⊂ M,

”Lstp(x/A) = Lstp(y /A)” is definable by an existential type over A. Another partial answer to Problem 3 (Main Theorem)

for M : thicklowe.u.domain, A ⊂ M, a ∈ M, Lstp(a/A) = stp(a/A)

Definition [P]

Σ(x, B) : existential type over B

1 Σ(x, B) divides over A

⇐⇒ ∃(Bi : i < ω) : existentially indiscernible sequence over A with B₀ = B s.t. ^∪

i <ω

Σ(x, B_i) is not realized in M

2 Σ(x) forks over A

⇐⇒ ∃Ψ : a small set of dividing (/A) existential formulas (with parameters) s.t. M |= Σ →^∨Ψ

Definition [P]

Σ(x, B) : existential type over B

1 Σ(x, B) divides over A

⇐⇒ ∃(Bi : i < ω) : existentially indiscernible sequence over A with B₀ = B s.t. ^∪

i <ω

Σ(x, B_i) is not realized in M

2 Σ(x) forks over A

⇐⇒ ∃Ψ : a small set of dividing (/A) existential formulas (with parameters) s.t. M |= Σ →^∨Ψ

Remark [P]

Σ(x) divides over A ⇐⇒ Σ ⊢ ∃φ(x) s.t. φ(x) divides over A.

Does ”Σ forks over A” imply ∃ψ₁, . . . , ψ_n : dinviding (/A) existential formulas Σ ⊢ ∃θ s.t. M |= θ →

∨n i=1

ψ_i ?

Definition [P]

M is simple ⇔ for all a ∈ M, A ⊂ M, there exists B ⊂ A with

|B| ≤ |T | + ℵ0 s. t. etp(a/A) does not fork over B fact (M is simple) [P]

dividing over A = forking over A

Problem 1 [P] For M : e.u.domain,

Local character of forking = Local character of dividing ?

for elementary classes forking satisfies

local character

dividing satisfies local character

trivial

forking (dividing) satisfies symmetry

forking (dividing) satisfies transitivity

dividing ⇔

∀ Morley seq. ^でdivide

∀Σ, φ, k, well-known

well known

well known

D(Σ, φ, k) < ∞

Kim

difference from elementary classes

We can use compactness only for existential types. We can not prove the following directly:

∀n < ω, ∃ tree of height n =⇒ ∀κ ∃ tree of height κ

φ(x, a0) ^{φ(x, a1)}

consistent

k-inconsistent

D(Σ, ϕ, ψ) (Ben-Yaacov)

We use D(Σ, φ, ψ) instead of D(Σ, φ, k). ψ is an existential formula such that

ψ(y₁, . . . , y_k) → ¬∃xφ(x, y₁) ∧ · · · ∧ φ(x, y_k)

φ(x, a₀) ^{φ(x, a}1⁾

consistent

for each k elements satisfies ψ

Definition(Ben-Yaacov)

Let φ(x, y ) be an existentiall formula, k < ω, ¯y = y₀, . . . , y_k−1 with lh(yi) = lh(y ). ψ(¯y) is a k-inconsistency witness for φ

⇐⇒

M |= ∀y₀, . . . , y_k−1ψ(y₀, . . . , yk−1) → ¬∃xφ(x, y₀) ∧ · · · ∧ φ(x, y_k−1).

Definition(Ben-Yaacov)

Let φ(x, y ) be an existentiall formula, k < ω, ¯y = y₀, . . . , y_k−1 with lh(yi) = lh(y ). ψ(¯y) is a k-inconsistency witness for φ

⇐⇒

M |= ∀y₀, . . . , y_k−1ψ(y₀, . . . , yk−1) → ¬∃xφ(x, y₀) ∧ · · · ∧ φ(x, y_k−1).

Fact(Ben-Yaacov)

For any existentiall type Σ(x, b), TFAE:

1 Σ(x, b) divides over A

2 ∃φ(x, y ) with Σ(x, y ) ⊢ φ(x, y ),

∃k, ψ(¯y) : k-inconsistency witness for φ s.t.

∃(bi : i < ω) in etp(b/A) with M |= ψ(b_i1, . . . , b_ik) for each i₁ < · · · < ik < ω.

Pillay’s condition forking satisfies

local character

dividing satisfies local character trivial

forking (dividing) satisfies symmetry

forking (dividing) satisfies transitivity

dividing ⇔

∀ Morley seq. ^でdivide Pillay

∀Σ, φ, ψ,

D(Σ, φ, ψ) < ∞ Ben

? Problem 1

For Hrushovski’s Robinson theories forking satisfies

local character

dividing satisfies local character trivial

forking (dividing) satisfies symmetry

forking (dividing) satisfies transitivity

dividing ⇔

∀ Morley seq. ^でdivide Pillay

known

∀Σ, φ, ψ,

D(Σ, φ, ψ) < ∞ Ben

A

Hrushovski’s Robinson theory

Let ∆ be a class of formulas closed under subformulas and Boolian combinations

Hrushovski’s Robinson theory

Let ∆ be a class of formulas closed under subformulas and Boolian combinations

φ is ∃(∆)-formula ⇐⇒ φ = ∃xψ, ψ ∈ ∆. φ is ∀(∆)-formula ⇐⇒ φ = ∀xψ, ψ ∈ ∆.

Hrushovski’s Robinson theory

Let ∆ be a class of formulas closed under subformulas and Boolian combinations

φ is ∃(∆)-formula ⇐⇒ φ = ∃xψ, ψ ∈ ∆. φ is ∀(∆)-formula ⇐⇒ φ = ∀xψ, ψ ∈ ∆. Definition

An ∀(∆)-theory T is a Robinson theory

⇐⇒

if M, N : e.c.m. for T , a ∈ M, b ∈ N, where tp_∆(a) = tp_∆(b) ⇒ tp_∃(∆)(a) = tp_∃(∆)(b)

”e.c.m.” means closed for ∃(∆)-formulas

For Hrushovski’s Robinson theories forking satisfies

local character

dividing satisfies local character trivial

forking (dividing) satisfies symmetry

forking (dividing) satisfies transitivity

dividing ⇔

∀ Morley seq. ^でdivide Pillay

known

∀Σ, φ, ψ,

D(Σ, φ, ψ) < ∞ Ben

A

Problem 2 [P]

For M : simplee. u. domain,

Is ”Lstp(x/A) = Lstp(y /A)” difinable by an existential type over A? For simplicity, we assume A = ∅.

Our arguments in this section refer to ”Shami, Definability in Low Simple Theories, J. S. L. 65. 2000” and Tsuboi’s unpublished note on Shami’s paper.

Difinition Let a, b ∈ M.

1 Lstp(a) = Lstp(b) ⇔ for any E (x, y ) : bounded ∅-invariant equivalence relation, E (a, b) holds.

2 _d(a, b) ≤ 1 ⇔ ∃I : existentially indiscernible sequence s.t. a, b ∈ I

3 _d(a, b) ≤ n ⇔ ∃a0, . . . , an with a0 = a, an= b s.t. d(ai, ai+1) ≤ 1 for any i < n

4 _d(a, b) < ω ⇔ d(a, b) ≤ n for some n < ω

Difinition Let a, b ∈ M.

1 Lstp(a) = Lstp(b) ⇔ for any E (x, y ) : bounded ∅-invariant equivalence relation, E (a, b) holds.

2 _d(a, b) ≤ 1 ⇔ ∃I : existentially indiscernible sequence s.t. a, b ∈ I

3 _d(a, b) ≤ n ⇔ ∃a0, . . . , an with a0 = a, an= b s.t. d(ai, ai+1) ≤ 1 for any i < n

4 _d(a, b) < ω ⇔ d(a, b) ≤ n for some n < ω Fact [P]

Lstp(a) = Lstp(b) ⇔ d(a, b) < ω

Existence of various existentially indiscernible sequences [P]

If (ai : i < λ) is an enoughly long sequence then there is an existentially indiscernible sequence (b_i : i < ω) such that for any n < ω, there are i₀ < · · · < in−1< λ s.t. etp(b0, . . . , bn−1) = etp(ai0, . . . , ai_n−1).

Existence of various existentially indiscernible sequences [P]

If (ai : i < λ) is an enoughly long sequence then there is an existentially indiscernible sequence (b_i : i < ω) such that for any n < ω, there are i₀ < · · · < in−1< λ s.t. etp(b0, . . . , bn−1) = etp(ai0, . . . , ai_n−1).

Fact (M is simple) [P]

∀a, ∀B, ∃a^′ s.t.

Lstp(a^′) = Lstp(a) a⌣^| b

a⌣^| b ⇔ etp(a^′/B) does not fork over ∅.

Fact (M is simple) Independence theorem for simple e.u.domain [P] Lstp(a₁) = Lstp(a₂),

a₁⌣^| b₁, a₂⌣^| b₂, b₁⌣^| b₂

⇒ ∃a s.t.

a|= etp(a1^/b1^{) ∪ etp(a}2^/b2⁾

a⌣^| b₁b₂.

Notation

M^が thick^のとき, ”d(x, y ) ≤ 1”^{を表現する}existential type ^をq₁ ^で表 わす

Lemma 2 (M is thick)

For any M, ”d(x, y ) ≤ 2” is definable by an existential type. Proof.

It is defined by {∃zφ(x, z) ∧ φ(z, y )| φ(x, y ) ∈ q₁(x, y )}.

Lemma 3 (M is thick and simple) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{d(a, b) ≤ 2}

3 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ Proof. (3 → 2 → 1 : trivial)

(1 → 2)

Lemma 3 (M is thick and simple) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{d(a, b) ≤ 2}

3 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ Proof. (3 → 2 → 1 : trivial)

(1 → 2)

Let c be an element s.t. Lstp(c) = Lstp(a) = Lstp(b) and c ⌣^| ab.

Lemma 3 (M is thick and simple) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{d(a, b) ≤ 2}

3 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ Proof. (3 → 2 → 1 : trivial)

(1 → 2)

Let c be an element s.t. Lstp(c) = Lstp(a) = Lstp(b) and c ⌣^| ab. Take a^′ s.t. etp(a^′a) = etp(ac).

Lemma 3 (M is thick and simple) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{d(a, b) ≤ 2}

3 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ Proof. (3 → 2 → 1 : trivial)

(1 → 2)

Let c be an element s.t. Lstp(c) = Lstp(a) = Lstp(b) and c ⌣^| ab. Take a^′ s.t. etp(a^′a) = etp(ac).

Then Lstp(a^′) = Lstp(a) and a^′⌣^| a.

Lemma 3 (M is thick and simple) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{d(a, b) ≤ 2}

3 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ Proof. (3 → 2 → 1 : trivial)

(1 → 2)

Let c be an element s.t. Lstp(c) = Lstp(a) = Lstp(b) and c ⌣^| ab. Take a^′ s.t. etp(a^′a) = etp(ac).

Then Lstp(a^′) = Lstp(a) and a^′⌣^| a.

So, by independence theorem, we can get a₂ s.t. a₂ |= etp(a/c) ∪ etp(a^′/a) and a₂⌣^| ac.

c a

a^′

⌣^|

⌣^|

c a

a^′

⌣^|

⌣^|

a₂

c a

a^′

⌣^|

⌣^|

a₂

a^′₂

c a

a^′

⌣^|

⌣^|

a₂

a^′₂ a₃

c a

a^′

⌣^|

⌣^|

a₂

a^′₂ a₃

Then, we can get a sequence (ai : i < ω) s.t. etp(aiaj) = etp(ac) for each j < i < ω. We can assume this sequence is existentially indiscernible. So, ∃I , J: existentially indiscernible sequences s.t. a, c ∈ I and b, c ∈ J. We have d(c, a) ≤ 1, d(c, b) ≤ 1 and c ⌣^| ab. So, q1(x, a) ∪ q1(x, b) does not fork over ∅.

Lemma 2 (M is thick)

For any M, ”d(x, y ) ≤ 2” is definable by an existential type. Lemma 3 (M is thick and simple)

The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{d(a, b) ≤ 2}

Lemma 2 (M is thick)

For any M, ”d(x, y ) ≤ 2” is definable by an existential type. Lemma 3 (M is thick and simple)

The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{d(a, b) ≤ 2}

Theorem 1 (M is thick and simple)

”Lstp(x) = Lstp(y )” is definable by an existential type. Proof. By the above lemmas.

Problem 3

For M : lowe.u.domain, A ⊂ M, a ∈ M, Lstp(a/A) = stp(a/A) ?

簡単のため_{, A = ∅}とする_.

Problem 3

For M : lowe.u.domain, A ⊂ M, a ∈ M, Lstp(a/A) = stp(a/A) ?

簡単のため_{, A = ∅}とする_. Definition

Let a, b ∈ M. stp(a) = stp(b) ⇔ for any E (x, y ) : definable (by an existential formula over ∅) finite equivalence relation, E (a, b) holds.

Definition M is low ⇔

M is simple

D(x = x, φ) < ω for any φ.

φ(x, a0) ^{φ(x, a1)}

consistent

ψ₁ ψ₂

Lemma 4 (M is thick and low)

(1) {a : φ(x, a) divides over ∅} is definable by an existential type.

Lemma 4 (M is thick and low)

(1) {a : φ(x, a) divides over ∅} is definable by an existential type. (2) {(a, b) : φ(x, a) ∧ φ(x, b) does not divide over ∅}

Lemma 4 (M is thick and low)

(1) {a : φ(x, a) divides over ∅} is definable by an existential type. (2) {(a, b) : φ(x, a) ∧ φ(x, b) does not divide over ∅} is definable by an existential type if it is restricted to (p ⊗ p)^M = {(a, b) : a, b |= p, a ⌣^| b}.

Lemma 4 (M is thick and low)

(1) {a : φ(x, a) divides over ∅} is definable by an existential type. (2) {(a, b) : φ(x, a) ∧ φ(x, b) does not divide over ∅} is definable by an existential type if it is restricted to (p ⊗ p)^M = {(a, b) : a, b |= p, a ⌣^| b}. So, it is definable by an existential universal formula if it is restricted to (p ⊗ p)^M

Lemma 4 (M is thick and low)

(1) {a : φ(x, a) divides over ∅} is definable by an existential type. (2) {(a, b) : φ(x, a) ∧ φ(x, b) does not divide over ∅} is definable by an existential type if it is restricted to (p ⊗ p)^M = {(a, b) : a, b |= p, a ⌣^| b}. So, it is definable by an existential universal formula if it is restricted to (p ⊗ p)^M

Proof.

(1) Note that ∀φ(x, y ), ∃ψ s.t. ∀a, φ(x, a) divides over ∅ ⇒ φ(x, a) devides by an existentially indiscernible sequence in which any k-elements satisfies ψ.

Lemma 4 (M is thick and low)

(1) {a : φ(x, a) divides over ∅} is definable by an existential type. (2) {(a, b) : φ(x, a) ∧ φ(x, b) does not divide over ∅} is definable by an existential type if it is restricted to (p ⊗ p)^M = {(a, b) : a, b |= p, a ⌣^| b}. So, it is definable by an existential universal formula if it is restricted to (p ⊗ p)^M

Proof.

(1) Note that ∀φ(x, y ), ∃ψ s.t. ∀a, φ(x, a) divides over ∅ ⇒ φ(x, a) devides by an existentially indiscernible sequence in which any k-elements satisfies ψ.

(2) For a, b |= p, a ⌣^| b, TFAE:

1 φ(x, a) ∧ φ(x, b) does not divide over ∅

2 _∃a^∗_b^∗ _s.t.

|= φ(a^∗, a) and a^∗⌣^{| a};

|= φ(b^∗, b) and b^∗⌣^{| b}; Lstp(a^∗) = Lstp(b^∗)

a^∗⌣^| a⇔ D(etp(a/a^∗), φ, ψ) ≥ D(p, φ, ψ) for any φ, ψ.

Ep(x),ϕ(x,y )^{(b, c) ⇐⇒}

∀a |= p with a ⌣^| bc,

φ(x, a) ∧ φ(x, b) does not divide over ∅

⇔ φ(x, a) ∧ φ(x, c) does not divide over ∅

Ep(x),ϕ(x,y )^{(b, c) ⇐⇒}

∀a |= p with a ⌣^| bc,

φ(x, a) ∧ φ(x, b) does not divide over ∅

⇔ φ(x, a) ∧ φ(x, c) does not divide over ∅ Lemma 5 (M is thick and low)

Suppose a |= p and φ(x, a) does not divide over ∅. Then Ep(x),ϕ(x,y ) ^{is a}

definable (by an existential formula) finite equivalence relation on (p²)^M.

Ep(x),ϕ(x,y )^{(b, c) ⇐⇒}

∀a |= p with a ⌣^| bc,

φ(x, a) ∧ φ(x, b) does not divide over ∅

⇔ φ(x, a) ∧ φ(x, c) does not divide over ∅ Lemma 5 (M is thick and low)

Suppose a |= p and φ(x, a) does not divide over ∅. Then Ep(x),ϕ(x,y ) ^{is a}

definable (by an existential formula) finite equivalence relation on (p²)^M. Proof.

E_p,ϕ is a bounded equivalence relation: easy, bdd is by

”Lstp(x) = Lstp(y ) ⇒ Ep,ϕ(x, y )”

Ep(x),ϕ(x,y )^{(b, c) ⇐⇒}

∀a |= p with a ⌣^| bc,

φ(x, a) ∧ φ(x, b) does not divide over ∅

⇔ φ(x, a) ∧ φ(x, c) does not divide over ∅ Lemma 5 (M is thick and low)

Suppose a |= p and φ(x, a) does not divide over ∅. Then Ep(x),ϕ(x,y ) ^{is a}

definable (by an existential formula) finite equivalence relation on (p²)^M. Proof.

E_p,ϕ is a bounded equivalence relation: easy, bdd is by

”Lstp(x) = Lstp(y ) ⇒ Ep,ϕ(x, y )”

By the above lemma, ¬Ep,ϕ is definable by an existential type.

Ep(x),ϕ(x,y )^{(b, c) ⇐⇒}

∀a |= p with a ⌣^| bc,

φ(x, a) ∧ φ(x, b) does not divide over ∅

⇔ φ(x, a) ∧ φ(x, c) does not divide over ∅ Lemma 5 (M is thick and low)

Suppose a |= p and φ(x, a) does not divide over ∅. Then Ep(x),ϕ(x,y ) ^{is a}

definable (by an existential formula) finite equivalence relation on (p²)^M. Proof.

E_p,ϕ is a bounded equivalence relation: easy, bdd is by

”Lstp(x) = Lstp(y ) ⇒ Ep,ϕ(x, y )”

By the above lemma, ¬Ep,ϕ is definable by an existential type. E_p,ϕ is a finite equivalence relation

Ep(x),ϕ(x,y )^{(b, c) ⇐⇒}

∀a |= p with a ⌣^| bc,

φ(x, a) ∧ φ(x, b) does not divide over ∅

⇔ φ(x, a) ∧ φ(x, c) does not divide over ∅ Lemma 5 (M is thick and low)

Suppose a |= p and φ(x, a) does not divide over ∅. Then Ep(x),ϕ(x,y ) ^{is a}

definable (by an existential formula) finite equivalence relation on (p²)^M. Proof.

E_p,ϕ is a bounded equivalence relation: easy, bdd is by

”Lstp(x) = Lstp(y ) ⇒ Ep,ϕ(x, y )”

By the above lemma, ¬Ep,ϕ is definable by an existential type. E_p,ϕ is a finite equivalence relation

Let a₁, . . . , a_n: representation of each class

∪{¬E (x, ai) : i ≤ n} is not satisfiable. for simplicity, we assume n = 3.

∃φ(x, y ): eixistential formula s.t. (1) ¬E (x, a_i) ⊢ φ(x, a_i) for each i ≤ 3 (2) M |= ¬∃xφ(x, a1) ∧ φ(x, a2) ∧ φ(x, a3).

∃φ(x, y ): eixistential formula s.t. (1) ¬E (x, a_i) ⊢ φ(x, a_i) for each i ≤ 3 (2) M |= ¬∃xφ(x, a1) ∧ φ(x, a2) ∧ φ(x, a3). Put ψ(x, y ) = ¬φ(x, y ).

∃φ(x, y ): eixistential formula s.t. (1) ¬E (x, a_i) ⊢ φ(x, a_i) for each i ≤ 3 (2) M |= ¬∃xφ(x, a1) ∧ φ(x, a2) ∧ φ(x, a3). Put ψ(x, y ) = ¬φ(x, y ).

Note that M |= ∀x(ψ(x, a₁) ↔ φ(x, a₂) ∧ φ(x, a₃)).

∃φ(x, y ): eixistential formula s.t. (1) ¬E (x, a_i) ⊢ φ(x, a_i) for each i ≤ 3 (2) M |= ¬∃xφ(x, a1) ∧ φ(x, a2) ∧ φ(x, a3). Put ψ(x, y ) = ¬φ(x, y ).

Note that M |= ∀x(ψ(x, a₁) ↔ φ(x, a₂) ∧ φ(x, a₃)). So, ψ(x, a₁) is also existential. By a symmetric argument, ψ(x, a₂), ψ(x, a₃) are all existential.

∃φ(x, y ): eixistential formula s.t. (1) ¬E (x, a_i) ⊢ φ(x, a_i) for each i ≤ 3 (2) M |= ¬∃xφ(x, a1) ∧ φ(x, a2) ∧ φ(x, a3). Put ψ(x, y ) = ¬φ(x, y ).

Note that M |= ∀x(ψ(x, a₁) ↔ φ(x, a₂) ∧ φ(x, a₃)). So, ψ(x, a₁) is also existential. By a symmetric argument, ψ(x, a₂), ψ(x, a₃) are all existential.

E(x, y ) ↔^∧_i≤3(ψ(x, a_i) ↔ ψ(y , a_i)).

∃φ(x, y ): eixistential formula s.t. (1) ¬E (x, a_i) ⊢ φ(x, a_i) for each i ≤ 3 (2) M |= ¬∃xφ(x, a1) ∧ φ(x, a2) ∧ φ(x, a3). Put ψ(x, y ) = ¬φ(x, y ).

Note that M |= ∀x(ψ(x, a₁) ↔ φ(x, a₂) ∧ φ(x, a₃)). So, ψ(x, a₁) is also existential. By a symmetric argument, ψ(x, a₂), ψ(x, a₃) are all existential.

E(x, y ) ↔^∧_i≤3(ψ(x, a_i) ↔ ψ(y , a_i)).

We can omit parameters a_i’s because this does not depend a choice of representations and ψ(x, a_i) is existential universal.

Lemma 3 (M is thick and simple, ^再掲) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ (q₁(x, y ) express ”d(x, y ) ≤ 1”)

Theorem 2 (M is thick and low) stp= Lstp

Proof.

Lemma 3 (M is thick and simple, ^再掲) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ (q₁(x, y ) express ”d(x, y ) ≤ 1”)

Theorem 2 (M is thick and low) stp= Lstp

Proof.

If stp(a) = stp(b), then by the above lemma a, b |= E_p,ϕ for any φ.

Lemma 3 (M is thick and simple, ^再掲) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ (q₁(x, y ) express ”d(x, y ) ≤ 1”)

Theorem 2 (M is thick and low) stp= Lstp

Proof.

If stp(a) = stp(b), then by the above lemma a, b |= E_p,ϕ for any φ. Take c s.t. Lstp(c) = Lstp(a) and c ⌣^| ab.

Lemma 3 (M is thick and simple, ^再掲) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ (q₁(x, y ) express ”d(x, y ) ≤ 1”)

Theorem 2 (M is thick and low) stp= Lstp

Proof.

If stp(a) = stp(b), then by the above lemma a, b |= E_p,ϕ for any φ. Take c s.t. Lstp(c) = Lstp(a) and c ⌣^| ab.

Then, q₁(x, a) ∪ q₁(x, c) does not divide by Lemma 3,

Lemma 3 (M is thick and simple, ^再掲) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ (q₁(x, y ) express ”d(x, y ) ≤ 1”)

Theorem 2 (M is thick and low) stp= Lstp

Proof.

If stp(a) = stp(b), then by the above lemma a, b |= E_p,ϕ for any φ. Take c s.t. Lstp(c) = Lstp(a) and c ⌣^| ab.

Then, q₁(x, a) ∪ q₁(x, c) does not divide by Lemma 3, q₁(x, b) ∪ q1(x, c) does not divide by Ep,ϕ(a, b),

Lemma 3 (M is thick and simple, ^再掲) The following are equivalent:

1 Lstp(a) = Lstp(b)

2 _{q1(x, a) ∪ q1}(x, b) does not fork over ∅ (q₁(x, y ) express ”d(x, y ) ≤ 1”)

Theorem 2 (M is thick and low) stp= Lstp

Proof.

If stp(a) = stp(b), then by the above lemma a, b |= E_p,ϕ for any φ. Take c s.t. Lstp(c) = Lstp(a) and c ⌣^| ab.

Then, q₁(x, a) ∪ q₁(x, c) does not divide by Lemma 3, q₁(x, b) ∪ q1(x, c) does not divide by Ep,ϕ(a, b), Lstp(b) = Lstp(c) by Lemma 3

Another partial answer to Problem 2 (Ben-Yaacov) for M : thicksimplee.u.domain, A ⊂ M,

”Lstp(x/A) = Lstp(y /A)” is definable by an existential type over A. Another partial answer to Problem 3 (Main Theorem)

for M : thicklowe.u.domain, A ⊂ M, a ∈ M, Lstp(a/A) = stp(a/A)

Note that if T = Th_∀(∆)(M) is a Robinson theory, then ”d(x, y ) ≤ 1” (i.e. ”x and y are contained some ∆-indiscernible sequence”) is definable by a ∆-type.