Ugrás a tartalomhoz

A matematikai logika alkalmazásszemléletű tárgyalása

Pásztorné Varga Katalin, Várterész Magda, Sági Gábor

Panem Kft.

A tablók módszere – tablókalkulus

A tablók módszere – tablókalkulus

A tablók módszerét (tablókalkulust vagy analitikus táblázat módszerét) mint automatikus tételbizonyítási eszközt az 1960-as évek végén Smullyan vezette be ([60]). A módszerhez kapcsolható szemantikus eldöntésprobléma (hasonlóan a rezolúciós kalkulushoz) az {A1,A2,,An} formulahalmaz és egy B formula esetén a

  1. ¬ ( A 1 A 2 A n 1 A n B ) formula,

  2. { A 1 , A 2 , , A n , ¬ B } formulahalmaz

kielégíthetetlenségének igazolása.

Később látni fogjuk, hogy a tablókalkulus nem véges formulahalmaz esetén is alkalmazható. A tablók módszere nem követeli meg sem a formulák speciális alakra hozását, sem a logikai összekötőjelek és a kvantorok használatának korlátozását.

Előkészítő fogalmak, ítéletlogika

6.4.1. DEFINÍCIÓ. Legyen 0 az ítéletlogika nyelve, 0 egy interpretációja. Nevezzük igazhalmazának0 azon formuláinak a halmazát, amelyek -ben igazak.

Egy interpretáció és az interpretáció S igazhalmaza kölcsönösen meghatározzák egymást. Így nem meglepő, hogy a formulák szemantikus tulajdonságai megfogalmazhatók az igazhalmaz segítségével is. Egy ítéletlogikai formula tautológia, ha minden igazhalmaznak eleme, kielégíthetetlen, ha egyetlen igazhalmaznak sem eleme, kielégíthető, ha van olyan igazhalmaz, amelynek eleme.

6.4.2. DEFINÍCIÓ. Legyen S ítéletlogikai formulák egy halmaza. Stelített[11]formulahalmaz, ha rendelkezik az alábbi tulajdonságokkal:

  1. ¬ A S akkor és csak akkor, ha AS. Más szóval A,¬A formulapár pontosan egyike eleme S-nek.

  2. A B S akkor és csak akkor, ha AS és BS.

  3. A B S akkor és csak akkor, ha AS vagy BS.

  4. A B S akkor és csak akkor, ha AS vagy BS.

Az olvasóra bízzuk az alábbi lemma belátását:

6.4.3. LEMMA. Egy S formulahalmaz pontosan akkor igazhalmaz, ha telített.

6.4.4. DEFINÍCIÓ. Vezessünk be az ítéletlogika nyelvébe két új szimbólumot: a T-t és az F-et. Ha A egy ítéletlogikai formula, eléírva a T-t vagy az F-et jelölt formulát nyerünk belőle. Tehát TA és FA jelölt formulák. Egy interpretációban TA igaz, ha A igaz és TA hamis, ha A hamis. Továbbá FA igaz, ha A hamis és FA hamis, ha A igaz.

Table 6.15. Jelölt és ,,jelöletlen” formulapárok igazságtáblája

1.

2.

3.

4.

5.

6.

A

B

A B

¬ ( A B )

¬ ( A B )

¬ ( A B )

A B

A B

TA B

FA B

FA B

FA B

TA B

TA B

i

i

i

h

h

h

i

i

i

h

h

h

i

i

i

h

h

i

h

h

h

i

i

i

h

h

h

i

h

i

h

i


A jelölt formulák használata az igazságértékelés (4.2.8. definíció) folyamatában kényelmes lesz, mivel ha azt akarjuk megtudni, hogy egy formula milyen feltételek mellett igaz vagy hamis a φAi és φAh feltételek helyett rendre a TA és az FA jelölt formulát használhatjuk.

6.4.5. PÉLDA. Adott a (X(YZ))(XY)(XZ) formula. Keressük azokat az igazságértékeléseket, amelyek hamissá teszik a formulát.

φ ( ( X ( Y Z ) ) ( X Y ) ( X Z ) ) h

alapján áll elő.

Figure 6.16.  φ ( ( X ( Y Z ) ) ( X Y ) ( X Z ) ) h igazságértékelés-fája

φ ( ( X ∨ ( Y ∧ Z ) ) ⊃ ( X ∨ Y ) ∧ ( X ∨ Z ) ) h igazságértékelés-fája

A formula hamissá válásához kapott négy feltételcsoport:

1.

φ X i

φ X h

φ Y h

2.

φ X i

φ X h

φ Z h

3.

φ Y i

φ Z i

φ X h

φ Y h

4.

φ Y i

φ Z i

φ X h

φ Z h

  1. Ezután mutassuk meg ugyanezt az igazságértékelést jelölt formulával. Az igazságértékelés-fa az

F ( X ( Y Z ) ) ( X Y ) ( X Z )

szerkezeti fája alapján az alábbi ábrán látható.

Figure 6.17.  F ( X ( Y Z ) ) ( X Y ) ( X Z ) igazságértékelés-fája

F ( X ∨ ( Y ∧ Z ) ) ⊃ ( X ∨ Y ) ∧ ( X ∨ Z ) igazságértékelés-fája

A formula hamissá válásához kapott négy feltételcsoport:

1.

T X

F X

F Y

2.

T X

F X

F Z

3.

T Y

T Z

F X

F Y

4.

T Y

T Z

F X

F Z

  1. Az igazságértékelést ,,jelöletlen” formulával úgy is elvégezhetjük, hogy alapértelmezés szerint mindig a gyökérbeli formula igazzá válási feltételeit keressük az igazságértékelés-fával. Ennek megfelelően az igazságértékelés-fát a

¬ ( ( X ( Y Z ) ) ( X Y ) ( X Z ) )

formula alapján állítjuk elő (6.18. ábra).

Figure 6.18.  ¬ ( ( X ( Y Z ) ) ( X Y ) ( X Z ) ) igazságértékelés-fája

¬ ( ( X ∨ ( Y ∧ Z ) ) ⊃ ( X ∨ Y ) ∧ ( X ∨ Z ) ) igazságértékelés-fája

A hamissá váláshoz kapott négy feltételcsoport:

1.

X

¬ X

¬ Y

2.

X

¬ X

¬ Z

3.

Y

Z

¬ X

¬ Y

4.

Y

Z

¬ X

¬ Z

A feltételek egyike sem teljesíthető, tehát a (X(YZ))(XY)(XZ) formula tautológia.

Figyeljük meg a 6.15. táblázatban, hogy az AB, ¬(AB), ¬(AB) formulák (1–3. oszlop) egyetlen igazságkiértékelésre veszik fel az igaz értéket, tehát az igazzá válásuk a két közvetlen részformulára együttesen megadott feltételtől függ. A ¬(AB), AB, AB formulák (4–6. oszlop) három igazságkiértékelésre veszik fel az igaz értéket, tehát az igazzá válásuk a két közvetlen részformulára egymástól függetlenül megadott feltételektől függ.

