Típus (modellelmélet)

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 \mbox{ }_{\mathfrak{p}(x_1,x_2,...,x_n)=\{\varphi(x_1,x_2,...,x_n),\ldots\}} formulaosztályát értjük, mely különböző mellékfeltételeknek tesz eleget. Egy \mbox{ }_{\mathfrak{p}(x_1,x_2,\ldots,x_n)} típussal kapcsolatban a leggyakoribb kérdés, hogy a nyelv egy \mbox{ }_\mathfrak{A} 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 lehetelen 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 | forrásszöveg szerkesztése]

Legyen T elmélet egy \mbox{ }_\mathcal{L} elsőrendű nyelvben. A legfeljebb csak az x1, x2, …, xn változókat tartalmazó formulák egy \mbox{ }_{\mathfrak{p}(x_1,x_2,...,x_n)} halmazáról azt mondjuk, hogy parciális típusa T-nek, ha \mbox{ }_{\mathfrak{p}(x_1,x_2,...,x_n)} konzisztens T-vel, azaz létezik T-nek olyan \mbox{ }_{\mathfrak{A}} modellje és olyan A-beli a1, a2, …, an sorozat, hogy minden \mbox{ }_{\varphi\in\mathfrak{p}(x_1,x_2,...,x_n)}-ra

\mathfrak{A}\models\varphi[a_1,a_2,...,a_n]

(ez pont azt jelenti, hogy \mbox{ }_\mathfrak{A}-ban realizálható \mbox{ }_{\mathfrak{p}(x_1,x_2,...,x_n)}) é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 | forrásszöveg szerkesztése]

Ha v változók egy véges sorozata, akkor \mbox{ }_{\mathfrak{p}} formulahalmaz teljes v-típus a Γ elméletben, ha

1. \mbox{ }_{\mathfrak{p}} elemeiben csak a v-beli változók fordulnak elő szabadon,
2. \mbox{ }_{\mathfrak{p}} minden véges \mbox{ }_{\mathfrak{p}_0} részére
\Gamma\models (\exists \mathbf{v})\wedge\mathfrak{p}_0
3. minden \mbox{ }_{\varphi} formula esetén, amiben csak v változói szerepelnek vagy \mbox{ }_{\varphi\in\mathfrak{p}} vagy \mbox{ }_{\neg\varphi\in\mathfrak{p}}

Példák[szerkesztés | forrásszöveg szerkesztése]

  • \{x>0,x>1,x>2,x>3,...,x>n,...\}=\{x>n\}_{n\in\omega} 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.
  • \{\forall y(y^2<2 \rightarrow y<x),\forall y((y>0 \and y^2>2) \rightarrow y>x)\} 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 \mbox{ }_\mathfrak{A} modell univerzumából vett sorozat, akkor
\{\varphi(x_1,x_2,...,x_n)\mid \mathfrak{A}\models\varphi[a_1,a_2,...,a_n]\}
egy teljes típus a \mbox{ }_{\mathsf{Th}\,\mathfrak{A}} elméletben (a modellbeli igaz mondatok elméletében) és az (a1,a2,…,an) sorozat \mbox{ }_\mathfrak{A}-beli típusának nevezzük.
  • Ha \mbox{ }_\mathfrak{A} modellje az \mbox{ }_\mathcal{L} nyelvnek és XA, akkor definiálható az az \mbox{ }_{\mathcal{L}_X} nyelv, melyet úgy kapunk, hogy \mbox{ }_\mathcal{L}-et a {cx | xX} konstansokkal bővítjük. Az \mbox{ }_{\mathfrak{A}_X} modell annyiban különbözik \mbox{ }_\mathfrak{A}-tól, hogy a cx konstans interpretáltja x. Ekkor \mbox{ }_{\mathsf{Th}\,\mathfrak{A}_X} teljes típusai az úgy nevezett \mbox{ }_\mathfrak{A}-beli X típusok.

Modellbeli típusok és szaturáltság[szerkesztés | forrásszöveg szerkesztése]

A példák közül az utolsó olyan jelentős, hogy gyakran egyszerűen ezt a fogalmat nevezik típusnak. Eszerint az \mbox{ }_\mathcal{L} elsőrendű nyelv \mbox{ }_\mathfrak{A} modellje és XA esetén a \mbox{ }_{\mathcal{L}_X} nyelvbeli Γ formulahalmaz akkor és csak akkor X-típus, ha:

Γ konzisztens \mbox{ }_{\mathsf{Th}\,\mathfrak{A}_X}-szel és maximális ilyen.

Ez ekvivalens azzal, hogy

Γ minden véges része kielégíthető \mbox{ }_{\mathfrak{A}_X}-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 \mbox{ }_\mathfrak{A} modellt κ-szaturáltnak nevezzük, ha

tetszőleges κ-nál kisebb számosságú XA esetén minden X-típus kielégíthető \mbox{ }_{\mathfrak{A}_X}-ben.

Típuskihagyás (típuselkerülés)[szerkesztés | forrásszöveg szerkesztése]

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 θ \rightarrow φ 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 | forrásszöveg szerkesztése]