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 ${}_{𝔭(x_1,x_2,...,x_n)=\{\phi (x_1,x_2,...,x_n),\dots \}}$ formulaosztályát értjük, mely különböző mellékfeltételeknek tesz eleget. Egy ${}_{𝔭(x_1,x_2,\dots ,x_n)}$ 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 x₁, x₂, …, x_n változókat tartalmazó formulák egy ${}_{𝔭(x_1,x_2,...,x_n)}$ halmazáról azt mondjuk, hogy parciális típusa T-nek, ha ${}_{𝔭(x_1,x_2,...,x_n)}$ konzisztens T-vel, azaz létezik T-nek olyan ${}_{𝔄}$ modellje és olyan A-beli a₁, a₂, …, a_n sorozat, hogy minden ${}_{\phi \in 𝔭(x_1,x_2,...,x_n)}$-ra

$𝔄\models \phi [a_1,a_2,...,a_n]$

(ez pont azt jelenti, hogy ${}_{𝔄}$-ban realizálható ${}_{𝔭(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 ${}_{𝔭}$ 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 ${}_{{𝔭}_0}$ részére

$\mathrm{\Gamma }\models (\mathrm{\exists }𝐯)\wedge {𝔭}_0$

3. minden ${}_{\phi }$ formula esetén, amiben csak v változói szerepelnek vagy ${}_{\phi \in 𝔭}$ vagy ${}_{\mathrm{\neg }\phi \in 𝔭}$

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 ezt a típust.
• $\{\mathrm{\forall }y(y^2<2\to y<x),\mathrm{\forall }y((y>0\wedge y^2>2)\to 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 ${}_{𝔄}$ modell univerzumából vett sorozat, akkor

$\{\phi (x_1,x_2,...,x_n)\mid 𝔄\models \phi [a_1,a_2,...,a_n]\}$

egy teljes típus a ${}_{𝖳𝗁𝔄}$ elméletben (a modellbeli igaz mondatok elméletében) és az (a₁,a₂,…,a_n) sorozat ${}_{𝔄}$-beli típusának nevezzük.

• Ha ${}_{𝔄}$ modellje az ${}_{ℒ}$ nyelvnek és X ⊆ A, akkor definiálható az az ${}_{{ℒ}_X}$ nyelv, melyet úgy kapunk, hogy ${}_{ℒ}$-et a {c_x | x ∈ X} konstansokkal bővítjük. Az ${}_{{𝔄}_X}$ modell annyiban különbözik ${}_{𝔄}$-tól, hogy a c_x konstans interpretáltja x. Ekkor ${}_{𝖳𝗁{𝔄}_X}$ 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 ${}_{{ℒ}_X}$ nyelvbeli Γ formulahalmaz akkor és csak akkor X-típus, ha:

Γ konzisztens ${}_{𝖳𝗁{𝔄}_X}$-szel és maximális ilyen.

Ez ekvivalens azzal, hogy

Γ minden véges része kielégíthető ${}_{{𝔄}_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 ${}_{𝔄}$ 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ő ${}_{{𝔄}_X}$-ben.

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

Sablon:Bővebben 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 θ $\to$ φ 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

• Sablon:Cite web Előadásjegyzet.
• Sablon:Cite book Egyetemi jegyzet.