Az 1–3. oszlopokban lévő ,,jelöletlen” formulákat α-típusú, a 4–6. oszlopokban lévő ,,jelöletlen” formulákat β-típusú formuláknak nevezzük. Az α-típusú formulák átalakíthatók α1α2 alakú ,,jelöletlen” formulává, a β-típusú formulák átalakíthatók β1β2 alakú ,,jelöletlen” formulává. α1 és α2 az α-típusú, β1 és β2 a β-típusú formulák közvetlen részformulái. Ezek nem mindig a formulák eredeti közvetlen részformulái. Például a ¬(AB) formula közvetlen részformulája AB, de mint α-típusú formulának ¬A és ¬B a két közvetlen részformulája. Az alábbi táblázat mutatja az α-típusú és β-típusú formulákhoz tartozó α1,α2 és β1,β2 közvetlen részformulákat.

Table 6.19. Az α- és β-formulák közvetlen részformulái

α

α 1

α 2

β

β 1

β 2

A B

A

B

¬ ( A B )

¬ A

¬ B

¬ ( A B )

¬ A

¬ B

A B

A

B

¬ ( A B )

A

¬ B

A B

¬ A

B


A táblázat alapján nyilvánvaló, hogy tetszőleges interpretációban egy α-formula pontosan akkor igaz, ha α1 is, és α2 is igaz, egy β-formula pontosan akkor igaz, ha vagy β1 igaz, vagy β2 igaz. Az olvasóra bízzuk a 6.4.3. lemma átfogalmazásának belátását is:

6.4.6. LEMMA.

Egy S formulahalmaz pontosan akkor igazhalmaz, ha tetszőleges A formulára és α-, valamint β-típusú formulákra a következő tulajdonságokkal bír:

  1. Az A és ¬A formulák közül pontosan az egyik eleme S-nek, azaz ¬AS akkor és csak akkor, ha AS.

  2. α S akkor és csak akkor, ha α1S és α2S.

  3. β S akkor és csak akkor, ha β1S vagy β2S.

6.4.7. DEFINÍCIÓ. Legyen S ítéletlogikai formulák tetszőleges halmaza.

  1. S lefele zárt, ha minden olyan esetben, amikor

    1. α S , akkor α1S és α2S és

    2. β S , akkor β1S vagy β2S.

  2. S felfele zárt, ha minden olyan esetben, amikor

    1. α 1 S és α2S, akkor αS és

    2. β 1 S vagy β2S, akkor βS.

6.4.8. DEFINÍCIÓ. Ítéletlogikai formulák egy S halmaza Hintikka-halmaz, ha S lefele zárt és nem tartalmazza egyetlen formulája esetén sem annak negáltját is, azaz S a következő tulajdonságokkal rendelkezik:

H 0: Ha az A és ¬A formulák közül az egyik eleme S-nek, akkor a másik nem eleme S-nek. Más szóval ha ¬AS, akkor AS, és ha AS, akkor ¬AS.

H 1: Ha αS, akkor α1S és α2S.

H 2: Ha βS, akkor β1S vagy β2S.

Könnyen meg lehet mutatni, hogy az olyan lefele zárt formulahalmaz, amely teljesíti a H0 feltételt is, mindig igazhalmaz. Az olyan felfele zárt formulahalmaz, amely teljesíti a H0 feltételt is, szintén igazhalmaz.

Vessük össze az igazhalmaz és a maximális konzisztens formulahalmaz(6.1.29. és 6.1.30. tételek) tulajdonságait. Ebből következik, hogy ítéletlogikai formulák egy halmaza pontosan akkor maximális konzisztens, ha igazhalmaz.

6.4.9. TÉTEL. Ha S Hintikka-halmaz, akkor kielégíthető.

BIZONYÍTÁS. Az S Hintikka-halmaz lefele zárt, tehát tartalmaz literálokat, de nem tartalmaz komplemens literálpárt. Legyen e tetszőlegesen rögzített igazságérték. Legyen az interpretáció a következő:

( X ) { i ha T X S vagy F ¬ X S , h ha F X S vagy T ¬ X S , e egyébként .

A szerkezeti indukció elvének segítségével megmutatjuk, hogy tetszőleges AS formulára (A)=i.

(alaplépés:) Jelölt ítéletváltozókra definíciója miatt nyilvánvaló, hogy igaz az állítás.

(indukciós lépések:)

  • Legyen Aα-formula, közvetlen részformulái α1 és α2. Mivel AS, így α1S és α2S. Indukciós feltevésünk, hogy (α1)=i és (α2)=i. De mivel α=α1α2, ezért (α)=i.

  • Legyen Aβ-formula, közvetlen részformulái β1 és β2. Mivel AS, ezért β1S vagy β2S. Tegyük fel, hogy (β1)=i vagy (β2)=i. De mivel β=β1β2, ezért (β)=i.

Ezzel a tételt bebizonyítottuk.

Analitikus és jelölt tabló az ítéletlogikában

A tablók módszerében (mint kalkulusban) minden ,,formulafajtára” (negációs, konjunkciós, diszjunkciós, implikációs, illetve α-típusú, β-típusú) van egy-egy levezetési szabály. A levezetési szabályt a formula közvetlen tablójának is nevezik. Az alábbiakban felsoroljuk ,,jelöletlen” és jelölt formulákra, valamint az α-, β-formulákra a közvetlen tablókat:

Figure 6.20. Közvetlen tablók ,,jelöletlen” és α-, β-formulákra

Közvetlen tablók ,,jelöletlen” és α-, β-formulákra

6.4.10. DEFINÍCIÓ. Egy C ítéletlogikai formula analitikus tablója egy olyan bináris fa, melynek csúcsai ,,jelöletlen” ítéletlogikai formulák. A fa gyökere a C formula. Előállítjuk C közvetlen tablóját a 34. táblázat alapján. Tegyük fel, hogy C-nek egy T tablója adott. Legyen T-ben D egy levélcsúcs. Ekkor a T tabló közvetlen kiterjesztése a következő lehet:

  1. Ha van még nem ,,feldolgozott” α-formula a gyökérből a D csúcsba vezető úton, akkor kapcsoljuk D-hez rendre ezen út folytatásaként az α formula közvetlen tablója szerint nyert α1 és α2 formulákat mint új csúcsokat.

  2. Ha van még nem ,,feldolgozott” β-formula a gyökérből a D csúcsba vezető úton, akkor D-ben elágazik a tabló, és a bal oldali rákövetkező csúcsba β közvetlen tablójából β1, a jobb oldali rákövetkezőbe pedig β2 kerül.

  1. Ha van ¬¬A alakú nem ,,feldolgozott” formula a gyökérből a D csúcsba vezető úton, akkor D-hez kapcsoljuk ezen út folytatásaként az A formulát tartalmazó új csúcsot.

Figure 6.21. Közvetlen tablók jelölt formulákra

Közvetlen tablók jelölt formulákra

6.4.11. MEGJEGYZÉS. Az analitikus tabló előállítása során tehát kiindulunk egy formulából. A formula tablóját közvetlen kiterjesztésekkel kapjuk meg. A közvetlen kiterjesztéseket pedig a közvetlen tablók alapján nyerjük. Ha adott két analitikus tabló, T1 és T2, a T2 tablót T1 közvetlen kiterjesztésének nevezzük, ha T2-t a T1-ből az (A) vagy a (B) szabályok valamelyikének alkalmazásával kaptuk meg. Tehát egy C formula tablója T, ha van olyan T1,T2,,Tn=T véges tablósorozat, ahol T1 egy egyetlen, a C csúcsból álló fa, és minden i=1,2,,n1-re Ti+1 közvetlen kiterjesztése a Ti-nek.

6.4.12. PÉLDA. Tekintsük most a 6.4.5. példabeli

¬ ( ( X ( Y Z ) ) ( X Y ) ( X Z ) )

formula ,,jelöletlen” tablóját (6.22. ábra). Hasonlítsuk össze a tablót a 6.18. ábrabeli igazságértékelés-fával, nyilvánvaló az egyezés.

Figure 06.22.  ¬ ( ( X ( Y Z ) ) ( X Y ) ( X Z ) ) analitikus tablója

¬ ( ( X ∨ ( Y ∧ Z ) ) ⊃ ( X ∨ Y ) ∧ ( X ∨ Z ) ) analitikus tablója

6.4.13. DEFINÍCIÓ. Egy C formula jelölt tablója egy olyan bináris fa, amelynek csúcsai jelölt formulák. A gyökérbe elhelyezzük a C jelölt formulát. Előállítjuk C közvetlen tablóját a 6.21. táblázatbeli közvetlen tablók alapján. Feltesszük, hogy a C-nek egy T tablója adott. Legyen T-ben D egy levélcsúcs. Ekkor a T tabló közvetlen kiterjesztése a következő:

  1. Ha van még nem ,,feldolgozott” TAB, FAB vagy FAB alakú jelölt formula a gyökérből a D csúcsba vezető úton, akkor kapcsoljuk D-hez ezen út folytatásaként a megfelelő formula közvetlen tablójából nyert jelölt formulákat mint új csúcsokat. Azaz két egymást követő csúcsot illesztünk a tablóhoz.

  2. Ha van még nem ,,feldolgozott” FAB, TAB vagy TAB alakú jelölt formula a gyökérből a D csúcsba vezető úton, akkor D-hez kapcsoljunk két csúcsot: a bal oldali a megfelelő formula közvetlen tablójából nyert egyik, a jobb oldali pedig a másik jelölt formula.

  1. Ha van még nem ,,feldolgozott” T¬A vagy F¬A alakú jelölt formula a gyökérből a D csúcsba vezető úton, akkor kapcsoljuk D-hez ezen út folytatásaként a megfelelő formula közvetlen tablójából nyert jelölt formulát mint új csúcsot.

6.4.14. PÉLDA. Adjuk meg most a 6.4.5. példabeli

F ( X ( Y Z ) ) ( X Y ) ( X Z )

formula jelölt tablóját (6.23. ábra). Összevetve a tablót a 6.17. ábrán lévő igazságértékelés-fával az egyezés most is világos.

Figure 6.23.  F ( X ( Y Z ) ) ( X Y ) ( X Z ) jelölt tablója

F ( X ∨ ( Y ∧ Z ) ) ⊃ ( X ∨ Y ) ∧ ( X ∨ Z ) jelölt tablója

A tabló egy ága teljes, ha az ágon lévő fel nem dolgozott formulák literálok. A tabló teljes, ha minden ága teljes. A tabló egy ága zárt, ha az ágon egy formula és a formula negáltja is előfordul. A tabló zárt, ha minden ága zárt, egyébként a tabló nyitott.

A tablók módszere a vizsgált formula teljes tablójának felépítésére alkalmas algoritmus. Az algoritmus megállási feltétele, azaz a tablókalkulus eldöntésproblémája: ,,lezárható-e a formula tablója”. Azt mondjuk, hogy az A formulának létezik tablócáfolata, ha a tablója zárt, vagy hogy a B formula bizonyítható tablóval, ha ¬B tablója zárt.

A formulák feldolgozási sorrendje a tablóban nem kötött, így a tabló mérete nem meghatározott. Célszerű először az α típusú, és csak ha ilyen éppen nincs, akkor a β típusú formulákat feldolgozni, így a tabló szélessége jelentősen csökkenhet. Ezt illusztrálja az F(X(YZ))(XY)(XZ) jelölt formulának a 6.24. és 6.25. ábrákon látható két tablója.

Figure 6.24. A jelölt formulák feldolgozása a tablóba kerülés sorrendjében

A jelölt formulák feldolgozása a tablóba kerülés sorrendjében

Legyen T egy tabló, T egy ága Θ és a Θ ágon lévő formulákban előforduló ítéletváltozók egy interpretációja. Azt mondjuk, hogy a Θág igaz-ben, ha Θ minden formulája igaz az -ben. A Ttabló igaz-ben, ha legalább egy ága igaz -ben.

Legyen az A formula tablója T, és legyen az A formula egy interpretációja. Ha az A formula -beli igazságértéke i, akkor A közvetlen tablója is igaz -ben. Ha a T tabló igaz -ben, akkor a tabló T közvetlen kiterjesztése is igaz -ben. Tegyük fel ugyanis, hogy a közvetlen kiterjesztés egy igaz ágat érint. (Ha nem igaz ágat érintene, a T-beli igaz ág nyilván T-ben is igaz ág, így T igaz tabló.)

Figure 6.25. A jelölt formulák feldolgozása ,,α-típus előbb” stratégiával

A jelölt formulák feldolgozása ,,α-típus előbb” stratégiával

  • Ha α-típusú formulát dolgoztunk fel az igaz ágon, akkor az ág α1 és α2-vel bővül. De α igaz volt -ben, ezért az α1 és α2 is igaz lesz. Tehát az ág igaz marad.

  • Ha β-típusú formulát dolgoztunk fel az igaz ágon, akkor az elágazásnál egyik ágra β1, a másik ágra â2 kerül. β igaz -ben, ezért β1 és β2 közül legalább az egyik igaz -ben. Ez azt jelenti, hogy legalább az egyik ág igaz ág lesz.

  • Ha ¬¬A alakú formulát dolgoztunk fel az igaz ágon, akkor az ág A-val bővül. Mivel ¬¬A igaz, így A is igaz -ben.

Abból, hogy egy igaz tabló minden közvetlen kiterjesztése igaz, következik, hogy ha a gyökérben lévő A formula igaz -ben, akkor az A formula T tablója is igaz -ben.

6.4.15. TÉTEL. (A TABLÓKALKULUS HELYESSÉGE.)

Ha az A formula tablója zárt, akkor A kielégíthetetlen.

BIZONYÍTÁS. Ha egy T tabló zárt, akkor minden ága zárt. Nyilvánvaló, hogy ha egy tabló valamely ága zárt, az az ág egyetlen interpretációban sem lehet igaz, hisz tartalmaz olyan formulát, melynek negáltja is az ág formulája. Tehát T egyetlen ága egyetlen interpretációban sem lehet igaz. Tegyük fel, hogy az A formula tablója zárt. Ha A kielégíthető, lenne olyan interpretáció, melyben igaz, de akkor ebben az interpretációban a tablója is igaz. Viszont A tablója zárt, tehát nem lehet egyetlen interpretációban sem igaz ága, így nem lehet maga a tabló sem igaz, azaz A csak kielégíthetetlen lehet.

6.4.16. TÉTEL. Egy tabló bármely teljes, nyitott ága kielégíthető.

BIZONYÍTÁS. Legyen Θ egy T tabló teljes, nyitott ága. Legyen S az ágon lévő összes formula halmaza. Egyszerű belátni, hogy S teljesíti a következő három feltételt:

H 0: Nincs olyan X ítéletváltozó, hogy X is, és ¬X is egyszerre eleme lenne S-nek.

H 1: Ha αS, akkor α1S és α2S.

H 2: Ha βS, akkor β1S vagy β2S.

Tehát S Hintikka-halmaz. A 6.4.9. tétel szerint a Hintikka-halmazok kielégíthetők, tehát S kielégíthető.

6.4.17. TÉTEL. (A TABLÓKALKULUS TELJESSÉGE.)

Ha egy A formula kielégíthetetlen, akkor bármely teljes tablója zárt.

BIZONYÍTÁS. Tegyük fel, hogy T az A formula egy teljes tablója. Ha T nyitott, akkor A kielégíthető (6.4.16. tétel). Ezért ha A kielégíthetetlen, akkor T biztosan zárt.

Másképp fogalmazva a teljesség a tablókalkulus esetében azt jelenti, hogy tetszőleges tautológia bizonyítható tablóval.

A tablók módszerének alkalmazásai

A tabló fogalmát egy formula esetére definiáltuk. Most kiterjesztjük a tabló fogalmát formulahalmazokra is. Egy {C1,C2,,Cn}véges formulahalmaz tablója gyökerében a formulahalmaz minden formulája szerepel. Ezután a C1 teljes tablóját a gyökérhez kapcsoljuk. A nyitott ágakat a C2 teljes tablójával folytatjuk és így tovább. Egy {C1,C2,}megszámlálhatóan végtelen formulahalmaz tablója gyökerében a formulahalmaz minden formulája szerepel. Ezután az előbbi módszerrel definiáljuk a formulahalmaz tablóját.

A kompaktsági probléma

Legyen S megszámlálható formulahalmaz. Azt mondtuk, hogy egy interpretáció kielégíti S-t, ha az interpretációban S minden eleme igaz. Továbbá S kielégíthető, ha legalább egy interpretáció kielégíti. Vizsgáljuk meg a következő kérdést: ,,abból, hogy S minden véges részhalmaza kielégíthető, következik-e, hogy S is kielégíthető”.

A kérdést többféleképpen átfogalmazhatjuk:

  • Rendezzük S elemeit egy A1,A2, megszámlálható hosszúságú sorozatba. Az az állítás, hogy S minden véges részhalmaza kielégíthető, ekvivalens azzal, hogy minden n=1,2, esetén a sorozat A1,A2,,An kezdőszeletében szereplő formulák halmaza kielégíthető. Ugyanis, ha S minden véges részhalmaza kielégíthető, akkor nyilván minden n-re {A1,A2,,An} is kielégíthető. Ha pedig azt tesszük fel, hogy minden n-re {A1,A2,,An} kielégíthető, akkor mivel S-nek egy tetszőleges S0 részhalmaza valamilyen n-re részhalmaza {A1,A2,,An}-nek, így S0 kielégíthető.

  • Tegyük fel, hogy van olyan 1 interpretáció, amelyben A1 igaz, és van olyan 2 interpretáció, amelyben A1 is, és A2 is igaz (a két interpretáció nem feltétlenül egyezik meg). Tegyük fel továbbá, hogy minden n-re van olyan n interpretáció, amelyben az első n formula mind igaz. Vajon létezik-e ekkor olyan interpretáció is, amelyben az összes Ai igaz.

  • Nevezzünk a továbbiakban egy S megszámlálható formulahalmazt konzisztensnek, ha S minden véges részhalmaza kielégíthető (ez ekvivalens azzal, hogy S tablója nem lesz zárt, azaz nincs olyan n, hogy {A1,A2,,An} tablója zárt lenne). Ha S véges, akkor S pontosan akkor kielégíthető, ha konzisztens. Vajon egy megszámlálható konzisztens formulahalmaz biztosan kielégíthető-e, avagy ha az S megszámlálható formulahalmaz tablója nem zárt, akkor biztosan létezik-e egy interpretáció, amelyben S minden eleme igaz.

6.4.18. LEMMA. (KÖNIG LEMMÁJA.) Minden végesen generált fa, amelyben a csúcsok száma végtelen, tartalmaz legalább egy végtelen ágat.

BIZONYÍTÁS. Legyen T egy végesen generált végtelen fa, azaz T-nek végtelen sok csúcsa van, de minden csúcsának csak véges sok gyermeke. Nevezzük T egy csúcsát ,,jónak”, ha végtelen sok utódja van. A gyökér mint csúcs jó, hiszen a fa összes többi csúcsa utódja. Legyen a gyökér t0 és legyen t0,t1,,tn jó csúcsokból álló véges ág. A tn csúcs gyermekei között van legalább egy jó csúcs (különben tn sem lenne jó). Legyen tn+1 a tn egy jó gyermeke. Ily módon folytatva t0,t1,,tn,tn+1, egy végtelen ág.

6.4.19. TÉTEL. (KOMPAKTSÁGI TÉTEL.) Ha az S megszámlálható formulahalmaz minden véges részhalmaza kielégíthető, akkor S kielégíthető.

BIZONYÍTÁS. Rendezzük az S formulahalmaz formuláit egy A1,A2, sorozatba. Tegyük fel, hogy {A1,A2,,An} minden n-re kielégíthető. Állítsuk elő A1 teljes tablóját. Ez a tabló nem zárt, mivel A1 kielégíthető. Ezután kapcsoljuk hozzá minden nyitott ághoz A2 tablóját. Ebben az esetben is lesz legalább egy nyitott ága a tablónak, mivel {A1,A2} kielégíthető. Folytassuk az A3 tablójának, majd az A4,A5, tablójának a nyitott ágakhoz való kapcsolásával. A kapott tabló mindig nyitott lesz a feltétel miatt. Ily módon egy végtelen fát kapunk. Mivel a tabló végesen generált fa, König lemmája miatt van legalább egy végtelen nyitott ága, legyen ez Θ. Világos, hogy Θ tartalmaz minden Ai-t és a Θ ágban szereplő formulák halmaza Hintikka-halmaz, amely tartalmazza S-t is. A 6.4.9. tétel szerint ez a halmaz kielégíthető, valamint kielégíthető S is, mint az ő részhalmaza.

6.4.20. MEGJEGYZÉS. A kompaktsági tétel nyilván megfordítható: ha az S formulahalmaz kielégíthető, akkor minden véges részhalmaza is az. Továbbá a kompaktsági tétel igaz marad megszámlálhatónál nagyobb számosságú formulahalmazra is.

A kielégíthetőség mint tulajdonság a megszámlálható formulahalmaz véges részhalmazairól öröklődik a teljes formulahalmazra és annak összes részhalmazára. Az ilyen tulajdonságot véges jellegű tulajdonságnak nevezik. Miután egy véges formulahalmaz pontosan akkor elégíthető ki, ha konzisztens, a konzisztencia is véges jellegű tulajdonság. A 6.1.31. tétel kimondja, hogy tetszőleges konzisztens formulahalmaz kiterjeszthető maximális konzisztens formulahalmazzá. Az ott bemutatott – Lindenbaum nevéhez fűződő – konstrukciós bizonyításban fontos tény, hogy az ítéletlogikai formulák halmaza megszámlálható számosságú.

Mint ismeretes, a halmazelméletben a kiválasztási függvények létét a halmazelmélet többi axiómái alapján nem lehetett bebizonyítani. Ezért kiválasztási axióma néven a halmazelmélet axiómái közé sorolták, hogy minden nemüres halmazrendszerhez létezik kiválasztási függvény. Az eredeti problémára sok ekvivalens átfogalmazás ismert. Ezek közül egyik a Tukey-lemma, amely kimondja, hogy tetszőleges H halmaz és H részhalmazaihoz rendelhető T véges jellegű tulajdonság esetén H tetszőleges T tulajdonságú részhalmaza kiterjeszthető maximális T tulajdonságú halmazzá. A lemma megszámlálható esetre bizonyítható be a kiválasztási axióma nélkül.

6.4.21. LEMMA. (TUKEY-LEMMA MEGSZÁMLÁLHATÓ HALMAZRA.)

Legyen H megszámlálható halmaz és T a H részhalmazaihoz rendelhető véges jellegű tulajdonság. Ha S a H halmaz T tulajdonságú részhalmaza, akkor S kiterjeszthető H-nak maximális T tulajdonságú részhalmazává.

BIZONYÍTÁS. Rendezzük H elemeit egy megszámlálható h1,h2, sorozatba. Ezután állítsuk elő az S0,S1, megszámlálható halmazsorozatot a következő módon. Legyen S0=S, és minden i=1,2,-re ha Si1-et már megkonstruáltuk, akkor

S i { S i 1 { h i } , ha S i 1 { h i } T tulajdonságú , S i 1 egyébként .

Világos, hogy az S0S1 halmazlánc minden eleme T tulajdonságú. Legyen M az összes Si uniója. M az S0 kiterjesztése. Belátjuk, hogy M maximális T tulajdonságú halmaz.

  • Lássuk be először, hogy M rendelkezik a T tulajdonsággal. Tekintsük M egy K véges részhalmazát. Ez a konstrukció miatt részhalmaza valamelyik Si-nek. Mivel SiT tulajdonságú, K is az. Emiatt M minden véges K részhalmaza T tulajdonságú, tehát M is T tulajdonságú.

  • Lássuk be ezután, hogy M maximális. Bővítsük ki M-et hi-vel úgy, hogy M{hi} rendelkezzen a T tulajdonsággal. Mivel M{hi} rendelkezik a T tulajdonsággal, így Si=Si1{hi} is T tulajdonságú, és ezért a konstrukció miatt hiM.

Ezzel a Tukey-lemmát bebizonyítottuk.

A lemmából egyszerűen adódik, hogy egy konzisztens formulahalmaz kiterjeszthető maximális konzisztens formulahalmazzá.

Az inkonzisztencia és a kielégíthetetlenség problémája

Az ítéletkalkulus tárgyalásánál bebizonyítottuk, hogy ha egy S formulahalmaz inkonzisztens, akkor kielégíthetetlen (6.1.23. tétel). A fordított állítást, miszerint ha az S formulahalmaz kielégíthetetlen, akkor inkonzisztens, a rendelkezésre álló eszközökkel nem lehetett bizonyítani. A kompaktsági tétel miatt egy S formulahalmaz akkor és csak akkor kielégíthetetlen, ha van véges, kielégíthetetlen részhalmaza. A következő tétel lehetővé teszi annak belátását, hogy ha S kielégíthetetlen, akkor inkonzisztens is.

6.4.22. TÉTEL.

Minden véges, kielégíthetetlen S formulahalmaz inkonzisztens.

BIZONYÍTÁS. Ha az S kielégíthetetlen, akkor van zárt tablója. Ezen zárt tabló mélysége szerinti indukcióval bizonyítjuk a tételt.

  1. Ha a tablónak csak egyetlen csúcsa van, az maga az S formulahalmaz. Ekkor kell lennie olyan X (prím)formulának, amelyre XS, és ¬XS, tehát S inkonzisztens.

  2. Most tegyük fel, hogy ha S zárt tablója legfeljebb n mélységű, akkor S inkonzisztens.

  3. Legyen S zárt tablója n+1 mélységű. Vizsgáljuk meg a tabló gyökerének közvetlen kiterjesztését. A következő esetek lehetségesek:

  1. A ¬¬BS formulára vonatkozó közvetlen tabló alapján terjesztettük ki a gyökeret. Ekkor a tabló így kezdődik:

Ha ebben a tablóban összevonjuk a két első csúcsot, akkor megkapjuk az S{B} tablóját, amelynek mélysége n. Az indukciós feltevés miatt ekkor S{B} inkonzisztens. A 6.1.22. tétel szerint ekkor S0¬B. Viszont ¬¬BS, tehát S inkonzisztens.

  1. Az ABS formulára vonatkozó közvetlen tabló alapján terjesztettük ki a gyökeret. A tabló így kezdődik:

Ha ebben a tablóban összevonjuk a gyökeret a ¬A csúccsal, akkor az S{¬A} egy tablóját kapjuk, amelynek mélysége n. (Tulajdonképpen az eredeti tablóból kivágjuk a B csúcsot, és az összes leszármazottját.) Az indukciós feltevésből következik, hogy S{¬A} inkonzisztens. Hasonlóan kapjuk azt, hogy S{B} is inkonzisztens.

  • Mivel S{¬A} inkonzisztens, ezért S0A, de ABS, így S0B.

  • Mivel S{B} is inkonzisztens, ezért S0¬B.

Látjuk, hogy S0B és S0¬B, tehát S inkonzisztens.

  1. A ¬(AB)S formulára vonatkozó közvetlen tabló alapján terjesztettük ki a gyökeret. A tabló így kezdődik:

Ha ebben a tablóban összevonjuk a három első csúcsot, akkor megkapjuk az S{A,¬B} tablóját, amelynek mélysége n. Az indukciós feltevésből következik, hogy S{A,¬B} inkonzisztens. A 6.1.22. tétel miatt S{A}0B és a dedukciós tétel miatt S0AB. Mivel ¬(AB)S, így nyilván S inkonzisztens.

  1. A többi eset hasonlóan vizsgálható.

Ezzel a tételt bebizonyítottuk.

Előkészítő fogalmak, elsőrendű logika

Annak érdekében, hogy a tárgyalás egyszerűbb legyen, az (egyfajtájú) elsőrendű logika nyelv ábécéjét – a nyelv kifejezőerejét megőrizve – újradefiniáljuk. A nyelv ábécéjének logikán kívüli szimbólumai legyenek a következők:

  1. minden k=1,2, esetén k aritású predikátumszimbólumok megszámlálható sorozata,

  2. individuumváltozók megszámlálható sorozata,

  3. az individuumváltozóktól különböző ún. (individuum-) paraméterszimbólumok megszámlálható sorozata.

A nyelv szintaxisa csak a termek definiálásában változik: az individuumváltozók és a paraméterszimbólumok lesznek a nyelv termjei. A formuladefiníció ugyanaz, mint a klasszikus elsőrendű nyelv esetében. Tiszta formuláknak hívjuk majd azokat az elsőrendű formulákat, amelyekben nem fordul elő paraméterszimbólum.

Az elsőrendű formulák logikai szerkezetét tekintve az α- és β-formulák mellett még két formulatípus jelenik meg:

  • γ -típusú (univerzális típusú) a xA, illetve a ¬xA formula, mint jelölt formulák pedig a TxA, illetve az FxA. Ezeket a γ jellel helyettesíthetjük, γ(a) pedig, ahol a egy paraméterszimbólum, az A(xa), illetve a ¬A(xa) formulákat jelöli.

  • δ -típusú (egzisztenciális típusú) a xA, illetve a ¬xA formulák, és mint jelölt formulák a TxA, illetve az FxA. Ezeket δ-val jelölhetjük. A δ(a) az A(xa), illetve a ¬A(xa) formulákat jelenti, ahol a paraméterszimbólum.

A nyelv szemantikájának megadása során rögzítünk egy tetszőleges, nemüres halmazt, az univerzumot, jelöljük ezt most is U-val. A nyelv egy U feletti interpretációja a nyelv minden k aritású predikátumszimbólumához egy U feletti k változós logikai leképezést rögzít. Ezután a nyelv tiszta formuláinak igazságértékét a különböző U feletti változókiértékelések mellett a szokásos módon definiálhatjuk.

Ha egy elsőrendű formulában minden paraméterszimbólum helyére U-nak egy-egy elemét írjuk be, ún. U-formulát nyerünk. Nyilván a tiszta formulák is U-formulák. Az összes – szabad individuumváltozót nem tartalmazó – zártU-formulának a halmazát jelöljük EU-val. Legyen A egy az u1,u2,,un univerzumelemeket tartalmazó zárt U-formula. A az U feletti valamely interpretációban pontosan akkor igaz, ha A-ba az u1,u2,,un helyére most az A-ban nem szereplő x1,x2,,xn egymástól különböző individuumváltozókat írva, az így kapott tiszta formula a κ(xi)=ui (i=1,2,,n) változókiértékelés mellett igaz -ben. Legyenek α,β,γ és δ zárt U-formulák. Az U univerzum feletti bármely interpretációban az EU-beli formulák szemantikája alapján nyilvánvaló, hogy

  1. α pontosan akkor igaz, ha α1 is és α2 is igaz,

  2. β pontosan akkor igaz, ha β1 vagy β2 igaz,

  3. γ pontosan akkor igaz, ha γ(u) igaz minden uU-ra,

  4. δ pontosan akkor igaz, ha δ(u) igaz legalább egy uU-ra.

Határozzuk meg végül a paraméterszimbólumokat is tartalmazó zárt – szabad individuumváltozót nem tartalmazó – formulák szemantikáját. Egy az a1,a2,,an paraméterszimbólumokat tartalmazó zárt formulát az U feletti valamely interpretáció kielégíti, ha van a paraméterszimbólumoknak U-ba való olyan ς leképezése, hogy az ς(ai)U individuumokat rendre ai helyére írva, az így nyert zárt U-formula igaz -ben. Jelöljük az A formulából így nyert U-formulát Aς-val.

6.4.23. LEMMA. Legyen S egy olyan elsőrendű zárt formulahalmaz, melynek elemei paraméterszimbólumokat tartalmazhatnak (de U-beli individuumokat nem).

  1. Ha S kielégíthető és αS, akkor S{α1,α2} is kielégíthető.

  2. Ha S kielégíthető és βS, akkor S{β1} és S{β2} közül legalább az egyik kielégíthető.

  3. Ha S kielégíthető és γS, akkor minden a paraméterszimbólumra S{γ(a)} is kielégíthető.

  4. Ha S kielégíthető, δS és a olyan paraméterszimbólum, amely nem fordul elő S-ben, akkor S{δ(a)} is kielégíthető.

BIZONYÍTÁS. Az első három állítás igazolása egyszerű, ezért az olvasóra bízzuk. A negyedik bizonyítása a következő: A feltétel szerint van S leíró nyelvének olyan interpretációja valamely U univerzum felett és S paraméterszimbólumainak olyan ς leképezése U-ba, hogy minden AS-re Aς – ami paraméterszimbólumot nem tartalmazó zárt U-formula – -ben igaz. Így esetünkben δς-ben igaz, de ekkor van legalább egy uU, hogy δς(u) igaz -ben. A ς leképezést csak S-beli paraméterszimbólumokra definiáltuk, most terjesszük ki a-ra is:

ς * ( a ) { u , ha a = a , ς ( a ) egyébként .

ς * nyilván S{δ(a)} minden paraméterszimbólumára definiált. Világos, hogy minden AS-re Aς* ugyanaz a zárt U-formula, mint Aς, ezért Aς* igaz -ben. A δ(a)ς* is ugyanaz a zárt U-formula, mint a δς(u), ezért δ(a)ς* is igaz -ben. Következésképpen minden AS{δ(a)} esetén Aς* igaz -ben. Így S{δ(a)} kielégíthető.

6.4.24. DEFINÍCIÓ. Az U univerzum feletti elsőrendű Hintikka-halmaz egy olyan SEU formulahalmaz, amely az alábbi tulajdonságokkal rendelkezik:

H 0: Komplemens literálpár (U-atom és negáltja) nem fordul elő S-ben.

H 1: Ha αS, akkor α1S és α2S.

H 2: Ha βS, akkor β1S vagy β2S.

H 3: Ha γS, akkor γ(u)S minden uU-ra.

H 4: Ha δS, akkor δ(u)S legalább egy uU-ra.

6.4.25. LEMMA. (HINTIKKA-LEMMA AZ ELSŐRENDŰ LOGIKÁBAN.)

Ha S az U univerzum feletti elsőrendű Hintikka-halmaz, akkor S kielégíthető (U felett).

BIZONYÍTÁS. Mivel S Hintikka-halmaz tartalmaz, elemei zárt U-formulák. Továbbá S tartalmaz literálokat, de H0 miatt nem tartalmaz komplemens literálpárt. Legyen e tetszőlegesen rögzített igazságérték és legyen az interpretáció a következő:

| P ( u 1 , u 2 , , u n ) | { i , ha P ( u 1 , u 2 , , u n ) S , h , ha ¬ P ( u 1 , u 2 , , u n ) S , e egyébként .

A szerkezeti indukció elvének segítségével megmutatjuk, hogy tetszőleges AS formula igaz az így megadott interpretációban.

(alaplépés:) Atomi formulák és negált atomi formulák esetén nyilvánvaló az állítás.

(indukciós lépések:)

  • Az α- és β-formulákra a 6.4.9. tételhez hasonlóan bizonyítunk, így az olvasóra hagyjuk.

  • Tekintsünk egy γS formulát, ekkor H3 miatt minden uU-ra γ(u)S. Amennyiben γ(u) minden uU-ra igaz -ben, akkor nyilván γ is igaz -ben.

  • Tekintsünk egy δS formulát, ekkor H4 miatt δ(u)S legalább egy uU-ra. Amennyiben δ(u) igaz -ben, akkor δ is igaz lesz -ben.

Ezzel a Hintikka-lemmát bebizonyítottuk.

Az elsőrendű analitikus tabló

Az elsőrendű tablók módszerében – az ítéletlogikai tablókhoz hasonlóan – minden formulafajtára van egy-egy levezetési szabály, azaz közvetlen tabló. A 6.26. ábrában felsoroljuk az α-, β-, γ- és a δ-típusú formulákra a közvetlen tablókat:

Figure 6.26. Közvetlen tablók α-, β-, γ- és δ- formulákra

Közvetlen tablók α-, β-, γ- és δ- formulákra

Hasonlóan adhatjuk meg a ,,jelöletlen” és a jelölt elsőrendű formulákra is a közvetlen tablókat. A 6.27. és a 6.28. ábrákban csak a (C) és (D) közvetlen tablókat soroljuk fel:

Figure 6.27. Közvetlen tablók ,,jelöletlen” formulákra

Közvetlen tablók ,,jelöletlen” formulákra

A (D) közvetlen tablóknál a ,,megkötéssel” megjegyzés azt jelenti, hogy ha az a paraméterszimbólumot a tablóépítés során korábban már bevezettük valamely (C) vagy (D) közvetlen tablóval az ágon, akkor nem használhatjuk fel újra (mert az interpretációban szabadon választható értéket szeretnénk majd biztosítani a (D) közvetlen tablóval bekerülő paraméterszimbólum számára). Ha viszont a (C) közvetlen tablót alkalmazzuk egy ilyen a ún. kritikus paraméterszimbólum bevezetése után, a felhasználható C-ben.

Figure 6.28. Közvetlen tablók jelölt formulákra

Közvetlen tablók jelölt formulákra

6.4.26. DEFINÍCIÓ. Egy C elsőrendű tiszta formula analitikus tablója egy olyan bináris fa, melynek csúcsai ,,jelöletlen” elsőrendű formulák. A fa gyökere a C formula. Előállítjuk C közvetlen tablóját a 6.26. vagy 6.27. ábra alapján. Tegyük fel, hogy C-nek egy T tablója adott. Legyen T-ben D egy levélcsúcs. Ekkor a T tabló közvetlen kiterjesztése a következők valamelyike:

  1. Ha van még nem ,,feldolgozott” α-formula a gyökérből a D csúcsba vezető úton, akkor kapcsoljuk D-hez rendre ezen út folytatásaként az α formula közvetlen tablója alapján nyert α1 és α2 formulákat mint új csúcsokat.

  2. Ha van még nem ,,feldolgozott” β-formula a gyökérből a D csúcsba vezető úton, akkor D-ben elágazik a tabló, és a bal oldali rákövetkező csúcsba β közvetlen tablójából β1, a jobb oldali rákövetkezőbe pedig β2 kerül.

  3. Ha van γ-formula a gyökérből a D csúcsba vezető úton, akkor D-hez kapcsoljunk ezen út folytatásaként egy a γ közvetlen tablója szerint nyert γ(a) formulát mint új csúcsot, ahol a tetszőleges paraméterszimbólum.

  4. Ha van δ nem ,,feldolgozott” formula a gyökérből a D csúcsba vezető úton, akkor D-hez kapcsoljuk ezen út folytatásaként a δ közvetlen tablója szerint nyert δ(a)-t mint új csúcsot, ahol a gyökérből a D csúcsba vezető úton az a paraméterszimbólum nem fordul elő, azaz a egy kritikus paraméterszimbólum.

  5. Ha van ¬¬A alakú nem ,,feldolgozott” formula a gyökérből a D csúcsba vezető úton, akkor D-hez kapcsoljuk ezen út folytatásaként az A formulát tartalmazó új csúcsot.

6.4.27. PÉLDA. A x(P(x)Q(x))(xP(x)xQ(x)) formula analitikus tablója:

Egy tiszta formula jelölt tablóját – az analitikus elsőrendű tablóhoz hasonlóan – a 6.28. ábrán látható közvetlen tablók segítségével a 6.4.13. definíció kiterjesztésével adhatjuk meg. Egészítsük ki ezt a definíciót a következőkkel:

C. Ha van TA, illetve FA alakú jelölt formula a gyökérből a D csúcsba vezető úton, akkor D-hez kapcsoljuk ezen út folytatásaként TA(xa), illetve FA(xa) formulát mint új csúcsot, ahol a tetszőleges paraméterszimbólum.

D. Ha van FA, illetve TA alakú nem ,,feldolgozott” jelölt formula a gyökérből a D csúcsba vezető úton, akkor D-hez kapcsoljuk ezen út folytatásaként TA(xa), illetve FA(xa) formulát mint új csúcsot, ahol a kritikus paraméterszimbólum.

A (D) közvetlen tablót liberalizálhatjuk a következők szerint: Ha az a paraméterszimbólumot új paraméterszimbólumként vezettük be egy (C) közvetlen tablóval a tabló aktuális ágán, akkor később egy (D) közvetlen tablóval újra felhasználhatjuk (mivel a (C)-vel bevezetett paraméterszimbólum interpretációbeli értéke tetszőleges, tehát a (D)-vel bevezetett érték is megfelel számára.) Ezzel a liberalizálással a tabló sok esetben rövidíthető.

6.4.28. PÉLDA. A y(xP(x)P(y)) formula jelölt tablója

  1. nem liberalizált paramétertechnikával:

  1. liberalizált paramétertechnikával:

Az elsőrendű tablókalkulus helyességének bizonyításához először be kell látni, hogy a tabló közvetlen kiterjesztésével a (C) és a (D) közvetlen tablók alkalmazása esetén is kielégíthetőek maradnak az addig kielégíthető ágak. Legyen Θ a T tabló egy kielégíthető ága. Más szóval legyen T igaz tabló valamely interpretációban.

  • Ha egy (C) közvetlen tablóval történt a közvetlen kiterjesztés, akkor a megfelelő γ formula igaz volt az ágat kielégítő interpretációban, de emiatt a γ(a) is igaz lesz ebben az interpretációban.

  • Ha egy (D) közvetlen tablóval történt a közvetlen kiterjesztés, akkor a megfelelő δ formula igaz volt az ágat kielégítő interpretációban, de amiatt, hogy a δ(a)-ban az a paraméterszimbólum új, megválasztható úgy, hogy a δ(a) is igaz legyen az eredeti interpretáció olyan alkalmas bővítésében, mely a-t is kiértékeli.

Abból, hogy egy adott interpretációban igaz tabló minden közvetlen kiterjesztése is igaz az interpretációban, következik, hogy ha a gyökérben lévő A (zárt és tiszta) formula igaz egy interpretációban, akkor az A formula T tablója is igaz az interpretációban.

A tabló egy ágát most is zártnak nevezzük, ha az ágon (elsőrendű) komplemens literálpár fordul elő, és a tabló akkor zárt, ha minden ága zárt, egyébként a tabló nyitott.

6.4.29. TÉTEL. (AZ ELSŐRENDŰ TABLÓ HELYESSÉGE.)

Ha az elsőrendű A formula tablója zárt, akkor A kielégíthetetlen.

BIZONYÍTÁS. Ha egy T tabló zárt, akkor T nem lehet igaz egyetlen interpretációban sem, hisz egyetlen ága sem lehet igaz egyetlen interpretációban sem. Tehát – a fentiek alapján – a T gyökerében lévő formula kielégíthetetlen.

A tabló egy Θ ága befejezett, ha a Θ-n lévő fel nem dolgozott formulák literálok, és ha egy γ-típusú formula és egy a paraméterszimbólum előfordul Θ-n, akkor γ(a) is szerepel Θ-n. A tabló befejezett, ha minden ága befejezett.

Ezután olyan szisztematikus tablóépítési stratégiát vezetünk be, amely biztosítja, hogy befejezett ágak állhassanak elő: Először az (A), a (B) és a (D) tablóépítési szabályokat hajtjuk végre, amíg lehet. Ezután a (C) közvetlen tablók egyszeri alkalmazása következik úgy, hogy a közvetlen kiterjesztés során a γ(a) formulán kívül a γ formula is az ág végére kerül. A tablóépítést addig folytatjuk, amíg az ág vagy befejezett, vagy zárt nem lesz. Befejezett szisztematikus tablónak nevezzük azt a szisztematikus tablót, amely vagy végtelen, vagy véges, de további kiterjesztése már nem lehetséges (minden nem atomi formulát feldolgoztunk és a γ formulák feldolgozása is befejeződött).

6.4.30. TÉTEL. Egy befejezett szisztematikus tabló nyitott ágai kielégíthetők.

BIZONYÍTÁS. Vegyük észre, hogy egy befejezett szisztematikus tabló nyitott ágán egy elsőrendű Hintikka-halmaz áll elő, ahol U az ágon szereplő paraméterszimbólumok halmaza. Egy elsőrendű Hintikka-halmaz pedig a 6.4.25. lemma miatt kielégíthető.

Ez a tétel lehetővé teszi, hogy véges univerzumon kielégíthető formula esetén az univerzum számosságáról információt kapjunk. Ha egy formula tablója nem zárt, tehát van legalább egy nyitott Θ ága, amelyen Hintikka-halmaz állt elő az ágon előforduló paraméterszimbólumok véges halmazára nézve. Ekkor nem folytatjuk a szisztematikus tabló építését, mivel a Hintikka-lemma szerint Θ (így a gyökérformula is) kielégíthető e véges univerzumon.

6.4.31. PÉLDA. A x(P(x)Q(x))xP(x)xQ(x) formula nem logikai törvény. Ha tudni szeretnénk, hogy milyen interpretációkban hamis ez a formula, akkor keressük meg az

F x ( P ( x ) Q ( x ) ) x P ( x ) x Q ( x )

jelölt formulát kielégítő interpretációkat tablóval.

A tablónak van egy nyitott Θ ága. Ezen az ágon az α- és a β-csúcsok, valamint a δ-csúcsok mind fel lettek dolgozva. A γ-csúcs pedig az ágon megjelenő mindkét paraméterszimbólummal fel van dolgozva. Ez egy igaz ág, és a kételemű {a,b} univerzumon már kielégíthető. Ezért a gyökérben lévő formula is kielégíthető az {a,b} univerzum felett. A formulát kielégítő interpretáció: {¬P(a),P(b),Q(a),¬Q(b)}.

6.4.32. TÉTEL. (AZ ELSŐRENDŰ TABLÓ TELJESSÉGE.)

Ha az A elsőrendű formula logikailag igaz, akkor van az FA jelölt formulának zárt, befejezett tablója.

BIZONYÍTÁS. Legyen A logikailag igaz elsőrendű formula. Legyen T az FA jelölt formula befejezett szisztematikus tablója. Ha T-nek lenne egy Θ nyitott ága, akkor Θ (és így ¬A is) kielégíthető lenne, ellentétben azzal, hogy A logikailag igaz.

Most az elsőrendű tablómódszerrel bebizonyítjuk a 6.3.49. tételt.

6.4.33. TÉTEL. (LÖWENHEIM ÉS SKOLEM TÉTELE.)

Ha egy elsőrendű formula kielégíthető egyáltalán, akkor kielégíthető legfeljebb megszámlálható univerzumon is.

BIZONYÍTÁS. Legyen A egy kielégíthető elsőrendű formula, és T legyen A befejezett szisztematikus tablója. Mivel A kielégíthető, T-nek van nyitott ága. Két eset lehetséges.

  • Ha a nyitott ág véges, A már véges univerzum felett kielégíthető.

  • Ha a nyitott ág végtelen, a faépítési szabályok szerkezete miatt az ágon a paraméterszimbólumok halmaza megszámlálhatóan végtelen, így A kielégíthető megszámlálható univerzum felett.

Így a tétel bizonyítást nyert.

Tabló a klasszikus elsőrendű logikai nyelv esetén

Legyen [Vv] az 5.1. fejezetben definiált elsőrendű logikai nyelv. Az alábbi ábra mutatja a (C) és a (D) közvetlen tablókat [Vv]-ben:

A (C) közvetlen tablóban t az [Vv] nyelv tetszőleges termje lehet. A (D) közvetlen tablóban y egy olyan individuumváltozó, amelynek nincs szabad előfordulása a kiterjesztés alatt levő ág egyetlen formulájában sem. Az y-t kritikus változónak hívjuk.

6.4.34. PÉLDA. Vizsgáljuk meg, hogy a (xAB)x(AB) zárt formula logikailag igaz-e. A vizsgálandó formula zárt, tehát xPar (B).

A tabló építése során a ¬xA formulára (D) szabályt kell alkalmazni. Választhatjuk az x individuumváltozót is kritikus változónak, mivel x nem fordul elő szabadon az ágon. Tovább építve az ágat, a ¬x(AB) formulára a (C) szabályt alkalmaztuk, ahol egy tetszőleges termet (tehát épp x-et is) írhatunk a felszabadult x helyére a ¬(AB) formulában.

Ha az elsőrendű logikai nyelv egyenlőségjeles, akkor a következő – az egyenlőségre vonatkozó – szabályokat is hozzá kell venni a tablóépítő szabályokhoz:

A tablókalkulus helyességének és teljességének bizonyítása a klasszikus elsőrendű logikai nyelv esetére nem változik.

6.4.35. MEGJEGYZÉS. A tabló módszernek mint tételbizonyító eljárásnak eszközzé való fejlesztése aktuális kutatási témája a számítástudomány-orientált logikának. Egy összefoglaló mű ebben a témában [2]. 1995 óta nemzetközi konferenciákat is szerveznek ,,Automated Reasoning with Analytic Tableaux and Related Methods” címmel, amelynek az LNAI sorozatban jelenik meg az anyaga.

Feladatok

6.4.1. FELADAT. Lássuk be a tablók módszerével, hogy az alábbi formulák tautológiák.

  1. Y ( X Y )

  2. ( X Y ) ( Y Z ) ( X Z )

  3. ( X Y ) ( X Z ) ( X Y Z )

  4. ( X Z ) ( Y Z ) ( X Y ) Z

  5. ¬ ( X Y ) ¬ X ¬ Y

  6. ¬ ( X Y ) ¬ X ¬ Y

  7. ¬ X ¬ Y ¬ ( X Y )

  8. X ( Y Z ) ( X Y ) ( X Z )

6.4.2. FELADAT. Mutassuk meg tablóval, hogy az alábbi formulák logikai törvények.

  1. x ( A B ) ( x A x B )

  2. A x A , ahol xPar (A)

  3. x A [ A ( x t ) ]

  4. [ A ( x t ) ] x A

6.4.3. FELADAT. Legyenek s és t olyan termek, amelyekben az y individuumváltozó nem fordul elő. Mutassuk meg, hogy az

( s = t ) , y ( ( s = y ) ( t = y ) ) és y ( ( s = y ) ( t = y ) )

formulák logikailag ekvivalensek.

6.4.4. FELADAT. Legyen A a

x y R ( x , y ) ¬ x R ( x , x ) x y z ( R ( x , y ) R ( y , z ) R ( x , z ) )

formula. Könnyű belátni, hogy ez a formula igaz a természetes számok halmazán, ha R a ,,kisebb” reláció. Vagyis A kielégíthető megszámlálható univerzumon. Lássuk be tablóval, hogy A egyetlen egy véges univerzumon sem elégíthető ki.



[11] Angolul saturated.