A matematikai logikában közelebbről a modellelméletben típuson egy elsőrendű nyelv x1, x2, ..., xn változósorozatát tartalmazó adott formulaosztályát értjük, mely különböző mellékfeltételeknek tesz eleget. Egy típussal kapcsolatban a leggyakoribb kérdés, hogy a nyelv egy modellje mikor valósítja meg (realizálja), azaz A-ban a változók alkalmas értékelésével egyszerre igazzá tehető-e a típus összes eleme és mikor hagyja ki (kerüli el), azaz mikor lehetetlen kielégíteni egyszerre a típus összes elemét. Ez utóbbi esetre adnak elégséges feltételt a típuselkerülési tételek.

Teljes és parciális típusok

Legyen T elmélet egy elsőrendű nyelvben. A legfeljebb csak az x1, x2, ..., xn változókat tartalmazó formulák egy halmazáról azt mondjuk, hogy parciális típusa T-nek, ha konzisztens T-vel, azaz létezik T-nek olyan modellje és olyan A-beli a1, a2, ..., an sorozat, hogy minden -ra

(ez pont azt jelenti, hogy -ban realizálható ) és teljes típusa, ha ezen kívül maximális is, azaz nem bővíthető konzisztensen tovább.

Ekvivalens definíció

Ha v változók egy véges sorozata, akkor formulahalmaz teljes v-típus a Γ elméletben, ha 1. elemeiben csak a v-beli változók fordulnak elő szabadon, 2. minden véges részére

3. minden formula esetén, amiben csak v változói szerepelnek vagy vagy

Példák formulaosztály parciális típusa az aritmetikának; egy modell pontosan akkor sztenderd (azaz elemien ekvivalens ω-val, ahol ω a véges rendszámok halmaza), ha elkerüli ezt a típust. parciális típus a rendezett testek elméletében és a négyzetgyök kettő számot szándékozna megfogalmazni; míg Q kihagyja ezt a típust, addig R realizája. Ha a1, a2, ..., an az modell univerzumából vett sorozat, akkor

egy teljes típus a elméletben (a modellbeli igaz mondatok elméletében) és az (a1,a2,…,an) sorozat -beli típusának nevezzük. Ha modellje az nyelvnek és X ⊆ A, akkor definiálható az az nyelv, melyet úgy kapunk, hogy -et a {cx | x ∈ X} konstansokkal bővítjük. Az modell annyiban különbözik -tól, hogy a cx konstans interpretáltja x. Ekkor teljes típusai az úgy nevezett -beli X típusok.

Modellbeli típusok és szaturáltság

A példák közül az utolsó olyan jelentős, hogy gyakran egyszerűen ezt a fogalmat nevezik típusnak. Eszerint az elsőrendű nyelv modellje és X ⊆ A esetén a nyelvbeli Γ formulahalmaz akkor és csak akkor X-típus, ha: Γ konzisztens -szel és maximális ilyen. Ez ekvivalens azzal, hogy Γ minden véges része kielégíthető -ben és maximális ilyen. Az összes, adott számosságnál kisebb méretű X részhalmazhoz tartozó X-típust realizáló modelleket nevezik szaturált modelleknek. Pontosabban, adott κ számosság esetén az modellt κ-szaturáltnak nevezzük, ha tetszőleges κ-nál kisebb számosságú X ⊆ A esetén minden X-típus kielégíthető -ben. Típuskihagyás (típuselkerülés)

A szaturált modellek az összes elég „kis” számosságú X részhalmazból építkező X-típust realizálják. A fogalom ellenpontja bizonyos szempontból, amikor egy teljes típust ki nem elégítő modelleket keresünk. Ezekről szól a típuskihagyási tétel: Ha egy elmélet lokálisan kihagyja a Γm (m ∈ ω) formulahalmazokat, akkor van az elméletnek olyan modellje, mely kihagyja az összes Γm-et.

Itt a lokális kihagyáson a következőket kell érteni. Ha van a T elmélettel konzisztens θ formula, hogy θ φ levezethető minden φ∈Γ-ra, akkor azt mondjuk, hogy T lokálisan megvalósítja Γ-t (θ-t tanúnak nevezzük). Ellenkező esetben T lokálisan elkerüli Γ-t.

Külső hivatkozások Előadásjegyzet. Egyetemi jegyzet.

Kategória:Modellelmélet Kategória:Matematikai logika