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.

Chapter 6. A logika szintaktikus tárgyalása

Chapter 6. A logika szintaktikus tárgyalása

Bizonyításelmélet

Az ítéletlogikában a szemantikus eldöntésprobléma megoldásakor a vizsgált ítéletlogikai formuláról el kell tudni dönteni azt, hogy tautológia-e, esetleg azt, hogy kielégíthetetlen-e. A döntéshez egy n-változós formula esetén a formula összes – 2n különböző – interpretációjában szükséges lehet a formula vizsgálata. Ez akkor is kezelhetetlen feladat, ha a ,,lusta” kiértékeléssel dolgozunk. Az elsőrendű logika vonatkozásában ugyanez a feladat annak a kérdésnek az eldöntése, hogy egy elsőrendű formula logikailag igaz-e (logikai törvény-e). Mivel a megszámlálható univerzum esetén a lehetséges modellek száma kontinuum, az esetek végignézése szóba sem jöhet. Ezért olyan módszereket kerestek, amelyek a formula szintaktikai jellegzetességeit használják ki, és egy olyan szintaktikus eldöntésproblémára adnak döntési eljárást, amely megoldása az eredeti szemantikus eldöntésprobléma megoldását vonja maga után.

Egy ilyen döntési eljárás során ,,adatokból” – egy formulából vagy egy formulahalmazból – kiindulva az eljárás lépései során formulák egy sorozatát állítjuk elő. Ezt a formulasorozatot levezetésnek nevezzük. Az eljáráshoz levezetési szabályok tartoznak, amelyek formulákból új formulát alkotva lehetővé teszik a levezetés előállítását. Minden döntési eljárás esetén adott egy ún. megállási feltétel. Ez általában egy meghatározott formula megjelenése a levezetésben vagy a levezetés speciális szerkezetűvé válása. Egy konkrét döntési eljárás esetén az a kérdés, hogy ,,adott bemenet mellett elérhető-e a megállási feltétel” úgy is tekinthető, mint a döntési eljáráshoz tartozó (szintaktikus) eldöntésprobléma. Ezen döntési eljárásokat kalkulusoknak szokás nevezni. Az alábbiakban a döntési eljárások két fontos tulajdonságát fogalmazzuk meg.

6.1.1. DEFINÍCIÓ.

  1. Azt mondjuk, hogy egy kalkulus helyes, ha a szintaktikus eldöntésproblémára adott igen válaszból következik, hogy a szemantikus eldöntésproblémára is igen a válasz.

  2. Egy kalkulus teljes, ha minden olyan esetben, amikor a szemantikus eldöntésproblémára igen a válasz, a döntési eljárás a szintaktikus eldöntésproblémára adott igen válasszal eléri a megállási feltételt.

Ha a logika alapproblémájának a tételbizonyítás megoldását tekintjük, akkor a logika tárgyalásának tekinthető bármely kalkulus, amely mögött következményfogalom és (vagy) eldöntésprobléma áll. Ezért mondhatjuk azt, hogy a

logika = nyelv + kalkulus.

A logika ilyen felépítését (szintaktikus következményfogalom, szintaktikus eldöntésprobléma) szokták a logika értékmentes tárgyalásának is nevezni, mivel logikai igazságértékeket, igazságtáblát nem használ. Az alábbiakban áttekintjük a legismertebb kalkulusokat.

Az ítéletkalkulus

Nézzük meg, hogyan lehet felépíteni az ítéletlogikát szemantikai fogalmak nélkül, tisztán szintaktikai eszközökkel. Az ítéletkalkulus, más néven az ítéletlogika bizonyításelméleti tárgyalása Hilbert nevéhez fűződik. Az ítéletkalkulusban néhány kitüntetett szerkezetű ítéletlogikai formulát, ún. axiómasémát, valamint egy levezetési szabályt rögzítünk. Az axiómasémák tautológiák, és ha bennük az ítéletváltozókat tetszőleges ítéletlogikai formulával helyettesítjük, a 4.3.5. tétel szerint újból tautológiákat kapunk. Az axiómasémákból formulahelyettesítéssel állnak elő az axiómaformulák, röviden axiómák. Mivel minden tautológia ugyanazt a logikai műveletet írja le, egyes szerzők úgy tekintik, hogy a bizonyításelméletben az axiómák halmaza az összes tautológia. Ekkor azonban problematikus annak eldöntése, hogy egy formula – szerkezetét tekintve – axióma-e. Az axiómák a nyelvben felhasznált logikai műveletek tulajdonságait írják le. A {¬,} funkcionálisan teljes művelethalmaz, ezért egy logikai nyelv ábécéjébe elegendő csak ezt a két műveletet betenni. Egy ilyen nyelv esetén a kiválasztott axiómasémáknak csak e két műveletnek megfelelő logikai összekötőjeleket kell tartalmazniuk.

Table 6.1. Az ítéletkalkulus axiómasémái

(A1)

X ( Y X )

(A2)

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

(A3)

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


Az ítéletkalkulus három axiómasémája alapján helyettesítéssel kapjuk az axiómaformulákat.

6.1.2. MEGJEGYZÉS. Az (A1) axiómaséma a 4.3.6. tételben bizonyított ,,bővítés előtaggal”, az (A2) az ,,implikációlánc”, az (A3) a ,,reductio ad absurdum” tautológia. Az (A3) axiómaséma helyett szoktak más sémát is használni, például a kontrapozíciót kifejező (¬X¬Y)(YX) sémát.

Egy levezetési szabály ítéletlogikai formulákból új ítéletlogikai formulát állít elő. Azt mondjuk, hogy a levezetési szabály helyes, ha a levezetett formula szemantikus következménye azoknak a formuláknak, amelyekből levezettük. Az ítéletkalkulus levezetési szabálya – a modus ponens vagy leválasztási szabály – a 4.4.12. tételből ismert ({XY,X},Y) helyes következtetési formához kötődik.

Table 6.2. Az ítéletkalkulus levezetési szabálya

(MP)

{ X Y , X } 0 Y


A leválasztási szabály – (MP) – segítségével a következőképpen állíthatunk elő formulát: ha rendelkezésünkre áll egy implikációs formula: AB és ennek bal oldali közvetlen részformulája (előtagja): A is, akkor azt mondjuk, hogy a modus ponenssel előáll a jobb oldali közvetlen részformula (utótag): B.

Az ítéletkalkulus axiómasémáinak és levezetési szabályának rögzítése után bevezetjük a bizonyításelméleti levezetés fogalmát.

6.1.3. DEFINÍCIÓ. Legyen {A1,A2,} formulák tetszőleges, esetleg üres halmaza és B egy formula. Az {A1,A2,} formulahalmazból a B formula ítéletkalkulusbeli levezetése egy olyan D1,D2,,Dm(m1) formulasorozat, ahol minden j=1,2,,m-re Dj

  1. vagy eleme az {A1,A2,} formulahalmaznak, azaz ún. feltételformula vagy hipotézis,

  2. vagy valamelyik axiómasémából formulahelyettesítéssel állt elő, azaz axiómaformula,

  3. vagy van olyan 1s,tj, hogy a Ds és a Dt formulákból a levezetési szabállyal állt elő,

és a formulasorozat utolsó tagja, Dm, éppen a B formula.

6.1.4. DEFINÍCIÓ. Azt mondjuk, hogy a B formula az {A1,A2,} formulahalmazból az ítéletkalkulusban levezethető, ha B-nek van az {A1,A2,} formulahalmazból levezetése. Jelölése: {A1,A2,}0B, amit röviden szekvenciának fogunk nevezni.

A logika szemantikus következményfogalma az igazság fogalmán alapul. Az igazságfogalmat a tényekre alapozzuk. Az ítéletkalkulusbeli levezethetőség az ítéletkalkulus következményfogalma, amelyet szintaktikus következményfogalomnak is neveznek. A szintaktikus következményfogalom definiálásához csak szintaktikai fogalmakat használtunk.

6.1.5. MEGJEGYZÉS. A levezetés fogalmának definíciója biztosítja, hogy a hipotézisek halmazából ezen feltételformulák bármelyike levezethető, egy axiómaformula pedig levezethető bármely hipotézishalmazból, tehát az üres hipotézishalmazból is.

6.1.6. DEFINÍCIÓ. Egy B formula bizonyítható az ítéletkalkulusban, ha van hipotézismentes levezetése (azaz levezethető az üres feltételformula-halmazból). Ebben az esetben a 0B jelölést alkalmazzuk.

6.1.7. PÉLDA. Most megmutatjuk, hogy AA bizonyítható az ítéletkalkulusban, azaz megalapozzuk a 0AA szekvenciát. A levezetés megszerkesztése során az ,,(Ai) axiómasémából a … formulahelyettesítéssel nyert formula” helyett röviden [ (Ai): … ]-t, a ,,levezetés i. és j. formulájából modus ponenssel állt elő” helyett pedig röviden [ (MP): i,j ]-t írunk. A levezetés a következő:

