In model theory, a subfield of mathematical logic, an atomic model is a model such that the complete type of every tuple is axiomatized by a single formula. Such types are called principal types, and the formulas that axiomatize them are called complete formulas.
Definitions
Let T be a theory. A complete type p(x1, ..., xn) is called principal or atomic (relative to T) if it is axiomatized relative to T by a single formula φ(x1, ..., xn) ∈ p(x1, ..., xn).
A formula φ is called complete in T if for every formula ψ(x1, ..., xn), the theory T ∪ {φ} entails exactly one of ψ and ¬ψ.[1]
It follows that a complete type is principal if and only if it contains a complete formula.
A model M is called atomic if every n-tuple of elements of M satisfies a formula that is complete in Th(M)—the theory of M.
Examples
- The ordered field of real algebraic numbers is the unique atomic model of the theory of real closed fields.
- Any finite model is atomic.
- A dense linear ordering without endpoints is atomic.
- Any prime model of a countable theory is atomic by the omitting types theorem.
- Any countable atomic model is prime, but there are plenty of atomic models that are not prime, such as an uncountable dense linear order without endpoints.
- The theory of a countable number of independent unary relations is complete but has no completable formulas and no atomic models.
Properties
The back-and-forth method can be used to show that any two countable atomic models of a theory that are elementarily equivalent are isomorphic.
Notes
- ↑ Some authors refer to complete formulas as "atomic formulas", but this is inconsistent with the purely syntactical notion of an atom or atomic formula as a formula that does not contain a proper subformula.
References
- Chang, Chen Chung; Keisler, H. Jerome (1990), Model Theory, Studies in Logic and the Foundations of Mathematics (3rd ed.), Elsevier, ISBN 978-0-444-88054-3
- Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6
Mathematical logic |
|---|
| General |
- Formal language
- Formation rule
- Formal proof
- Formal semantics
- Well-formed formula
- Set
- Element
- Class
- Classical logic
- Axiom
- Rule of inference
- Relation
- Theorem
- Logical consequence
- Type theory
- Symbol
- Syntax
- Theory
|
|---|
| Systems |
- Formal system
- Deductive system
- Axiomatic system
- Hilbert style systems
- Natural deduction
- Sequent calculus
|
|---|
| Traditional logic |
- Proposition
- Inference
- Argument
- Validity
- Cogency
- Syllogism
- Square of opposition
- Venn diagram
|
|---|
Propositional calculus and Boolean logic |
- Boolean functions
- Propositional calculus
- Propositional formula
- Logical connectives
- Truth tables
- Many-valued logic
|
|---|
| Predicate logic |
- First-order
- Quantifiers
- Predicate
- Second-order
- Monadic predicate calculus
|
|---|
| Naive set theory |
- Set
- Empty set
- Element
- Enumeration
- Extensionality
- Finite set
- Infinite set
- Subset
- Power set
- Countable set
- Uncountable set
- Recursive set
- Domain
- Codomain
- Image
- Map
- Function
- Relation
- Ordered pair
|
|---|
| Set theory |
- Foundations of mathematics
- Zermelo–Fraenkel set theory
- Axiom of choice
- General set theory
- Kripke–Platek set theory
- Von Neumann–Bernays–Gödel set theory
- Morse–Kelley set theory
- Tarski–Grothendieck set theory
|
|---|
| Model theory |
- Model
- Interpretation
- Non-standard model
- Finite model theory
- Truth value
- Validity
|
|---|
| Proof theory |
- Formal proof
- Deductive system
- Formal system
- Theorem
- Logical consequence
- Rule of inference
- Syntax
|
|---|
Computability theory |
- Recursion
- Recursive set
- Recursively enumerable set
- Decision problem
- Church–Turing thesis
- Computable function
- Primitive recursive function
|
|---|