Típuselkerülési tétel

A Wikipédiából, a szabad enciklopédiából

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[szerkeszté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étel[szerkeszté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ás[szerkeszté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ő gondolat[szerkeszté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ócikkek[szerkesztés]