1.

( A ( ( A A ) A ) ) ( ( A ( A A ) ) ( A A ) )

[ ( A 2 ) : ( X , Y , Z A , A A , A ) ]

2.

A ( ( A A ) A )

[ ( A1 ) : ( X , Y A , A A ) ]

3.

( A ( A A ) ) ( A A )

[ (MP): 1, 2 ]

4.

A ( A A )

[ ( A1 ) : ( X , Y | | A , A ) ]

5.

A A

[ (MP): 3, 4 ]

6.1.8. MEGJEGYZÉS. A levezetés során felhasznált formulák alakja implikációs lánc. A levezetési szabály az implikációs lánc előtagjának eltávolításával kapott új formulát vezeti be. Ezért kézenfekvő egy formula levezetésének megszerkesztését egy olyan implikációs láncformulával kezdeni, amelynek utolsó formulája a levezetendő formula és az előtag(ok) leválaszthatók. Ezt tettük a fenti példában is.

6.1.9. PÉLDA. Megmutatjuk, hogy a 4.1.21. példa (c) részében a nyomozók sejtését leíró formula levezethető a nyomozás során megállapított tényeket leíró, célszerű alakú formulákból, azaz

{ ¬ ¬ X Y , ¬ ¬ Y Z , X U , U V Z , ¬ Z } 0 ¬ X .

Először kiküszöböljük a -t. XU helyett bevezetjük a vele tautologikusan ekvivalens ¬XU,¬UX formulákat a feltételhalmazba. A levezetés:

1.

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

[ (A3) ]

2.

¬ ¬ X Y

[ hipotézis ]

3.

( ¬ ¬ X ¬ Y ) ¬ X

[ (MP): 1, 2 ]

4.

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

[ (A3) ]

5.

¬ ¬ Y Z

[ hipotézis ]

6.

( ¬ ¬ Y ¬ Z ) ¬ Y

[ (MP): 4, 5 ]

7.

¬ Z ( ¬ ¬ Y ¬ Z )

[ (A1) ]

8.

¬ Z

[ hipotézis ]

9.

¬ ¬ Y ¬ Z

[ (MP): 7, 8 ]

10.

¬ Y

[ (MP): 6, 9 ]

11.

¬ Y ( ¬ ¬ X ¬ Y )

[ (A1) ]

12.

¬ ¬ X ¬ Y

[ (MP): 10, 11 ]

13.

¬ X

[ (MP): 3, 12 ]

6.1.10. DEFINÍCIÓ. A D1,D2,,Dm1 és a D1,D2,,Dm2 formulasorozatok konkatenációján a D1,D2,,Dm1,D1,D2,,Dm2 formulasorozatot értjük.

6.1.11. LEMMA. Ha a d1 és d2 rendre a Γ1 és a Γ2 hipotézishalmazokból való levezetés, akkor a két levezetés konkatenációja egy – a Γ1Γ2 hipotézishalmazból való – levezetés.

BIZONYÍTÁS. A d1 és d2 levezetések konkatenációjával kapott formulasorozat tetszőleges D eleme

  1. vagy hipotézisként került valamelyik levezetésbe, tehát DΓ1Γ2,

  2. vagy axiómasémából állt elő a két levezetés valamelyikében, akkor a konkatenációban is axiómaformula,

  3. vagy a modus ponenssel állt elő két őt megelőző formulából a két levezetés valamelyikében, akkor (mivel a formulák sorrendjét a levezetésekben nem változtattuk meg) a konkatenált formulasorozatban ugyanez a szerepe.

Tehát a konkatenáció egy levezetés, ahol a hipotézishalmaz Γ1Γ2.

Definiáltuk a szintaktikus következményfogalmat, amely rokonítható a szemantikus következményfogalommal. Definiáltuk a bizonyíthatóságot, mint egy ítéletlogikai formula tulajdonságát. Most megvizsgáljuk, hogy a szemantikus eldöntésprobléma megfogalmazásához szükséges dedukciós tétel formai megfelelője bebizonyítható-e.

6.1.12. TÉTEL. (DEDUKCIÓS TÉTEL.) Legyenek A1,A2,,An,B(n1) tetszőleges ítéletlogikai formulák. {A1,A2,,An1,An}0B pontosan akkor, ha {A1,A2,,An1}0AnB.

BIZONYÍTÁS. Jelölje Γ az {A1,A2,,An1,An}, Γ pedig az {A1,A2,,An1} formulahalmazt.

  1. Először azt bizonyítjuk be, hogy ha Γ0B, akkor Γ 0AnB. Γ0B azt jelenti, hogy B-nek van levezetése Γ-ból. Legyen ez a levezetés D1,D2,,Dm=B. A bizonyítás a következő lépésekből áll:

  • Írjuk a levezetésben szereplő formulák elé az An szimbólumsorozatot. Így az AnD1,AnD2,,AnDm=AnB formulasorozatot kapjuk.

  • Lássuk be, hogy minden k-ra (1km) létezik AnDk-nak Γ -ből való levezetése.

    1. Legyen Dk axiómaformula, ekkor AnDk bizonyítható. A levezetés:

1.

D k A n D k

[ (A1) ]

2.

D k

[ axiómaformula ]

3.

A n D k

[ (MP): 1, 2 ]

  1. Legyen Dk(An) eleme a Γ-nak, ekkor AnDk levezethető Γ -ből. A levezetés:

    1.

    D k A n D k

    [ (A1) ]

    2.

    D k

    [ hipotézis ]

    3.

    A n D k

    [ (MP): 1, 2 ]

  1. Legyen Dk=An. Az AnAn szekvenciának a 6.1.7. példában megadtuk a bizonyítását.

  2. Legyen Dk az első olyan (eddig még nem vizsgált) formula az eredeti levezetésben, amely modus ponense Dt,Ds=DtDk levezetésbeli formuláknak (s,tk). Ez azt jelenti, hogy már igazoltuk, hogy Γ -ből az AnDtDk, valamint az AnDt formula levezethető:

i .

A n D t D k

j .

A n D t

w .

( A n D t D k ) ( A n D t ) A n D k  [ (A2) ]

( w + 1 ) .

( A n D t ) A n D k

[ (MP): i, w ]

( w + 2 ) .

A n D k

[ (MP): j, (w+1) ]

Indukcióval könnyen bizonyítható, hogy Γ 0AnDk akkor is, ha Dk tetszőleges – nem feltétlen az első – olyan formula az eredeti levezetésben, amelyet modus ponenssel nyertünk.

  • Az AnDk formulák elé (1km) beírjuk azok levezetését a Γ -ből. Ezzel Γ -ből való levezetések konkatenációját kapjuk, ami a Γ -ből való levezetése az AnB formulának.

2. Most pedig azt bizonyítjuk, hogy ha Γ 0AnB, akkor Γ0B. A feltétel szerint Γ 0AnB. Legyen ez a levezetés

D 1 , D 2 , , D m 1 , A n B .

Írjuk a levezetés végére az An formulát és a két utolsó formula modus ponensét. Ez éppen a B egy levezetése Γ-ból:

D 1 , D 2 , , D m 1 , A n B , A n , B

Ezzel a dedukciós tételt bebizonyítottuk.

6.1.13. TÉTEL. (AZ ELDÖNTÉSPROBLÉMA TÉTELE.)

Legyenek A1,A2,,An1,An,B(n1) tetszőleges ítéletlogikai formulák. {A1,A2,,An1,An}0B pontosan akkor, ha

0 A 1 A 2 A n 1 A n B .

BIZONYÍTÁS. {A1,A2,,An1,An}0B-re n-szer alkalmazva a dedukciós tételt egyik irányban, és 0A1A2An1AnB-re n-szer alkalmazva a dedukciós tételt visszafelé, a tétel mindkét irányú állítása könnyen adódik.

6.1.14. MEGJEGYZÉS. Mivel egy formulahalmazban a formulák sorrendje tetszőleges, a 6.1.13. tétel kimondható úgy is, hogy {A1,A2,,An1,An}0B akkor és csak akkor, ha 0Ai1Ai2AinB, ahol i1,i2,,in az 1,2,,n számok tetszőleges permutációja.

A 6.1.13. tétel azt mondja ki, hogy a következő két állítás ekvivalens:

  1. Az {A1,A2,,An} formulahalmazból a B formula levezethető.

  2. Az A1A2AnB formula bizonyítható.

