Ugrás a tartalomhoz

Típus (modellelmélet)

Ellenőrzött
A Wikipédiából, a szabad enciklopédiából

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

[szerkesztés]

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ó

[szerkesztés]

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

[szerkesztés]
  • 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 XA, akkor definiálható az az nyelv, melyet úgy kapunk, hogy -et a {cx | xX} 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

[szerkesztés]

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 XA 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ú XA esetén minden X-típus kielégíthető -ben.

Típuskihagyás (típuselkerülés)

[szerkeszté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

[szerkesztés]