Típuselkerülési tétel

A matematikai logikában, közelebbről a modellelméletben a szaturált modellek az összes elég „kis” számosságú X részhalmazból építkező X-típust megvalósítják. A fogalom ellenpontja bizonyos szempontból, amikor egy teljes típust ki nem elégítő modelleket keresünk. Ilyen modellek létezéséről szól a típuselkerülési tétel.

Típuselkerülés és megvalósítás

Ha egy T teljes elsőrendű elmélet, és ${}_{\vartheta (x_1,...,x_{n_m})}$ konzisztens T-vel, akkor

$T\cup \{(\mathrm{\exists }\bar{x})\vartheta (\bar{x})\}$

konzisztens. Ha ráadásul ${}_{\vartheta (x_1,...,x_n)}$ generálja ${}_{\mathrm{\Gamma }(x_1,...,x_n)}$ formulaosztályát, azaz minden ${}_{\psi (x_1,...,x_n)\in \mathrm{\Gamma }(x_1,...,x_n)}$ formulára

$T\models (\mathrm{\forall }\bar{x})\vartheta (\bar{x})\to \psi (\bar{x})$,

akkor T minden modellje megvalósítja ${}_{\mathrm{\Gamma }(x_1,...,x_n)}$-t. Kontraponálva, ha a ${}_{\mathrm{\Gamma }(x_1,...,x_n)}$-t T elkerüli, akkor lokálisan is elkerüli. Ennek a viszonylag egyszerű megállapításnak a fordítottja is igaz (ráadásul nem is kell, hogy T teljes legyen).

Típuselkerülési tétel

Legyen T elsőrendű elmélet, minden m természetes számra ${}_{{\mathrm{\Gamma }}_m(x_1,...,x_{n_m})}$ formulahalmaz T nyelvén. Ha

(1) T nyelve megszámlálható,

(2) T konzisztens és

(3) minden m-re T lokálisan elkerüli a ${}_{{\mathrm{\Gamma }}_m(x_1,...,x_{n_m})}$ formulahalmazt, akkor

létezik T-nek olyan megszámlálható modellje, mely minden m természetes számra elkerüli a ${}_{{\mathrm{\Gamma }}_m(x_1,...,x_{n_m})}$ formulahalmazt.

Bizonyítás

A konstrukció

Ha L a T nyelve, akkor konstruálni fogunk az L-nek olyan L⁺ és a T-nek olyan L⁺ feletti T⁺ bővítését, mely elmélet kanonikus modelljének L reduktuma a kívánt tulajdonságú. Megadunk véges elméletek olyan megszámlálható

$T_0\subseteq T_1\subseteq ...\subseteq T_i...$

láncolatát, melynek T-vel vett uniója a T⁺-t adja:

$T^{+}=T\cup \bigcup _{i=0}^{\mathrm{\infty }}{T}_i$

T⁺-t úgy fogjuk megkonstruálni, hogy teljesítse a következő kitételeket:

1) T⁺ teljes, azaz minden az L⁺ nyelven felírt mondat vagy negáltja T⁺-beli.

2) tetszőleges φ(x) egyváltozós formulára, ha a (∃x)φ(x) formula T⁺-beli, akkor legyen megszámlálhatóan végtelen sok különböző új c_k konstansjel, hogy φ(c_k) is T⁺-beli

3) minden m-re és minden ismétlésmentes L⁺\L-beli ${}_{(c_1,...,c_{n_m})}$ konstanssorozatra legyen olyan ${}_{\gamma (x_1,...,x_{n_m})\in {\mathrm{\Gamma }}_m}$ formula, hogy

$\mathrm{\neg }\gamma (c_1,...,c_{n_m})\in T^{+}$

Fő gondolat

Ha T ezeket mutatja, akkor készen vagyunk. Legyen ugyanis ${}_{𝔄}$ a T⁺ kanonikus modellje. Ismert, hogy egy teljes elmélet a kanonikus modellje valóban modellje az elméletnek, ha minden egyváltozós, levezethető egzisztenciális (∃x)φ(x) formula esetén létezik a nyelvnek olyan t zárt termje, mellyel a φ(t) mondat levezethető. Ezt T⁺ tudja, mert 1) miatt teljes és 2) pont az előző kitételt állítja. Így ${}_{𝔄}$ a részelméletnek is modellje, ill. ${}_{𝔄}$ L reduktuma is modellje T-nek.

Belátjuk T elkerülési tulajdonságot. A modell univerzumának elemei (lényegében) zárt termek. De minden zárt t term esetén a (∃x)(x=t) egzisztenciális kijelentés márcsak logikai okokból is levezethető, így 2) miatt lesz végtelen sok c_k új konstans, amire c_k=t is T⁺-beli. Legyen m tetszőleges természetes szám. Az kell, hogy akárhogy is vegyünk ${}_{(a_1,...,a_{n_m})}$ véges sorozatot ${}_{𝔄}$ univerzumából, legyen olyan Γ_m-beli formula, mely hamis az ${}_{(a_1,...,a_{n_m})}$ értékelés szerint. Az előbbi, zárt termekre vonatkozó megjegyzés miatt ${}_{(a_1,...,a_{n_m})}$-t megnevezi egy ismétlésmentes konstanssorozat, ${}_{(c_1,...,c_{n_m})}$. Ehhez 3) miatt van ${}_{\gamma (x_1,...,x_{n_m})\in {\mathrm{\Gamma }}_m}$ formula, hogy ${}_{\mathrm{\neg }\gamma (c_1,...,c_{n_m})\in T^{+}}$. Világos, hogy akkor

$\gamma (x_1,...,x_{n_m})$

nem lehet konzisztens T-vel, mert ${}_{(a_1,...,a_{n_m})}$ mutatja, hogy ${}_{𝔄}$-ban igaz a

$\mathrm{\neg }(\mathrm{\exists }(x_1,...,x_{n_m}))\gamma (x_1,...,x_{n_m})$

formula.

A „szakértős” konstrukció

Azt, hogy létezik T⁺, mely teljesíti 1), 2), 3)-at a W. Hodeges által papírra vetett, de a modellelmélészek körében közismert módszerrel látjuk be.

Kapcsolódó szócikkek

• Modellelmélet
• Típus (modellelmélet)
• Matematikai struktúra