Tehát annak eldöntéséhez, hogy egy B formula az adott feltételek mellett tétel-e, el kell tudni dönteni, hogy a megfelelő ítéletlogikai formula bizonyítható-e. Ez az ítéletkalkulus eldöntésproblémája. Az eldöntésprobléma megoldása itt is az automatikus tételbizonyítást jelenti. A bizonyításelméleti levezetés célja (megállási feltétele) az, hogy a levezetés során előálljon a levezetendő formula. A levezetés definíciója miatt az ítéletkalkulusban eldöntésproblémának nem csak azt tekintjük, hogy bizonyítható-e egy adott formula, hanem azt is, hogy levezethető-e feltételformulák valamely halmazából a formula.

6.1.15. TÉTEL. (AZ ÍTÉLETKALKULUS HELYESSÉGE.)

Legyenek A1,A2,,B ítéletlogikai formulák. Ha {A1,A2,}0B, akkor {A1,A2,}0B.

BIZONYÍTÁS. Jelölje Γ az {A1,A2,} formulahalmazt. A tétel feltétele miatt adott a D1,D2,,Dm=B levezetés. Indukcióval megmutatjuk, hogy a levezetés minden Dk(1km) formulája tautologikus következménye a hipotézisek halmazának, azaz Γ0Dk.

  1. Tetszőleges axiómaformula, illetve Γ tetszőleges eleme nyilvánvalóan szemantikus következménye Γ-nak és D1 (a levezetés első formulája) csak axiómaformula vagy Γ-beli hipotézis lehet.

  2. Tegyük most fel, hogy minden (nk)-ra igazoltuk már, hogy Γ0Dn.

  3. Ha most Dk+1 axiómaformula vagy hipotézis, akkor az előzők szerint Γ0Dk+1. Ha Dk+1 modus ponenssel állt elő Ds-ből és Dt=DsDk+1-ből, akkor s,tk miatt az indukciós feltételből Γ0Ds és Γ0DsDk+1 adódik. A modus ponensre vonatkozó 4.3.6. szemantikus tétel miatt {Ds,Dt}0Dk+1, a 4.4.3. tétel miatt pedig Γ0Dk+1.

Ezzel a tétel bizonyítást nyert.

6.1.16. DEFINÍCIÓ. Azt mondjuk, hogy az A és a B formula bizonyíthatóan ekvivalensek, ha {A}0B és {B}0A.

Ez a szemantikus tárgyalásnál definiált tautologikus ekvivalenciafogalom bizonyításelméleti megfelelője. A dedukciós tételből könnyen adódik, hogy ez pontosan akkor áll fenn, ha 0AB és 0BA. A 6.1.17. példa mutatja, hogy A és ¬¬A bizonyíthatóan ekvivalensek.

6.1.17. PÉLDA.

  1. A {¬¬A}0A szekvenciát megalapozó levezetés:

1.

5.

¬ A ¬ A

[ 6.1.7. példa ]

6.

( ¬ A ¬ A ) ( ( ¬ A ¬ ¬ A ) A )

[ (A3) ]

7.

( ¬ A ¬ ¬ A ) A

[ (MP): 5, 6 ]

8.

¬ ¬ A ( ¬ A ¬ ¬ A )

[ (A1) ]

9.

¬ ¬ A

[ hipotézis ]

10.

¬ A ¬ ¬ A

[ (MP): 8, 9 ]

11.

A

[ (MP): 7, 10 ]

  1. A {¬¬A}0A szekvenciához hasonlóan {¬¬¬A}0¬A is megalapozható. Ebből a dedukciós tétel miatt következik, hogy 0¬¬¬A¬A, azaz van hipotézismentes levezetése a ¬¬¬A¬A formulának. Így az {A}0¬¬A szekvenciát igazoló levezetés:

i .

¬ ¬ ¬ A ¬ A

[ (a) + dedukció tétel ]

( i + 1 ) .

( ¬ ¬ ¬ A A ) ( ( ¬ ¬ ¬ A ¬ A ) ¬ ¬ A )

[ (A3) ]

( i + 2 ) .

A ( ¬ ¬ ¬ A A )

[ (A1) ]

( i + 3 ) .

A

[ hipotézis ]

( i + 4 ) .

¬ ¬ ¬ A A

[ (MP): (i+2), (i+3) ]

( i + 5 ) .

( ¬ ¬ ¬ A ¬ A ) ¬ ¬ A

[ (MP): (i+1), (i+4) ]

( i + 6 ) .

¬ ¬ A

[ (MP): i, (i+5) ]

A következő példákban néhány további, az ítéletkalkulusban alapvető levezetést adunk meg.

6.1.18. PÉLDA. Megmutatjuk először, hogy {AB}0¬¬AB. Ehhez a dedukciós tétel miatt elég bizonyítani, hogy {AB,¬¬A}0B. Ha ugyanis az {AB,¬¬A}0B levezetést elő tudjuk állítani, akkor van levezetése az {AB}0¬¬AB szekvenciának is.

1.

¬ ¬ A

[ hipotézis ]

11.

A

[ 6.1.17. példa (a) része ]

12.

A B

[ hipotézis ]

13.

B

[ (MP): 11, 12 ]

6.1.19. PÉLDA. Bizonyítsuk be, hogy {AB}0¬B¬A. A 6.3. táblázat két levezetést tartalmaz. A bal oldali az AB és ¬B hipotézisekből ¬A-t vezeti le, a jobb oldali levezetésben pedig megmutatjuk, hogy ¬A levezetéséből hogyan szerkeszthetjük meg – a dedukciós tétel bizonyításánál felhasznált módszerrel – a ¬B¬A levezetését. Az első és az utolsó lépést kidolgoztuk, a második a 6.1.7. példa alapján megy, a többit az olvasóra bízzuk.

6.1.20. DEFINÍCIÓ. Azt mondjuk, hogy egy {A1,A2,} formulahalmaz ellentmondásos, ha van olyan A formula, hogy {A1,A2,}-ből A is, és ¬A is levezethető. Egyébként {A1,A2,}ellentmondástalan.

Az ellentmondásosság egy másik szokásos definíciója: Egy {A1,A2,} formulahalmaz ellentmondásos, ha {A1,A2,}-ből tetszőleges B formula levezethető. A 6.1.21. példa bizonyítja, hogy ha az {A1,A2,} formulahalmazból levezethető valamely A formula és A negáltja is, akkor tetszőleges B formula is levezethető belőle.

6.1.21. PÉLDA. Az {A,¬A} formulahalmazból tetszőleges B formula levezethető. A levezetés:

1.

( ¬ B A ) ( ( ¬ B ¬ A ) B )

[ (A3) ]

2.

A ( ¬ B A )

[ (A1) ]

3.

A

[ hipotézis ]

4.

¬ B A

[ (MP): 2, 3 ]

5.

( ¬ B ¬ A ) B

[ (MP): 1, 4 ]

6.

¬ A ( ¬ B ¬ A )

[ (A1) ]

7.

¬ A

[ hipotézis ]

8.

¬ B ¬ A

[ (MP): 6, 7 ]

9.

B

[ (MP): 5, 8 ]

Table 6.3. Levezetés generálása adott levezetésből

1.

( ¬ B ( ¬ ¬ A ¬ B ) ) ( ¬ B ( ¬ B ( ¬ ¬ A ¬ B ) ) )

2.

¬ B ( ¬ ¬ A ¬ B )

1.

¬ B ( ¬ ¬ A ¬ B )

[(A1)]

3.

¬ B ( ¬ B ( ¬ ¬ A ¬ B ) )

2.

¬ B

[hipotézis]

8.

¬ B ¬ B

3.

¬ ¬ A ¬ B

[(MP): 1, 2]

11.

¬ B ( ¬ ¬ A ¬ B )

4.

( ¬ ¬ A B ) ( ( ¬ ¬ A ¬ B ) ¬ A )

[(A3)]

14.

¬ B ( ¬ ¬ A B ) ( ( ¬ ¬ A ¬ B ) ¬ A )

5.

A B

[hipotézis]

17.

¬ B ( A B )

i.

¬ ¬ A B

[6.18. példa]

j.

¬ B ( ¬ ¬ A B )

(i+1).

( ¬ ¬ A ¬ B ) ¬ A

[(MP): 4, i]

(j+3).

¬ B ( ( ¬ ¬ A ¬ B ) ¬ A )

(j+4).

( ¬ B ( ¬ ¬ A ¬ B ) ¬ A ) ( ¬ B ( ¬ ¬ A ¬ B ) ) ( ¬ B ¬ A )

(j+5).

( ¬ B ( ¬ ¬ A ¬ B ) ) ( ¬ B ¬ A )

(i+2).

¬ A

[(MP): 3, (i+1)]

(j+6).

¬ B ¬ A


6.1.22. TÉTEL. Legyen {A1,A2,} egy formulahalmaz és B egy ítéletlogikai formula.

  1. { A 1 , A 2 , , ¬ B } pontosan akkor ellentmondásos, ha {A1,A2,}0B.

  2. { A 1 , A 2 , , B } pontosan akkor ellentmondásos, ha {A1,A2,}0¬B.

