Logika előadás 2000, Október 25

1. Leszálló Löwenheim-Skolem tétel

Tétel (Tarski–Vaught krtérium) Legyen 𝔅 részstruktúrája 𝔄-nak. 𝔅 akkor és csak akkor elemi rész, ha minden 𝔅 feletti e értékelésre és ∃x φ formulára igaz a következő implikáció: ha 𝔄 ⊧ ∃x φ[e], akkor van olyan b ∈ B, amire 𝔄 ⊧ φ[e[x/b]]. Bizonyítás Először tegyük fel, hogy 𝔅 elemi része 𝔄-nak. Az elemi rész definíciója miatt ha egy 𝔅 feletti e értékeléssel 𝔄-ban igaz egy formula, akkor ugyanazzal az értékeléssel 𝔅-ben is igaz, vagyis 𝔅 ⊧ ∃x φ[e]. Ez pedig azt jelenti, hogy van b ∈ B, amire 𝔅 ⊧ φ[e[x/b]]. Megint az elemi rész definíciója miatt ekkor 𝔄 ⊧ φ[[e[x/b]], hiszen ez egy 𝔅 feletti értékelés.

Fordítva tegyük fel, hogy 𝔄-ra és 𝔅-re áll a fenti implikáció. A φ formula felépítésére vonatkozó indukcióval mutatjuk meg, hogy az elemi rész definíciója erre a két struktúrára fennáll. Prímformulákra azért, mert feltétel szerint 𝔅 részstruktúrája 𝔄-nak. φ-ről ¬φ-re; illetve φ és ψ-ről φ ∨ ψ-re trivi. Tegyük most fel, hogy az elemi rész definíciója φ-re és tetszőleges 𝔅 feletti értékelésre teljesül, és nézzük ∃φ-t. Ha 𝔅 ⊧ ∃φ[e], akkor 𝔅 ⊧ φ[e[x/b]] valamilyen b ∈ B-vel, az indukciós hipotézis miatt 𝔄 ⊧ φ[e[x/b]], tehát 𝔄 ⊧ ∃φ[e]. Ha most 𝔄 ⊧ ∃φ[e], akkor az állításban szereplő feltétel miatt van b ∈ B, amivel 𝔄 ⊧ φ[e[x/b]], ahonnan az indukció miatt 𝔅 ⊧ φ[e[x/b]], ahonnan 𝔅 ⊧ ∃φ[e], ahogyan kívántuk. QED

Tétel Legyen 𝔄 egy végtelen t típusú struktúra, X ⊆ A. Ekkor van 𝔄-nak olyan 𝔅 elemi része, hogy X ⊆ B, és |B| ≤ |X| · |t| · ω Bizonyítás Legyen φ(x, y_{1}, …, y_{n}) egy formula, az ehhez tartozó f_{φ} Skolem-függvény olyan A-n értelmezett n-változós függvény, hogy tetszőleges a_{1}, …, a_{n} ∈ A elemekre, ha létezik egyátalán olyan b ∈ A, amivel 𝔄 ⊧ φ(b, a_{1}, …, a_{n}), akkor f_{φ}(a_{1}, …, a_{n}) ilyen.

Rögzítsünk minden formulához egy Skolem-függvényt. Ha az 𝔄 struktúra alaphalmazának egy B ⊆ A része zárt az összes Skolem-függvényre, akkor B részstruktúrát indukál (B zárt a függvényekre, amit az x = f(y_{1}, …, y_{n}) formulához tartozó Skolem-függvény mutat); továbbá a Tarski–Vaught kritérium alapján elemi rész is.

Mivel formulából |t|·ω darab van, azért ha X-et az összes Skolem-függvényre lezárjuk, legfeljebb |X|·|t|·ω számosságú halmazt kapunk. QED

Következmény (Leszálló Löwenheim-Skolem tétel) Ha egy Γ formulahalmaznak van modellje, akkor van legfeljebb |Γ| · |t| · ω számosságú modellje is.

Így például a halmazelmélet axiómarendszerének (egyetlen kétváltozós relációjel) ha van egyátalán modellje, akkor van megszámlálható modellje is.

A leszálló és felszálló Löwenheim–Skolem tételek együtt azt mondják ki, hogy ha egy Γ formulahalmaznak van végtelen modellje, akkor minden κ ≥ |t|ω̇ számosságra van pontosan κszámosságú modellje is.

2. Elsőfokú rezolóciós módszer

Legyen Γ egy t típusú formulákból álló formulahalmaz. Olyan eljárást keresünk, ami megmondja, hogy Γ-nak van-e modellje. Ehhez Γ elemeit átalakítjuk más típusú formulákká, de azt nem változtatjuk meg, hogy Γ kielégíthető-e.

Elsőként Γ elemeiből elhagyjuk az = jelet, és helyette egy új kétváltozós E(x, y) relációjelet vezetünk be: a k_{1} = k_{2} alakú részformulákat E(k_{1}, k_{2})-vel helyettesítjük. Ezen kívül Γ-hoz hozzávesszük az alábbi egyenlőség axiómákat: E1 E(x, x) E2 E(x, y) → E(y, x) E3 E(x, y) ∧ E(y, z) → E(x, z) E4 minden r relációjelre

(E(x_{1}, y_{1}) ∧ … ∧ E(x_{n}, y_{n})) → (r(x_{1}, …, x_{n}) ↔ r(y_{1}, …, y_{n}))

E5 minden f függvényjelre

(E(x_{1}, y_{1}) ∧ … ∧ E(x_{n}, y_{n})) → E(f(x_{1}, …, x_{n}), f(y_{1}, …, y_{n}))

Legyen az így kapott t′ típusú formulahalmaz Γ′. Ha Γ-nak van modellje, akkor persze Γ′-nek is van, egyszerűen E interpretáltja az igazi egyenlőség. Fordítva, ha Γ′-nek van modellje, akkor abban E interpretáltja az egyenlőség-axiómák miatt ekvivalencia reláció és kompatibilis a függvényjelek illetve relációjelek interpretáltjával, ezért a modellt e szerint le lehet faktorizálni. A faktormodell könnyen láthatóan modellje lesz Γ-nak.

Másodikként Γ′ elemeit prenex alakra hozzuk. Egy formula prenex alakú, ha benne a kvantorok elöl vannak, a kvantorok után egy kvnatormentes formula következik. Ezt az alábbi szabályok alkalmazásával tesszük:

¬∃xφ ⇒ ∀x¬φ ¬∀xφ ⇒ ∃x¬φ (∃xφ) ∨ ψ ⇒ ∃y(φ[x/y] ∨ ψ), ahol y olyan változójel, ami nem fordul máshol elő; hasonlóan a ∀ kvantorra. Ezek az átalakítások nem változtatják meg a formula értelmét, vagyis tetszőleges struktúrában tetsző-

leges értékelés mellett a bal oldali formula pontosan akkor igaz, ha a jobb oldali. Ezért Γ′ minden elemét prenex alakra hozhatjuk, ez nem változtat azon, hogy Γ′ kielégíthető-e vagy sem.

Utoljára minden egyes prenex alakú formulával a következőket csináljuk. Ha a formula nem volna zárt, akkor lezárjuk; ha ezek után nem ∀ kvantorral kezdődne, akkor elé teszünk egy univerzális kvantort olyan változóval, ami egyátalán nem fordul elő a formulában; végül további kvantorokat szúrunk be, hogy az univerzális és egzisztenciális kvantorok felváltva álljanak, és az utolsó kvantor egzisztenciális legyen. Ezek megintcsak nem változtatják meg a formula értelmét. Formulánk így néz ki:

∀x_{1}∃y_{1}∀x_{2}∃y_{2} … ∀x_{n}∃y_{n}ψ(x_{1}, y_{1}, …, x_{n}, y_{n}),

ahol ψ már kvantormentes. Ehhez a formulához választunk n darab vadonatúj függvényjelet: f_{1}(x_{1}), f_{2}(x_{1}, x_{2}), …, f_{n}(x_{1}, …, x_{n}), és ezeket a ψ formulában rendre az y_{1}, y_{2}, stb változójelek helyébe írjuk, az y-okat pedig kitöröljük:

∀x_{1} … ∀x_{n}ψ(x_{1}, f(x_{1}), …, x_{n}, f(x_{1}, …, x_{n})).

Ha az eredeti formulánk igaz volt valamilyen struktúrán, akkor az f_{1}, …, f_{n} függvényjeleket tudjuk úgy interpretáltni, hogy a végső formulánk is igaz legyen; fordítva pedig ha ez utóbbi formula igaz egy struktúrában, akkor ott az előbbi is, hiszen az f_{i} függvény értéke megadja a megfelelő y_{i} változójel értékét.

Végezetül az ezzel kapott formulahalmazban minden formula elejéről az ott álló univerzális kvantorokat lehagyjuk, így kapjuk Γ′′-t. Az előbbiek alapján világos, hogy Γ-nak pontosan akkor van modellje, ha Γ′′-nek.

A Γ′′ elemei tehát kvantormentes formulák, es nem szerepel bennük = jel. Tegyük fel, hogy Γ′′ típusában, amit t′′ fog jelölni, szerepel legalább egy konstansjel, ha nem így volna, vegyünk fel egy tetszőlegeset. Nézzük a t′′-beli függvényjelek segítségével a t′′-beli konstansjelek által generált szabadalgebrát (vagyis a változójel nélküli kifejezések halmazát). Ezt Herbrandt-univerzumnak nevezik. Ha most Γ′′-nek van egyátalán modellje, akkor van olyan modellje is, aminek alaphalmaza a Herbrandt-univerzum, és benne a függvényjelek interpretáltja a természetesen adódó függvény.

Ennek az állításnak egyik fele nyílvánvaló: ha van ilyen modellje, akkor van modellje is. Fordítva: ha van Γ′′-nek egy tetszőleges 𝔄 modellje, akkor a Herbrandt-univerzum beképezhető A-ba: a konstansjelek az interpretáltjukba mennek, a kifejezésekhez rendelt értéket pedig a függvényjelek interpretáltjai mentén számíthatjuk ki (a szabadalgebrát homomorf módon beképezzük egy algebrába). Ennek a leképezésnek a mentén visszahúzzuk a relációk interpretáltjait. Mivel Γ′′ elemeiben sem egyenlőség sem kvantor nem fordul elő, azért ha egy ilyen formula az eredeti modellben minden lehetséges értékelés mellett igaz, akkor az a visszahúzott modellben is minden lehetséges értékelés mellett igaz lesz. Vagyis Γ′′-nek a Herbrandt univerzumon is tudunk modelljét definiálni.

Ezek szerint Γ′′ pontosan akkor kielégíthető, ha tudjuk a relációjeleket úgy interpretálni a H Herbrandtuniverzumon, hogy Γ′′ minden formulája igaz legyen. Legyen r egy n-változós relációjel, k_{1}, …, k_{n} pedig H-nak elemei. Az, hogy r ezeken az elemeken igaz-e vagy sem, lényegében egy itéletváltozó. Legyenek tehát itéletváltozóink éppen ezek: r(k_{1}, …, k_{n}), Γ′′ egy φ elemébe pedig a változójelek helyébe minden lehetséges módon helyettesítsük be H elemeit. Ezzel sok–sok itéletkalkulusbeli formulát kaptunk, és ezek mindegyikének igaznak kell lennie. Tehát az így kapott (most már itéletkalkulusbeli) formulahalmaz pontosan akkor kielégíthető, ha Γ′′-nek, vagyis ha Γ-nak van modellje.

Arra pedig, hogy egy itéletkalkulusbeli formulahalmaz kielégíthető-e, van a rezolúciós módszer. Így ebből a formulahalmazból pontosan akkor vezethető le az üres klóz, ha Γ-nak nincs modellje.

A továbbiakban azt mutatjuk meg, hogy az utóbbi lépést, nevezetesen hogy Γ′′ elemeibe a Herbrandtuniverzum összes elemét be kell helyettesíteni, hogyan kerülhetjük el.

A formulák átalakítását (diszjunktív normál forma, illetve azok szétdarabolása) természetesen helyettesítés nélkül is megtehető. Egy literál alakja ebben az esetben r(k_{1}, …, k_{n}) (vagy ennek negáltja), ahol r egy n-változós relációjel, k_{i} pedig tetszőleges (esetleg változójeleket is tartalmazó) kifejezés. Egy klóz pedig literálok halmaza.

Egy helyettesítés egy x_{1} ← k_{1}, …, x_{s} ← k_{s} sorozat, ami azt jelenti, hogy az x_{i} változójelek helyébe a k_{i} kifejezéseket kell szimultán behelyettesíteni (nem egyesével, hanem egyszerre). Ha σ és τ is egy helyettesítés, akkor σ ∘ τ is egy helyettesítés: először σ-t, azután τ-t hajtjuk végre. A σ ∘ τ-t ki is számíthatjuk.

Legyen c egy klóz (literálhalmaz), a cσ az a klóz, amit c-ből a σ helyettesítés elvégzése után kapunk. A k = ⟨k_{1}, …, k_{n}⟩ és a k^{∗} = ⟨k_{1}^{∗}, …, k_{n}^{∗}⟩ kifejezés sorozatok egyesíthetők, ha van olyan σ helyettesítés, amivel k_{1}σ = k_{1}^{∗}σ, …, k_{n}σ = k_{n}^{∗}σ. Ez a σ a legáltalánosabb egyesítésük, ha tetszőleges τ egyesítésre (vagyis kτ = k^{∗}τ esetén) van olyan τ′, hogy τ = στ′.

Tétel Tetszőleges két kifejezéssorozatra, ha egyesíthető, létezik legáltalánosabb egyesítés, ami ráadásul gyorsan ki is számítható.

Bizonyítás Nézzük a sorozatok első elemét: k_{1} illetve k_{1}^{∗}. Következő lehetőségek vannak: egyik sem változójel, az egyik változójel, illetve mindkettő változójel.

Az első esetben k_{1} és k_{1}^{∗} alakja f(k_{11}, …, k_{1m}) illetve f^{∗}(k_{11}^{∗}, …, k_{1m}^{∗}). Ha f és f^{∗} különböző függvényjelek, akkor a két sorozat nem egyesíthető. Ha f és f^{∗} ugyanaz a függvényjel, akkor a sorozatok elejéről a k_{1}-et illetve k_{1}^{∗}-et kitöröljük, és a végére odaillesztjük a k_{11}, …, k_{1m} illetve k_{11}^{∗}, …, k_{1m}^{∗} kifejezéseket.

Másik esetünk ha a k_{1} és k_{1}^{∗} küzül az egyik, mondjuk k_{1} változójel. Ha most k_{1}^{∗} is változójel, akkor az egyiket megtartjuk, és a másikat a saját sorozatában helyettesítjük az egyikkel. Ezzel k_{1} és k_{1}^{∗} azonos, őket a sorozatból ki is törölhetjük.

Ha k_{1}^{∗} nem változójel, akkor benne k_{1} nem fordulhat elő. Ha mégis, akkor a két sorozat nem egyesíthető (k_{1} és k_{1}^{∗} semmilyen helyettesítés után sem lehet egyforma). Ha k_{1} nem fordul elő k_{1}^{∗}-ben, akkor a legáltalánosabb helyettesítés k_{1} ← k_{1}^{∗} lesz, ezt a k sorozatban végigvezetjük, ami által a sorozatok első elemei egyformák lesznek, tehát őket el lehet hagyni. QED

Definíció Legyen c_{1} és c_{2} két (nem feltétlenül különböző) klóz, ℓ_{1} egy c_{1}-beli literál, és ¬ℓ_{2} ∈ c_{2}. Az általános rezolúciós lépés a következő. Először is változtassuk meg c_{2}-ben (és ezzel együtt ℓ_{2}-ben is) az összes változójelet úgy, hogy azok diszjunktak legyenek a c_{1}-ben használt változójelektől. Ha ezek után ℓ_{1} és ℓ_{2} nem egyesíthető, a rezolúciós lépés nem alkalmazható. Ha igen, legyen σ a legáltalánosabb egyesítésük, ekkor a rezolvensük:

R(c_{1}, c_{2}, ℓ_{1}, ℓ_{2}) = (c_{1}σ − {ℓ_{1}σ}) ∪ (c_{2}σ − {¬ℓ_{2}σ}).

Szükségünk lesz még egy átalakításra, az úgynevezett faktorizációra. Legyen c egy klóz, és ℓ_{1} valamint ℓ_{2} két egyesíthető literál c-ben. A c-nek ℓ_{1} és ℓ_{2} szerinti faktora

F (c, ℓ_{1}, ℓ_{2}) = cσ − {ℓ_{1}σ},

ahol σ az ℓ_{1} és ℓ_{2} legáltalánosabb egyesítése.

Tétel Egy klózhalmaz akkor és csak akkor nem elégíthető ki a Herbrandt-univerzumon, ha belőlük az üres klóz rezolúcióval és faktorizációval levezethető.

Bizonyítás Egy klóz kielégíthető, ha a változójelek tetszőleges értékelés mellett benne valamelyik literál igaz lesz. Jól látszik, hogy ha c_{1} és c_{2} is kielégíthető, akkor rezolvensük és faktorjaik is. Ezért ha a klózhalmaz kielégíthető, akkor nem vezethető le belőle az üres klóz.

Fordítva, ha a klózhalmaz nem kielégíthető, akkor az összes klózból az összes helyettesítéssel kapott “itéletváltozós” klózokból az üres klóz levezethető. A helyettesített klózokon való levezetés imitálható a következőképpen: ha a rezolúciós lépésben részt vevő egyik klóz c_{1}σ_{1}, a másik c_{2}σ_{2}, akkor van olyan ℓ_{1} ∈ c_{1}, ¬ℓ_{2} ∈ c_{2}, és σ helyettesítés, hogy a lépés eredménye éppen R(c_{1}, c_{2}, ℓ_{1}, ℓ_{2})σ egy faktora.

Ha ezt megmutattuk, készen vagyunk, ugyanis helyettesítés és faktorizáció után üres klózt csak az üres klózból kaphatunk.

A fenti, úgynevezett “emelési lemma” bizonyítása egyszerű: ℓ_{1} ∈ c_{1} és ¬ℓ_{2} ∈ c_{2} azok, amikre ℓ_{1}σ_{1} = ℓ_{2}σ_{2} az a literál, amivel a c_{1}σ_{1} és c_{2}σ_{2} klózokra a rezolúciós lépést alkalmaztuk. Ha c_{2}-ben az összes változót átnevezzük, akkor a σ_{1} és σ_{2} helyettesítéseket kicserélhetjük a σ′ uniójukra; ez a σ′ egyesíti ℓ_{1}-et és ℓ_{2}-t. Ezért ez a két literál egyesíthető, következésképp van legáltalánosabb egyesítésük is, ami legyen τ, és σ′ = τ ∘ σ. Ezek után R(c_{1}, c_{2}, ℓ_{1}, ℓ_{2})-re alkalmazva a σ helyettesítést, éppen R(c_{1}σ_{1}, c_{2}σ_{2}, ℓ_{1}σ_{1})-et kapjuk.

Persze nem egészen. Előfordulhat ugyanis, hogy ez utóbbiban ugyanaz az itéletváltozós literál mind c_{1}σ_{1}-ben, mind c_{2}σ_{2}-ben szerepel, ezért a rezolvensben (mind halmazelméleti unióban) ez csak egyszer lesz. Ugyanakkor R(c_{1}, c_{2}, ℓ_{1}, ℓ_{2})σ-ban ugyanaz a literál kétszer fog szerepelni. A két literált éppen egy faktorizációval ejthetjük össze. QED