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ásSzerkesztés

Ha egy T teljes elsőrendű elmélet, és   konzisztens T-vel, akkor

 

konzisztens. Ha ráadásul   generálja   formulaosztályát, azaz minden   formulára

 ,

akkor T minden modellje megvalósítja  -t. Kontraponálva, ha a  -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ételSzerkesztés

Legyen T elsőrendű elmélet, minden m természetes számra   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   formulahalmazt, akkor
létezik T-nek olyan megszámlálható modellje, mely minden m természetes számra elkerüli a   formulahalmazt.

BizonyításSzerkesztés

A konstrukcióSzerkesztés

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ó

 

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

 

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 ck konstansjel, hogy φ(ck) is T+-beli

3) minden m-re és minden ismétlésmentes L+\L-beli   konstanssorozatra legyen olyan   formula, hogy

 

Fő gondolatSzerkesztés

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 ck új konstans, amire ck=t is T+-beli. Legyen m tetszőleges természetes szám. Az kell, hogy akárhogy is vegyünk   véges sorozatot   univerzumából, legyen olyan Γm-beli formula, mely hamis az   értékelés szerint. Az előbbi, zárt termekre vonatkozó megjegyzés miatt  -t megnevezi egy ismétlésmentes konstanssorozat,  . Ehhez 3) miatt van   formula, hogy  . Világos, hogy akkor

 

nem lehet konzisztens T-vel, mert   mutatja, hogy  -ban igaz a

 

formula.

A „szakértős” konstrukcióSzerkesztés

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ócikkekSzerkesztés