Típus (modellelmélet)

A matematikai logikában közelebbről a modellelméletben típuson egy elsőrendű nyelv x₁, x₂, …, x_n 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

Legyen T elmélet egy $\mbox{ }_\mathcal{L}$ elsőrendű nyelvben. A legfeljebb csak az x₁, x₂, …, x_n 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 a₁, a₂, …, a_n 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ó

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

• $\{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 a₁, a₂, …, a_n 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 (a₁,a₂,…,a_n) sorozat $\mbox{ }_\mathfrak{A}$-beli típusának nevezzük.

• Ha $\mbox{ }_\mathfrak{A}$ modellje az $\mbox{ }_\mathcal{L}$ nyelvnek és X ⊆ A, akkor definiálható az az $\mbox{ }_{\mathcal{L}_X}$ nyelv, melyet úgy kapunk, hogy $\mbox{ }_\mathcal{L}$-et a {c_x | x ∈ X} konstansokkal bővítjük. Az $\mbox{ }_{\mathfrak{A}_X}$ modell annyiban különbözik $\mbox{ }_\mathfrak{A}$-tól, hogy a c_x 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

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 X ⊆ A 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ú X ⊆ A esetén minden X-típus kielégíthető $\mbox{ }_{\mathfrak{A}_X}$-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 θ $\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

• Sági, Gábor: Válogatott fejezetek a modellelméletből és határterületeiből (PDF), 2005. április 4 Előadásjegyzet.
• Csirmaz, László. 9. Alkalmazások, Matematikai logika (tömörített Postscript), Budapest: ELTE, 90–93. o (1993)  Egyetemi jegyzet.