BIZONYÍTÁS.

  1. Nyilvánvaló, hogy {A1,A2,}0B esetén az {A1,A2,,¬B} formulahalmaz ellentmondásos (B és ¬B is levezethető {A1,A2,,¬B}-ből). Fordítva, ha az {A1,A2,,¬B} formulahalmazról tudjuk, hogy ellentmondásos, akkor valamely C formulára

{ A 1 , A 2 , , ¬ B } 0 C és { A 1 , A 2 , , ¬ B } 0 ¬ C .

A dedukciós tétel miatt

{ A 1 , A 2 , } 0 ¬ B C és { A 1 , A 2 , } 0 ¬ B ¬ C .

Konkatenáljuk ezt a két levezetést és írjuk a végére az (A3) axióma

( ¬ B C ) ( ( ¬ B ¬ C ) B )

alakját. Majd válasszuk le a két előtagot a konkatenált levezetésben szereplő ¬BC és ¬B¬C formulákkal, az eredmény {A1,A2,}0B.

  1. Most is {A1,A2,}0¬B-ből az {A1,A2,,B} formulahalmaz ellentmondásossága azonnal következik. Visszafele, ha {A1,A2,,B} ellentmondásos, akkor valamely C formulára

{ A 1 , A 2 , , B } 0 C és { A 1 , A 2 , , B } 0 ¬ C .

Felhasználva azt, hogy ¬¬B0B, megállapíthatjuk, hogy ami levezethető B-ből az levezethető ¬¬B-ből is. Ebből azt kapjuk, hogy

{ A 1 , A 2 , , ¬ ¬ B } 0 C és { A 1 , A 2 , , ¬ ¬ B } 0 ¬ C

szintén fennáll, azaz {A1,A2,,¬¬B} ellentmondásos. Ekkor viszont {A1,A2,}0¬B az 1. eset szerint.

Ezzel mindkét állítást bebizonyítottuk.

6.1.23. TÉTEL. Ha egy {A1,A2,} formulahalmaz ellentmondásos, akkor kielégíthetetlen.

BIZONYÍTÁS. Jelölje Γ az {A1,A2,} formulahalmazt. Ha Γ ellentmondásos, akkor van olyan C formula, melyre Γ0C és Γ0¬C. Ekkor a 6.1.15. tétel miatt Γ0C és Γ0¬C, azaz ha létezik Γ-t kielégítő interpretáció, akkor az kielégíti C-t is, és ¬C-t is, ami lehetetlen. Tehát nincs olyan interpretáció, ami Γ-t kielégítené.

6.1.24. LEMMA. (KALMÁR LÁSZLÓ LEMMÁJA.)

Legyen A tetszőleges ítéletlogikai formula, legyenek az A-ban előforduló ítéletváltozók X1,X2,,Xn és legyen tetszőleges interpretáció. Legyen j=1,2,,n-re

