10.1 Omitting types theorem and its proof

The Omitting Types Theorem is a powerful tool in model theory, allowing us to build models that avoid certain types of elements. It's like having a recipe for making custom-made mathematical structures, where we can choose what to include and what to leave out.

This theorem is crucial for constructing models with specific properties, like atomic models or fields without algebraic closures. It's a bit like playing with Lego, where we carefully select and combine pieces to create exactly what we want, while following certain rules.

Omitting types theorem

Definition and key components

Top images from around the web for Definition and key components

• 

  Countable set - Knowino View original

  Is this image relevant?

• 

  Model theory of finite and pseudofinite groups | Archive for Mathematical Logic View original

  Is this image relevant?

• 

  analysis - How do I tell whether axiom of choice is used or not? - Mathematics Stack Exchange View original

  Is this image relevant?

• 

  Countable set - Knowino View original

  Is this image relevant?

• 

  Model theory of finite and pseudofinite groups | Archive for Mathematical Logic View original

  Is this image relevant?

1 of 3

Top images from around the web for Definition and key components

• 

  Countable set - Knowino View original

  Is this image relevant?

• 

  Model theory of finite and pseudofinite groups | Archive for Mathematical Logic View original

  Is this image relevant?

• 

  analysis - How do I tell whether axiom of choice is used or not? - Mathematics Stack Exchange View original

  Is this image relevant?

• 

  Countable set - Knowino View original

  Is this image relevant?

• 

  Model theory of finite and pseudofinite groups | Archive for Mathematical Logic View original

  Is this image relevant?

1 of 3

• Omitting Types Theorem states for a countable first-order theory T, if Σ(x) is a set of formulas not principal over T, there exists a model of T that omits Σ(x)
• Applies to countable theories with countable language and axiom set
• Σ(x) represents a set of formulas in the same free variables (x)
• Σ(x) must not be principal over T (no single formula φ(x) equivalent to entire type Σ(x) in T)
• Requires existence of countable set of constant symbols not in language of T for model construction
• Assumes theory T is consistent

Examples and applications

• Constructing models without certain types of elements (models without transcendental elements)
• Building atomic models (models where every element satisfies a complete formula)
• Creating models with specific algebraic properties (fields without algebraic closures)
• Demonstrating existence of models with countable elementary submodels
• Proving existence of models omitting infinitely many types simultaneously

Proving the omitting types theorem

Language extension and enumeration

• Extend language L of T to L' by adding countably many new constant symbols (c₁, c₂, c₃, ...)
• Enumerate all L'-sentences as {φn : n < ω} (φ₁, φ₂, φ₃, ...)
• Enumerate all L-formulas with one free variable as {ψn(x) : n < ω} (ψ₁(x), ψ₂(x), ψ₃(x), ...)

Theory chain construction

• Build chain of consistent L'-theories T = T₀ ⊆ T₁ ⊆ T₂ ⊆ ... with union T* as complete L'-theory
• Ensure Tₙ₊₁ decides φn (contains either φn or ¬φn)
• For each ψn(x) not in Σ(x), include witness in Tₙ₊₁ (sentence ψn(c) for some constant c)
• Prove T* omits Σ(x) by demonstrating T* ∪ Σ(c) inconsistency for any constant c
• Construct model M of T* using Henkin construction, yielding model of T omitting Σ(x)

Consistency maintenance and witnessing

• Verify consistency at each step of theory chain construction
• Add witnesses carefully to avoid introducing inconsistencies
• Balance between adding enough information to decide sentences and maintaining consistency
• Use compactness theorem to ensure overall consistency of the constructed theory T*

Consistency and realizability in omitting types

Role of consistency

• Ensures existence of model for theory T
• Guides construction of theory chain T₀ ⊆ T₁ ⊆ T₂ ⊆ ...
• Allows for simultaneous satisfaction of T and omission of Σ(x)
• Crucial for applying compactness theorem in the proof

Concept of realizability

• Refers to finding witness (constant c) satisfying formula ψ(x) in theory
• Non-realizability of Σ(x) used to construct model omitting this type
• Realizability checks performed at each stage for formulas not in Σ(x)
• Balances adding witnesses for realizable formulas while omitting non-realizable types

Interplay between consistency and realizability

• Consistency checks ensure adding witnesses doesn't lead to contradictions
• Realizability guides selection of formulas to witness in the construction
• Combination allows for building models with specific properties (omitting certain types)
• Demonstrates relationship between syntactic properties (consistency, realizability) and semantic properties (model existence, type omission)

Significance of omitting types in model theory

Model construction and analysis

• Provides powerful tool for building models with specific properties
• Cornerstone in study of countable first-order theories and their models
• Enables construction of atomic models and prime models
• Facilitates creation of models omitting multiple types simultaneously

Theoretical implications

• Central to development of stability theory in model theory
• Highlights importance of principal types concept
• Demonstrates limitations of first-order logic in capturing certain structures (uncountable structures unable to omit non-principal types)
• Establishes connections between syntactic theory properties and semantic model properties

Applications in mathematics

• Used in algebraic geometry to construct generic models
• Applies in functional analysis for creating specific operator algebras
• Aids in constructing models in set theory with desired combinatorial properties
• Utilized in differential geometry for building manifolds with particular characteristics