PlanetMath (more info)
 Math for the people, by the people.
Encyclopedia | Requests | Forums | Docs | Wiki | Random | RSS  
Login
create new user
name:
pass:
forget your password?
Main Menu
sections
Encyclopædia
Papers
Books
Expositions

meta
Requests (210)
Orphanage
Unclass'd (1)
Unproven (472)
Corrections (37)
Classification

talkback
Polls
Forums
Feedback
Bug Reports

downloads
Snapshots
PM Book

information
News
Docs
Wiki
ChangeLog
TODO List
Legalese
About
Owner confidence rating: Very low Entry average rating: No information on entry rating
type (Definition)

Let $ L$ be a first order language. Let $ M$ be an $ L$-structure. Let $ B \subseteq M$, and let $ a \in M^{n}$. Then we define the type of $ a$ over $ B$ to be the set of $ L$-formulas $ \phi(x,\bar{b})$ with parameters $ \bar{b}$ from $ B$ so that $ M \models \phi(a,\bar{b})$. A collection of $ L$-formulas is a complete $ n$-type over $ B$ iff it is of the above form for some $ B,M$ and $ a \in M^{n}$.


We call any consistent collection of formulas $ p$ in $ n$ variables with parameters from $ B$ a partial $ n$-type over $ B$. (See criterion for consistency of sets of formulas.)


Note that a complete $ n$-type $ p$ over $ B$ is consistent so is in particular a partial type over $ B$. Also $ p$ is maximal in the sense that for every formula $ \psi(x,\bar{b})$ over $ B$ we have either $ \psi(x,\bar{b}) \in p$ or $ \lnot \psi(x,\bar{b}) \in p$. In fact, for every collection of formulas $ p$ in $ n$ variables the following are equivalent:

  • $ p$ is the type of some sequence of $ n$ elements $ a$ over $ B$ in some model $ N \equiv M$
  • $ p$ is a maximal consistent set of formulas.

For $ n \in \omega$ we define $ S_{n}(B)$ to be the set of complete $ n$-types over $ B$.


Some authors define a collection of formulas $ p$ to be a $ n$-type iff $ p$ is a partial $ n$-type. Others define $ p$ to be a type iff $ p$ is a complete $ n$-type.


A type (resp. partial type/complete type) is any $ n$-type (resp. partial type/complete type) for some $ n \in \omega$.



"type" is owned by ratboy. [ full author list (2) | owner history (1) ]
(view preamble)

View style:

See Also: formula, definable type, first order language

Also defines:  type, complete type, partial type

Attachments:
definable type (Definition) by Timmy
Log in to rate this entry.
(view current ratings)

Cross-references: sequence, the following are equivalent, criterion for consistency of sets of formulas, variables, formulas, consistent, iff, complete, collection, parameters, first order language
There are 58 references to this entry.

This is version 3 of type, born on 2003-01-22, modified 2006-09-01.
Object id is 3913, canonical name is Type2.
Accessed 14341 times total.

Classification:
AMS MSC: 03C07 (Mathematical logic and foundations :: Model theory :: Basic properties of first-order languages and structures)
Pending Errata and Addenda
None.
[ View all 2 ]
Discussion
Style: Expand: Order:
forum policy

No messages.

Interact
post | correct | update request | add derivation | add example | add (any)