X j { X j , h a ( X j ) = i , ¬ X j e g y é b k é n t , é s A { A , h a ( A ) = i , ¬ A e g y é b k é n t .

Ekkor {X1,X2,,Xn}0A.

BIZONYÍTÁS. Nevezzünk a bizonyítás során egy A ítéletlogikai formulát jónak, ha tetszőleges interpretációban {X1,X2,,Xn}0A. A szerkezeti indukció elve segítségével igazolni fogjuk, hogy minden formula jó.

(alaplépés:) Ha A prímformula, legyen mondjuk X. X igazságtáblája kétsoros, tehát két szekvenciát kell megalapozni:

X

szekvencia

megalapozás

i

{ X } 0 X

X hipotézis

h

{ ¬ X } 0 ¬ X

¬ X hipotézis

Tehát egy prímformula jó.

(indukciós lépések:) Legyen az A formula jó, és legyenek benne az ítéletváltozók X1,X2,,Xn. Vizsgáljuk meg ¬A-t. ¬A igazságtáblája 2n sort tartalmaz, melyek közül valahányban A alatt i, valahányban pedig h igazságérték szerepel. Mivel A jó, az A alatt i-t tartalmazó sorokbeli interpretációkban az {X1,,Xn}0A, a többiben pedig az {X1,,Xn}0¬A szekvenciák megalapozhatók. Ez utóbbi esetben épp ez volt a célunk, míg az előbbi esetben az {X1,,Xn}0¬¬A levezetés megkonstruálásához az {A}0¬¬A szekvenciát kell megalapozni, amit viszont a 6.1.17. példában már megtettünk:

X 1 , , X n

A

¬ A

i

{ X 1 , , X n } 0 A

h

{ A } 0 ¬ ¬ A

6.1.17. példa

h

{ X 1 , , X n } 0 ¬ A

i

{ ¬ A } 0 ¬ A

¬ A hipotézis

Tehát ¬A is jó.

Legyen most az A és a B formula jó, és legyenek bennük az ítéletváltozók X1,X2,,Xn. Vizsgáljuk meg AB-t. AB igazságtáblája is 2n sort tartalmaz, melyek közül valahányban A és B alatt is i, néhányban A alatt i, B alatt h, néhányban épp fordítva: A alatt h, B alatt i, a többiben pedig A és B alatt is h igazságérték szerepel. Mivel A jó, az A alatt i-t tartalmazó sorokbeli interpretációkban az {X1,,Xn}0A, a többiben pedig az {X1,,Xn}0¬A, továbbá mivel B is jó, a B alatt i-t tartalmazó sorokbeli interpretációkban az {X1,,Xn}0B, a többiben pedig az {X1,,Xn}0¬B szekvenciák megalapozhatók. Továbbá az (a) és a (c) esetben a

1.

B A B

[ (A1) ]

2.

B

[ hipotézis ]

3.

A B

[ (MP): 1, 2 ]

levezetés megalapozza az (AB) megfelelő levezetéseit (ugyanis ezekben az esetekben B=B és (AB)=AB).

X 1 , , X n

A

B

A B

(a)

i

i

{ X 1 , , X n } 0 A { X 1 , , X n } 0 B

i

{ A , B } 0 A B

(b)

i

h

{ X 1 , , X n } 0 A { X 1 , , X n } 0 ¬ B

h

{ A , ¬ B } 0 ¬ ( A B )

(c)

h

i

{ X 1 , , X n } 0 ¬ A { X 1 , , X n } 0 B

i

{ ¬ A , B } 0 A B

(d)

h

h

{ X 1 , , X n } 0 ¬ A { X 1 , , X n } 0 ¬ B

i

{ ¬ A , ¬ B } 0 A B

A (d) esetben az

1.

¬ A ¬ B ¬ A

[ (A1) ]

2.

¬ A

[ hipotézis ]

3.

¬ B ¬ A

[ (MP): 1, 2 ]

w .

A B

[6.1. 19. példa ]

levezetés megalapozza {¬A,¬B}0AB-t (A=¬A, B=¬B, (AB)=AB).

A (b) esetben {A,¬B}0¬(AB) fennállását kell belátni (A=A, B=¬B, (AB)=¬(AB)). Az {A,¬B,AB} formulahalmaz ellentmondásos, mivel

{ A , ¬ B , A B } 0 B és { A , ¬ B , A B } 0 ¬ B .

A 6.1.22. tétel miatt {A,¬B}0¬(AB).

Ezzel beláttuk, hogy az AB formula is jó.

Mivel formuláinkban csak a ¬ és a műveleteket engedtük meg, elegendő volt megmutatni az indukciós lépésekben, hogy a tétel fennáll negációs és implikációs formulákra.

6.1.25. TÉTEL. Legyenek {A1,A2,} egy formulahalmaz, B és C ítéletlogikai formulák. Ha {A1,A2,,B}0C és {A1,A2,,¬B}0C, akkor {A1,A2,}0C.

BIZONYÍTÁS. Ha {A1,A2,,B}0C és {A1,A2,,¬B}0C, akkor a 6.1.12. tétel miatt {A1,A2,}0BC és {A1,A2,}0¬BC. A

B C 0 ¬ C ¬ B és ¬ B C 0 ¬ C ¬ ¬ B

szekvenciákat pedig a 6.1.19. példában megalapoztuk. A ¬C¬B és a ¬C¬¬B formulák levezetései konkatenációjának végére írva az (A3) axiómasémából nyert (¬C¬B)((¬C¬¬B)C) axiómaformulát, két leválasztással megkapjuk, hogy {A1,A2,}0C.

6.1.26. TÉTEL. Legyen A ítéletlogikai formula. Ha A tautológia, akkor A bizonyítható, azaz ha 0A, akkor 0A.

BIZONYÍTÁS. (Kalmár László gondolatmenete [31].) Legyenek az A formulában előforduló ítéletváltozók X1,X2,,Xn. Ha az A formula tautológia, akkor az igazságtábla minden sorában i az értéke, tehát a 6.1.24. lemma szerint minden sorban {X1,X2,,Xn}0A. A 6.1.25. tétel ismételt alkalmazásával sorra kiküszöböljük az összes literált a feltételhalmazból. Minden {X1,X2,,Xn} literálhalmazhoz van pontosan egy {¬X1,X2,,Xn} alakú literálhalmaz. Ekkor {X2,,Xn}0A. Ezt folytatva {X2,,Xn}-re kapjuk, hogy 0A.

6.1.27. TÉTEL. (AZ ÍTÉLETKALKULUS GYÖNGE TELJESSÉGE.)

Legyen {A1,A2,,An} véges formulahalmaz és B tetszőleges formula. Ha {A1,A2,,An}0B, akkor {A1,A2,,An}0B.

BIZONYÍTÁS. A szemantikus és a szintaktikus dedukciós tétel miatt elegendő azt belátni, hogy ha 0A1A2AnB, akkor 0A1A2AnB. Feltételeink szerint az A1A2AnB formula tautológia, tehát a 6.1.26. tétel miatt bizonyítható.

Az ítéletlogika szemantikus tárgyalása során a formulahalmazok halmazát két diszjunkt részre osztottuk, a kielégíthetetlen és a kielégíthető formulahalmazok halmazára. Az ítéletkalkulus esetén a formulahalmazok halmazának szintén egy diszjunkt osztályozása az ellentmondásos és az ellentmondástalan formulahalmazok halmazára való szétbontás. A logika különböző tárgyalásai esetén a formulahalmazok diszjunkt felbontását eredményező tulajdonságok egységes megnevezése: konzisztenciainkonzisztencia. Ezek a tulajdonságok – tárgyalásuk során – a tárgyalásmódhoz kötődő megnevezést kapnak. Például szemantikus tárgyalás esetén a konzisztencia (inkonzisztencia) tulajdonságnak a kielégíthetőség (kielégíthetetlenség), a szintaktikus tárgyalások közül a bizonyításelméletben az ellentmondástalanság (ellentmondásosság) a megfelelője. Ha pedig konzisztencia (inkonzisztencia) tulajdonságról beszélünk – egy tárgyalásmód keretei között –, mindig az illető tárgyalásmódbeli megfelelő tulajdonságot értjük rajta.

Érdekes kérdés, hogy a különböző tárgyalásmódok osztályozásai milyen kapcsolatban vannak egymással. Vizsgáljuk most ezt a kapcsolatot szemantikai és bizonyításelméleti tárgyalásmódok esetén. A 6.1.23. tétel szerint minden ellentmondásos formulahalmaz kielégíthetetlen. Ha sikerülne belátni azt, hogy minden ellentmondásmentes formulahalmaz pedig kielégíthető, akkor a kétféle osztályozás eredménye ugyanaz lenne.

6.1.28. DEFINÍCIÓ. Egy Γ formulahalmaz maximális konzisztens (vagy maximális ellentmondásmentes), ha konzisztens (ellentmondásmentes), de tetszőleges AΓ formula esetén Γ{A} már inkonzisztens (ellentmondásos).

6.1.29. TÉTEL. A Γ formulahalmaz akkor és csak akkor maximális konzisztens, ha

  1. Γ konzisztens és

  2. bármely A formulára vagy AΓ, vagy ¬AΓ.

BIZONYÍTÁS.

  1. Ha Γ maximális konzisztens, akkor (1) – a definíció miatt – teljesül. A (2) tulajdonság igazolásához tegyük fel, hogy van olyan A, hogy sem A, sem ¬A nem eleme Γ-nak. Ekkor a maximalitás miatt Γ{A} és Γ{¬A} inkonzisztens. Ez a 6.1. 22. tétel miatt azt jelenti, hogy Γ0¬A és Γ0A, vagyis Γ is inkonzisztens, ami ellentmond a feltételnek, tehát a (2)-nek fenn kell állnia.

  2. Ha pedig Γ-ra (1) és (2) is teljesül, akkor minden olyan Γ formulahalmaz inkonzisztens, amelynek Γ valódi része. Ugyanis legyen Γ az A formulával bővebb, mint Γ. Ekkor (2) miatt ¬AΓ, de Γ Γ , így ¬A Γ . Tehát A Γ és ¬A Γ , ami azt jelenti, hogy Γ inkonzisztens.

Ezzel a tétel bizonyítást nyert.

6.1.30. TÉTEL. Legyen Γ maximális konzisztens formulahalmaz.

  1. A B Γ pontosan akkor, ha ¬AΓ vagy BΓ.

  2. ¬ ( A B ) Γ pontosan akkor, ha AΓ és ¬BΓ.

BIZONYÍTÁS.

  1. Ha ABΓ, de ¬AΓ vagy BΓ nem teljesül, akkor ¬AΓ és BΓ. De mivel Γ maximális, egyrészt Γ¬A is és ΓB is inkonzisztens, másrészt a 6.1.29. tétel szerint AΓ és ¬BΓ. Ugyanakkor tudjuk, hogy ABΓ. Ennek alapján AΓ miatt Γ0B és ¬BΓ miatt Γ0¬B, vagyis Γ inkonzisztens, ellentétben a feltétellel.

Fordított irányban tegyük most fel, hogy ¬AΓ vagy BΓ. Mindkét esetben megmutatjuk, hogy Γ0AB. Ezt elég megmutatni, mert ha Γ0AB mellett ABΓ nem teljesülne, akkor Γ maximalitása miatt ¬(AB)Γ, tehát Γ0¬(AB) következne, azaz a feltételekkel ellentétben Γ inkonzisztens lenne.

  • ¬ A Γ : Ekkor Γ{A} inkonzisztens, tehát bármi levezethető belőle, speciálisan Γ{A}0B, így a dedukciós tétel miatt Γ0AB.

  • B Γ : Ebben az esetben a

1.

B ( A B )

[ (A1) ]

2.

B

[ hipotézis ]

3.

A B

[ (MP): 1, 2 ]

levezetés igazolja állításunkat.

  1. Tegyük fel, hogy ¬(AB)Γ, de AΓ és ¬BΓ nem teljesül, vagyis AΓ vagy ¬BΓ. Ekkor a maximalitás miatt ¬AΓ vagy BΓ. Az első állítás bizonyításánál láttuk, hogy ekkor ABΓ, ellentétben a feltétellel.

Visszafelé, ha AΓ és ¬BΓ, ekkor a Γ{¬A} is, és a Γ{B} is inkonzisztens. Tegyük fel, hogy ¬(AB)Γ, tehát ABΓ. Az első állítás bizonyításánál láttuk, hogy ekkor a feltétellel ellentétben ¬AΓ vagy BΓ lenne.

Ezzel mindkét állítást bebizonyítottuk.

6.1.31. TÉTEL. Tetszőleges konzisztens formulahalmaz kiterjeszthető maximális konzisztens formulahalmazzá.

BIZONYÍTÁS. A bizonyítás konstruktív, vagyis előállít egy a tetszőlegesen rögzített S konzisztens formulahalmazt tartalmazó, maximális konzisztens formulahalmazt. A konstrukció Lindenbaum nevéhez fűződik. Jelölje 0 az összes ítéletlogikai formulának a halmazát. Az 0 megszámlálhatóan végtelen halmaz elemeinek legyen {A1,A2,} egy felsorolása. A konstrukció a következő. Legyen S0 az S konzisztens formulahalmaz, és minden i=1,2,-re ha Si1-et már megkonstruáltuk, akkor

S i { S i 1 { A i } , ha S i 1 { A i } konzisztens , S i 1 egyébként .

Megmutatjuk, hogy az így kapott S0S1 konzisztens formulahalmazlánc elemeinek uniója egy Γ maximális konzisztens formulahalmaz.

  • Lássuk be először, hogy Γ konzisztens. Tegyük fel, hogy nem az. Ekkor Γ-ból levezethető valamely A és ¬A is. Legyenek B1,B2,,Bj a levezetésekben előforduló Γ-beli formulák. Mivel ezek a levezetések véges sok formulából állnak, van olyan i, hogy {B1,B2,,Bj}Si. De ez azt jelentené, hogy Si-nek van inkonzisztens részhalmaza, tehát Si inkonzisztens, ellentétben a konstrukcióval. Ez ellentmondás, tehát Γ konzisztens.

  • Lássuk be ezután, hogy Γ maximális is. Tegyük fel, hogy Γ konzisztens és Γ Γ . Belátjuk, hogy Γ= Γ , vagyis ha Ak Γ , akkor AkΓ is. Tegyük fel, hogy Ak Γ , de AkΓ. Konstrukciónk szerint az, hogy AkΓ, azt jelenti, hogy Sk1{Ak} inkonzisztens. Másrészt Sk1Γ Γ és Ak Γ , ami miatt Γ is inkonzisztens volna.

Tehát a tételt igazoltuk.

6.1.32. TÉTEL. A maximális konzisztens formulahalmazok kielégíthetők.

BIZONYÍTÁS. Legyen Γ maximális konzisztens formulahalmaz. A 6.1.29. tétel (b) állítása miatt tetszőleges X ítéletváltozó esetén az X és a ¬X literáloknak pontosan az egyike eleme Γ-nak. Tekintsük a következő interpretációt.

( X ) { i ha X Γ , h ha ¬ X Γ .

Megmutatjuk, hogy tetszőleges A formulára AΓ akkor és csak akkor, ha (A)=i.

(alaplépés:) Ha AΓ és az A formula literál, akkor A=X esetén (X)=(X)=i és A=¬X esetén (¬X)=¬(X)=i.

(indukciós lépések:) Tegyük fel, hogy ¬AΓ. Ekkor AΓΓ maximális konzisztenciája (6.1.29. tétel) miatt. Az indukciós feltétel szerint ekkor (A)=h. De (¬A) éppen ¬(A), tehát (¬A)=i. Fordítva, legyen (¬A)=i. Ekkor (A)=h, az indukciós feltétel szerint viszont így AΓ. A 6.1.29. tétel miatt tehát ¬AΓ.

Tegyük fel most, hogy ABΓ. Ekkor Γ a 6.1.30. tétel szerint ¬AΓ vagy BΓ. Az indukciós hipotézis alapján (¬A)=i vagy (B)=i, ami azt biztosítja, hogy (AB)=i. Fordítva, ha (AB)=i, akkor (¬A)=i vagy (B)=i. Az indukciós feltétel miatt ebben az esetben ¬AΓ vagy BΓ, így a 6.1.30. tétel miatt (AB)Γ.

Azaz tetszőleges AΓ formulára (A)=i, így a kielégíti Γ-t.

6.1.33. TÉTEL. Tetszőleges konzisztens formulahalmaz kielégíthető.

BIZONYÍTÁS. A 6.1.31. tétel szerint tetszőleges S konzisztens formulahalmaz kiterjeszthető egy Γ maximális konzisztens formulahalmazzá. A 6.1.32. tétel miatt egy maximális konzisztens formulahalmaz kielégíthető. Egy kielégíthető formulahalmaz minden részhalmaza kielégíthető, ezért – mivel SΓS is kielégíthető.

6.1.34. TÉTEL. Egy formulahalmaz pontosan akkor kielégíthetetlen, ha inkonzisztens.

BIZONYÍTÁS. Beláttuk, hogy ha egy formulahalmaz konzisztens, akkor kielégíthető (6.1.33. tétel). Beláttuk azt is (6.1.23. tétel), hogy ha egy formulahalmaz inkonzisztens, akkor kielégíthetetlen. Ebből következik, hogy egy formulahalmaz akkor és csak akkor inkonzisztens, ha kielégíthetetlen.

6.1.35. TÉTEL. (AZ ÍTÉLETKALKULUS TELJESSÉGE.)

Legyen {A1,A2,} tetszőleges, nem feltétlenül véges formulahalmaz és B tetszőleges formula. Ha {A1,A2,}0B, akkor {A1,A2,}0B.

BIZONYÍTÁS. (A Gödel-féle gondolatmenet.) Ha {A1,A2,}0B, akkor a 4.4.4. tétel szerint {A1,A2,,¬B} kielégíthetetlen. A 6.1.34. tétel miatt a kielégíthetetlen formulahalmazok ellentmondásosak is, tehát {A1,A2,,¬B} ellentmondásos. A 6.1.22. tétel azt mondja, hogy ha {A1,A2,,¬B} ellentmondásos, akkor {A1,A2,}0B. Ezzel a tételt bebizonyítottuk.

Azt kaptuk tehát, hogy a szintaktikus és szemantikus következményfogalom azonos egymással, azaz a (szemantikusan) helyes következtetések formálisan bizonyíthatók, valamint hogy minden szintaktikus következmény egyben szemantikus következmény is. Az ítéletkalkulus teljessége azt jelenti, hogy az ítéletlogikát fel lehet építeni szintaktikai alapokon és ez a felépítés ekvivalens a szemantikai alapú felépítéssel. Szokás ezt úgy is fogalmazni, hogy az ítéletlogika minden tautológiája (a bizonyításelmélet eszközeivel) bizonyítható.

Az ítéletlogika nyelvére is felépíthetjük az ítéletkalkulust. Ilyenkor gondoskodunk konjunkciós és diszjunkciós formulákra vonatkozó axiómasémákról, illetve levezetési szabályokról is. Bővítsük ki például az ítéletkalkulus axiómasémáinak rendszerét az (A4)–(A10) axiómasémákkal, és a levezetési szabály továbbra is egyedül a modus ponens legyen.

(A1)

X ( Y X )

(A2)

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

(A3)

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

(A4)

¬ ¬ X X

(A5)

X ( Y X Y )

(A6)

X Y X

(A7)

X Y Y

(A8)

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

(A9)

X X Y

(A10)

Y X Y

A levezetés és a levezethetőség definícióját ne változtassuk. (Természetesen a levezetésben az új kalkulusban mindig leírhatunk egy új axiómasémából nyert formulát is.) Világos, hogy ha {A1,A2,}0B, akkor az {A1,A2,} hipotézisekből ebben a bővebb axiómaséma-halmazzal rendelkező kalkulusban is levezethető lesz B. Fordítva, ha B a bővebb axiómaséma-halmazzal rendelkező kalkulusban vezethető le az {A1,A2,} hipotézisekből, akkor könnyű belátni, hogy az eredeti kalkulusban is le lehet vezetni B-t (vagy egy vele ekvivalens, csak ¬-t és -t tartalmazó formulát) {A1,A2,}-ből. Az új axiómasémák ugyanis tautológiák, így az ítéletkalkulusban mindegyik bizonyítható, tehát hipotézismentesen levezethető. Így egy az új kalkulusban adott levezetésből mindig előállítható az eredeti kalkulusbeli levezetés úgy, hogy a levezetésben az új axiómaformulák helyére beírjuk a levezetésüket. Tehát a két kalkulusban minden formulahalmazból pontosan ugyanazok a formulák lesznek levezethetők, a két kalkulus ekvivalens.

Egy másik lehetőség az ítéletkalkulusnak az ítéletlogika nyelvéhez illesztésére, hogy új levezetési szabályok bevezetése mellett változatlanul hagyjuk az axiómasémák halmazát. Ekkor az (A4)–(A10) tautológiákat levezetési szabályként használjuk fel. Például 0AAB az (A9)-nek megfelelő elemi levezetés, amelyből a dedukciós tétellel azt kapjuk, hogy A0AB, amit így használhatunk mint levezetési szabályt. A levezetés és a levezethetőség definícióját most se változtassuk. (Természetesen a levezetés során ebben a kalkulusban mindig leírhatunk egy – a már a levezetésben szereplő formulá(k)ból – az új levezetési szabállyal (szabályokkal) nyert formulát is.) Könnyen belátható, hogy egy így nyert kalkulus is ekvivalens az előzőekkel.

A predikátumkalkulus

Az elsőrendű logika bizonyításelméleti tárgyalását mint kalkulust szokás predikátumkalkulusnak vagy logikai függvénykalkulusnak nevezni. Az elsőrendű logika bizonyításelméleti eszközökkel való felépítéséhez bevezetünk elsőrendű formulákat mint ,,alapigazságokat – axiómasémákat” és egy levezetési szabályt, a modus ponenst. Definiáljuk a levezethetőség fogalmát és meghatározzuk, ha lehet, az eldöntésproblémát. Elegendő a kvantort és a ¬, logikai összekötőjeleket bevenni az elsőrendű nyelv ábécéjébe, így az axiómarendszerben a három, az ítéletkalkulusból már ismert sémán kívül az univerzális kvantorra vonatkozó axiómasémák fognak megjelenni. A predikátumkalkulus axiómaformuláit úgy kapjuk, hogy az axiómasémákban az A,B és a C betűk helyére az adott elsőrendű logikai nyelv tetszőleges formuláit, x helyére a nyelv valamely változóját és t helyére a nyelv valamely termjét írjuk, illetve egy így nyert formulát általánosítunk.

Table 6.4. A predikátumkalkulus axiómasémái

(B1)

A ( B A )

(B2)

( A ( B C ) ) ( ( A B ) ( A C ) )

(B3)

( ¬ A B ) ( ( ¬ A ¬ B ) A )

(B4)

x A [ A ( x t ) ]

(B5)

x ( A B ) ( x A x B )

(B6)

A x A , ahol xPar (A)

(B7)

a (B1)–(B6) axiómák általánosításai


A predikátumkalkulus levezetési szabálya is a modus ponens, az 5.4.13. tételből tudjuk, hogy ({AB,A},B) az elsőrendű logikában is helyes következtetési forma.

Table 6.5. A predikátumkalkulus levezetési szabálya

(MP)

{ A B , A } B


A levezetés definíciója formailag megegyezik az ítéletlogikában megadottal, csak most a definícióban hivatkozott axiómaformulák a predikátumkalkulus axiómaformulái.

6.1.36. DEFINÍCIÓ. Legyen {A1,A2,} egy elsőrendű logikai nyelv formuláinak tetszőleges, esetleg üres halmaza és B a nyelv egy formulája. Az {A1,A2,} formulahalmazból a B formula predikátumkalkulusbeli levezetése egy olyan D1,D2,,Dm(m1) formulasorozat, ahol minden j=1,2,,m-re Dj

  1. vagy eleme az {A1,A2,} formulahalmaznak, azaz hipotézis,

  2. vagy a (B1)–(B7) axiómasémák szerint nyert formula, azaz axiómaformula,

  3. vagy van olyan 1s,tj, hogy a Ds és a Dt formulákból levezetési szabállyal állt elő,

és a formulasorozat utolsó tagja, Dm, éppen a B formula.

6.1.37. DEFINÍCIÓ. Legyen {A1,A2,} egy elsőrendű logikai nyelv formuláinak tetszőleges, esetleg üres halmaza és B a nyelv egy formulája. Azt mondjuk, hogy B az {A1,A2,} formulahalmazból a predikátumkalkulusban levezethető, ha B-nek van az {A1,A2,} formulahalmazból (predikátumkalkulusbeli) levezetése. Jelölése {A1,A2,}B.

A levezethetőség a predikátumkalkulus következményfogalma, amely szintén szintaktikus következményfogalom.

6.1.38. DEFINÍCIÓ. Legyen B egy elsőrendű logikai nyelv formulája. B a predikátumkalkulusban bizonyítható, ha van hipotézismentes levezetése (azaz levezethető az üres feltételformula-halmazból). Ebben az esetben a B jelölést alkalmazzuk.

6.1.39. PÉLDA. Most megmutatjuk, hogy a xyQ(x,y)Q(x,y) szekvencia megalapozható a predikátumkalkulusban.

1.

x y Q ( x , y )

[ hipotézis ]

2.

x y Q ( x , y ) y Q ( x , y )

[ (B4) ]

3.

y Q ( x , y )

[ (MP): 1, 2 ]

4.

y Q ( x , y ) Q ( x , y )

[ (B4) ]

5.

Q ( x , y )

[ (MP): 3, 4 ]

Az ítélet- és a predikátumkalkulusban való levezetés definíciója tehát csak abban különbözik egymástól, hogy a predikátumkalkulusban való levezetésben az ítéletkalkulus axiómáin kívül újabb axiómákat is használhatunk. Nyilván előfordulhat az is, hogy a predikátumkalkulusban való levezetésben csak a (B1)–(B3) sémákból – az ítéletkalkulus sémáiból – előállított axiómák szerepelnek. Ha egy B formula predikátumkalkulusbeli levezetése az {A1,A2,} hipotézisekből (vagy hipotézismentesen) ilyen, használjuk a {A1,A2,}0B(0B) jelölést. Világos, hogy ha {A1,A2,}0B, akkor {A1,A2,}B, illetve ha 0B, akkor B. Nyilvánvaló az is, hogy ítéletkalkulusnak a levezetéssel kapcsolatos tételei, vagyis azok a tételek, amelyeknek a bizonyításában a levezetés tulajdonságait használjuk ki, a predikátumkalkulusban is érvényesek maradnak. Ezeket a tételeket bizonyítás nélkül adjuk meg.

6.1.40. TÉTEL. (DEDUKCIÓS TÉTEL.)

Legyenek A1,A2,,An,B(n1) egy elsőrendű logikai nyelv formulái. {A1,A2,,An1,An}B pontosan akkor, ha {A1,A2,,An1}AnB.

6.1.41. TÉTEL. (AZ ELDÖNTÉSPROBLÉMA TÉTELE.)

Legyenek A1,A2,,An,B(n1) egy elsőrendű logikai nyelv formulái. {A1,A2,,An1,An}B pontosan akkor, ha A1A2An1AnB.

6.1.42. TÉTEL. (A PREDIKÁTUMKALKULUS HELYESSÉGE.)

Legyenek A1,A2,,B egy elsőrendű logikai nyelv formulái. Ha {A1,A2,}B, akkor {A1,A2,}B.

6.1.43. PÉLDA. Bizonyítsuk be a predikátumkalkulusban a xP(x)yP(y) formulát. A dedukciós tétel a predikátumkalkulusban is érvényes, így elég megadni yP(y) levezetését a xP(x) hipotézisből. Ebből a levezetésből a 6.1.12. tétel bizonyításában megtanult módszerrel könnyen megkonstruálható xP(x)yP(y) hipotézismentes levezetése is.

1.

x P ( x )

[ hipotézis ]

2.

x P ( x ) y x P ( x )

[ (B6) ]

3.

y x P ( x )

[ (MP): 1, 2 ]

4.

y ( x P ( x ) P ( y ) )

[ (B4) általánosítása ]

5.

y ( x P ( x ) P ( y ) ) ( y x P ( x ) y P ( y ) )

[ (B5) ]

6.

y x P ( x ) y P ( y )

[ (MP): 4, 5 ]

7.

y P ( y )

[ (MP): 3, 6 ]

6.1.44. TÉTEL. (AZ ÁLTALÁNOSÍTÁS SZABÁLYA.)

Legyenek A1,A2,,B egy elsőrendű logikai nyelv formulái és x egy olyan változó, hogy xPar (Ai). Ha {A1,A2,}B, akkor {A1,A2,}xB.

BIZONYÍTÁS. Jelölje Γ az {A1,A2,} formulahalmazt. ΓB azt jelenti, hogy B-nek van levezetése Γ-ból. Legyen ez a levezetés D1,D2,,Dm=B. A bizonyítás a következő lépésekből áll:

  • Írjuk a levezetésben szereplő formulák elé a x prefixumot. Így a xD1,xD2,,xDm=xB formulasorozatot kapjuk.

  • Lássuk be, hogy minden k-ra (1km) létezik xDk-nak Γ-ból való levezetése.

    1. Legyen Dk axiómaformula, ekkor xDk is – (B7) miatt – axiómaformula.

    2. Legyen Dk eleme a Γ-nak. Ekkor xPar (Dk) és xDk levezethető Γ-ból. A levezetés:

1.

D k x D k

[ (B6) ]

2.

D k

[ hipotézis ]

3.

x D k

[ (MP): 1, 2 ]

  1. Legyen Dk az első olyan (eddig még nem vizsgált) formula az eredeti levezetésben, amely modus ponense Dt,Ds=DtDk levezetésbeli formuláknak (s,tk). Ez azt jelenti, hogy már igazoltuk, hogy Γ-ból a x(DtDk), valamint a xDt formula levezethető:

i .

x ( D t D k )

j .

x D t

w .

x ( D t D k ) ( x D t ) x D k

[ (B5) ]

( w + 1 ) .

x D t x D k

[ (MP): i, w ]

( w + 2 ) .

x D k

[ (MP): j, (w+1) ]

Indukcióval könnyen bizonyítható, hogy ΓxDk akkor is, ha Dk tetszőleges – nem feltétlen az első – olyan formula az eredeti levezetésben, amelyet modus ponenssel nyertünk.

  • A xDk formulák elé (1km) beírjuk azok levezetését Γ-ból. Ezzel Γ-ból való levezetések konkatenációját kapjuk, ami a Γ-ból való levezetése a xB formulának.

Ezzel a tételt bebizonyítottuk.

6.1.45. PÉLDA. Bizonyítsuk be a xP(x)yP(y) formulát az általánosítás szabálya (6.1.44. tétel) felhasználásával is. A dedukciós tétel a xP(x)yP(y) szekvenciát kell megalapozni, ehhez pedig az általánosítás szabálya miatt elég a xP(x)P(y) szekvenciát igazolni.

1.

x P ( x )

[ hipotézis ]

2.

x P ( x ) P ( y )

[ (B4) ]

3.

P ( y )

[ (MP): 1, 2 ]

Könnyű észrevenni, hogy ebből a levezetésből a 6.1.44. tétel bizonyításában megismert módszerrel is megkonstruálható a 6.1.43. példabeli levezetés.

Most a szemantikus tárgyalásnál definiált logikai ekvivalencia fogalom bizonyításelméleti megfelelőjét definiáljuk:

6.1.46. DEFINÍCIÓ. Azt mondjuk, hogy az A és a B elsőrendű logika formulák bizonyíthatóan ekvivalensek, ha {A}B és {B}A.

6.1.47. PÉLDA. Igazoljuk, hogy az RxP(x) és a x(RP(x)) formulák bizonyíthatóan ekvivalensek (xPar (R)).

  1. A x(RP(x))RxP(x) szekvencia megalapozásához a dedukciós tétel miatt elég a x(RP(x)),RxP(x) szekvenciát megalapozni, ezt meg az általánosítás szabálya miatt a x(RP(x)),RP(x) levezetés megkonstruálásával igazolhatjuk:

1.

x ( R P ( x ) )

[ hipotézis ]

2.

x ( R P ( x ) ) ( R P ( x ) )

[ (B4) ]

3.

R P ( x )

[ (MP): 1, 2 ]

4.

R

[ hipotézis ]

5.

P ( x )

[ (MP): 3, 4 ]

  1. Az RxP(x)x(RP(x)) szekvencia megalapozásához igazoljuk, hogy RxP(x)RP(x), majd alkalmazzuk az általánosítás szabályát.

1.

x P ( x ) P ( x )

[ (B4) ]

2.

( x P ( x ) P ( x ) ) ( R ( x P ( x ) P ( x ) ) )

[ (B1) ]

3.

R ( x P ( x ) P ( x ) )

[ (MP): 1, 2 ]

4.

( R ( x P ( x ) P ( x ) ) ) ( ( R x P ( x ) ) ( R P ( x ) ) )

[ (B2) ]

5.

( R x P ( x ) ) ( R P ( x ) )

[ (MP): 3, 4 ]

6.

R x P ( x )

[ hipotézis ]

7.

R P ( x )

[ (MP): 5, 6 ]

6.1.48. DEFINÍCIÓ. Azt mondjuk, hogy elsőrendű logikai formulák egy {A1,A2,} halmaza ellentmondásos, ha van olyan A formula, hogy {A1,A2,}-ből A is, és ¬A is levezethető. Egyébként {A1,A2,}ellentmondásmentes.

6.1.49. TÉTEL. Legyen {A1,A2,} egy elsőrendű logikai nyelv formuláinak tetszőleges halmaza és B a nyelv egy formulája.

  1. { A 1 , A 2 , , ¬ B } pontosan akkor ellentmondásos, ha {A1,A2,}B.

  2. { A 1 , A 2 , , B } pontosan akkor ellentmondásos, ha {A1,A2,}¬B.

6.1.50. TÉTEL. Ha egy {A1,A2,} elsőrendű formulahalmaz ellentmondásos, akkor kielégíthetetlen.

6.1.51. TÉTEL. Legyenek {A1,A2,} egy elsőrendű formulahalmaz, B és C elsőrendű logikai formulák. Ha {A1,A2,,B}C és {A1,A2,,¬B}C, akkor {A1,A2,}C.

6.1.52. TÉTEL. (A PREDIKÁTUMKALKULUS TELJESSÉGE.)

Legyen {A1,A2,} egy elsőrendű logikai nyelv formuláinak tetszőleges (nem feltétlenül véges) halmaza és B tetszőleges formula. Ha {A1,A2,}B, akkor {A1,A2,}B.

A predikátumkalkulus teljességének bizonyításához meg kell mutatni, hogy minden elsőrendű konzisztens (ellentmondásmentes) formulahalmaz kielégíthető. Ehhez viszont szükség van a következő tételek igazolására:

  • Tetszőleges elsőrendű konzisztens formulahalmaz kiterjeszthető maximális konzisztens formulahalmazzá.

  • Egy elsőrendű maximális konzisztens formulahalmaz kielégíthető.

A teljességi tételt Henkin 1949-ben bizonyította be. Ennek a bizonyításnak az ismertetése túlnő a könyv keretein, a szakirodalomban viszont több helyen is megtalálható [7,29,60].

Azt kaptuk tehát, hogy a megadott szintaktikus és szemantikus következményfogalom az elsőrendű logikában is azonos egymással, azaz a (szemantikusan) helyes következtetések formálisan bizonyíthatók, valamint hogy minden szintaktikus következmény egyben szemantikus következmény is. A predikátumkalkulus helyessége és teljessége azt jelenti, hogy az elsőrendű logikát fel lehet építeni szintaktikai alapokon és ez a felépítés ekvivalens a szemantikai alapú felépítéssel.

Legyen [Vν] egy – az 5.1. fejezetben definiált – elsőrendű logikai nyelv. Az [Vν] nyelvre is felépíthetjük a predikátumkalkulust. Ilyenkor gondoskodunk konjunkciós, diszjunkciós és egzisztenciálisan kvantált formulákra vonatkozó axiómasémákról is. A levezetési szabály továbbra is a modus ponens legyen.

(C1)

A ( B A )

(C2)

( A ( B C ) ) ( ( A B ) ( A C ) )

(C3)

( ¬ A B ) ( ( ¬ A ¬ B ) A )

(C4)

¬ ¬ A A

(C5)

A ( B A B )

(C6)

A B A

(C7)

A B B

(C8)

( A C ) ( ( B C ) ( A B C ) )

(C9)

A A B

(C10)

B A B

(C11)

x A [ A ( x t ) ]

(C12)

x ( B A ) ( B x A ) , ahol xPar (B)

(C13)

[ A ( x t ) ] x A

(C14)

x ( A B ) ( x A B ) , ahol xPar (B).

(C15)

A x A , ahol xPar (A)

(C16)

a (C1)–(C15) axiómák általánosításai

A levezetés definícióját módosítsuk úgy, hogy az új kalkulusban a levezetés során mindig leírhassunk egy új axiómasémából nyert formulát is. Be lehet látni, hogy ha {A1,A2,}B, akkor az {A1,A2,} hipotézisekből az új kalkulusban is levezethető lesz B. Fordítva, ha B az új kalkulusban vezethető le az {A1,A2,} hipotézisekből, akkor az eredeti kalkulusban is le lehet vezetni B-t (vagy egy vele ekvivalens, csak ¬, és logikai jeleket tartalmazó formulát) {A1,A2,}-ből. Az új axiómasémák ugyanis logikailag igazak, tehát az eredeti predikátumkalkulusban mindegyik bizonyítható, azaz hipotézismentesen levezethető. Így egy az új kalkulusban adott levezetésből mindig előállítható az eredeti kalkulusbeli levezetés úgy, hogy a levezetésben az új axiómaformulák helyére beírjuk a levezetésüket. Tehát a két kalkulusban minden formulahalmazból pontosan ugyanazok a formulák lesznek levezethetők, a két kalkulus ekvivalens.

A 3.3. fejezetben említést tettünk az egyenlőségjeles elsőrendű logikai nyelvről. Ha a nyelvünk ilyen, a kalkulusban megjelennek további, az egyenlőség predikátumra vonatkozó axiómasémák is, melyeket (D7)–(D9)-cel jelölünk. Az egyenlőségjeles predikátumkalkulus axiómasémái például a következők:

(D1)

A ( B A )

(D2)

( A ( B C ) ) ( ( A B ) ( A C ) )

(D3)

( ¬ A B ) ( ( ¬ A ¬ B ) A )

(D4)

x A [ A ( x t ) ]

(D5)

x ( A B ) ( x A x B )

(D6)

A x A , ahol xPar(A)

(D7)

t = t

(D8)

t 1 = t n + 1 t n = t 2 n f ( t 1 , t 2 , , t n ) = f ( t n + 1 , t n + 2 , , t 2 n )

(D9)

t 1 = t n + 1 t n = t 2 n P ( t 1 , t 2 , , t n ) P ( t n + 1 , t n + 2 , , t 2 n )

(D10)

a (D1)–(D9) axiómák általánosításai

A levezetési szabálynak megtartjuk a modus ponenst. Be lehet bizonyítani, hogy az egyenlőségjeles predikátumkalkulus is helyes és teljes kalkulus. Ezzel a bizonyítással nem foglalkozunk.

Feladatok

6.1.1. FELADAT. Legyen Γ formulahalmaz, B és C formulák. Igazoljuk, hogy ha Γ0B és Γ{B}0C, akkor Γ0C.

6.1.2. FELADAT. Bizonyíthatók-e a predikátumkalkulusban az alábbi formulák. Ha igen, adjuk meg egy-egy levezetésüket.

  1. x y Q ( x , y ) y x Q ( x , y )

  2. x y Q ( x , y ) y x Q ( x , y )

  3. x y Q ( x , y ) y x Q ( x , y )

  4. ( x P ( x ) x R ( x ) ) x ( P ( x ) R ( x ) )