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 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 ${\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 ezt a típust.
• $\{\forall y(y^{2}<2\rightarrow y<x),\forall y((y>0\land 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.