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 5. Az elsőrendű logika

Chapter 5. Az elsőrendű logika

Ebben a fejezetben az elsőrendű logikával vagy más néven predikátumlogikával foglalkozunk. Az elsőrendű logikában az egyszerű állítások belső szerkezetét is feltárjuk. A leíráshoz használt nem logikai eszközök az individuumnevek és a predikátumok. Ezek matematikai és logikai függvények. Segítségükkel egy individuumhalmaz – univerzum – konkrét elemeivel kapcsolatos állításokat fogalmazhatunk meg. A teljes univerzumra vonatkozó állítások szerkezetének leírásához szükségünk van az individuumhalmaz elemeit befutó individuumváltoókra és az univerzális és az egzisztenciális kvantorokra. Ha az állításoknak ezekkel az eszközökkel a belső szerkezetét is feltárjuk, kiderülhet, hogy a szerkezetükben közös – logikán kívüli – komponensek is vannak, tehát jelentésük sem feltétlen független egymástól.

Az elsőrendű logikában is a formulákat fogjuk tanulmányozni. Az ítéletlogikával szemben lehetővé tesszük ugyanakkor

  • az egyszerű állítások szerkezetét is feltáró leírást,

  • az elsőrendű állítások igazságértékének meghatározását,

  • a helyes következtetés fogalmának árnyaltabb definiálását, és

  • ezen definíciót figyelembe vevő döntési eljárás megfogalmazását a helyes következtetéssel kapcsolatban.

Elsőrendű logikai nyelvek – szintaxis

Egy elsőrendű logikai nyelv ábécéje logikai és logikán kívüli szimbólumokat, továbbá elválasztójeleket tartalmaz. A logikán kívüli szimbólumhalmaz megadható Srt,Pr,Fn,Cnst alakban, ahol

  1. Srt nemüres halmaz, elemei fajtákat szimbolizálnak,

  2. Pr nemüres halmaz, elemei predikátumszimbólumok,

  3. az Fn halmaz elemei függvényszimbólumok,

  4. Cnst pedig a konstansszimbólumok halmaza.

Az Srt,Pr,Fn,Cnst ábécé szignatúrája egy (ν1,ν2,ν3) hármas, ahol

  1. minden PPr predikátumszimbólumhoz ν1 a predikátumszimbólum alakját, azaz a (π1,π2,,πk) fajtasorozatot,

  2. minden fFn függvényszimbólumhoz ν2 a függvényszimbólum alakját, azaz a (π1,π2,,πk,π) fajtasorozatot és

  3. minden cCnst konstansszimbólumhoz ν3 a konstansszimbólum fajtáját, azaz (π)-t

rendel (k0ésπ1,π2,,πk,πSrt).

Logikai jelek az ítéletlogika nyelvében is használt ¬,,, logikai összekötőjelek, továbbá az és az kvantorok és a különböző fajtájú individuumváltozók. Egy elsőrendű nyelv ábécéjében minden πSrt fajtához szimbólumoknak megszámlálhatóan végtelen

v 1 π , v 2 π ,

rendszere tartozik, ezeket a szimbólumokat nevezzük πfajtájú változóknak. Elválasztójel a nyitó és a záró zárójel mellett a vessző.

Az elsőrendű logikai nyelvek ábécéiben a logikai jelek és elválasztójelek lényegében mindig ugyanazok, a logikán kívüli jelek halmaza, illetve ezek szignatúrája viszont nyelvről nyelvre lényegesen különbözhet. Ezért mindig megadjuk az Srt,Pr,Fn,Cnst halmaznégyest és ennek (ν1,ν2,ν3) szignatúráját, amikor egy elsőrendű logikai nyelv ábécéjére hivatkozunk. Jelölése: V[Vν], ahol Vν adja meg a (ν1,ν2,ν3) szignatúrájú Srt,Pr,Fn,Cnst halmaznégyest.

5.1.1. DEFINÍCIÓ. A V[Vν] ábécé feletti termek halmaza a legszűkebb olyan tulajdonságú szóhalmaz, amelynek

  1. minden változó és konstans – a fajtáját megőrző – szava, továbbá

  2. ha az fFn függvényszimbólum (π1,π2,,πk,π) alakú és az s1,s2,,sk – rendre π1,π2,,πk fajtájú – szavak elemei a szóhalmaznak, akkor az f(s1,s2,,sk)π fajtájú – szó is eleme a szóhalmaznak.

A 4.1.1. definíció után leírt gondolatmenethez hasonlóan be lehet látni, hogy a definícióban hivatkozott szóhalmaz egyértelműen létezik. Jelöljük ezt a szóhalmazt t[Vν]-vel.

5.1.2. DEFINÍCIÓ. A V[Vν] ábécé feletti elsőrendű formulák halmaza a legszűkebb olyan tulajdonságú szóhalmaz, amelynek

  1. ha a PPr predikátumszimbólum (π1,π2,,πk) alakú és az s1,s2,,sk – rendre π1,π2,,πk fajtájú – szavak elemei t[Vν]-nek, akkor a P(s1,s2,,sk) szó eleme,

  2. ha S eleme a szóhalmaznak, akkor ¬S is eleme,

  3. ha S és T elemei a szóhalmaznak és binér logikai összekötőjel, akkor (ST) is eleme és

  4. ha S eleme a szóhalmaznak, Q kvantor és x tetszőleges változó, akkor QxS is eleme.

Ugyancsak a 4.1.1. definíció után megadott gondolatmenet szerint lehet belátni, hogy az itt hivatkozott halmaz is egyértelműen létezik. Jelöljük ezt a halmazt f[Vν]-vel. Egy V[Vν] ábécé feletti nyelv termjei t[Vν] és formulái f[Vν] halmazának uniója adja a V[Vν] ábécé feletti elsőrendű logikai nyelvet. Jelöljük ezt a nyelvet [Vν]-vel.

Ezek után könnyű megadni egy elsőrendű logikai nyelv szintaxisát, vagyis azokat a szabályokat, amelyek alapján elő lehet állítani a nyelv ábécéjének jeleiből [Vν] szavait. Ezeknek a szabályoknak megfelelően előállított szavakat nevezzük az elsőrendű logikai nyelv termjeinek és formuláinak (néha hangsúlyozottan: jólformált termeknek, jólformált formuláknak). A nyelv termjeit és formuláit a nyelv kifejezéseiként is szoktuk emlegetni. A szintaktikai szabályok alapján egy elsőrendű nyelvben is el lehet dönteni, hogy egy, az ábécé feletti szó a nyelv kifejezése-e. A termeket a továbbiakban általában s,t,, a formulákat az A,B,C, betűkkel, vagy indexelt változataikkal jelöljük.

5.1.3. DEFINÍCIÓ. ((Vν) SZINTAXISA.)

  1. Minden πSrt fajtájú változó és konstans π fajtájú term.

  2. Ha az fFn függvényszimbólum (π1,π2,,πk,π) alakú és t1,t2,,tk – rendre π1,π2,,πk fajtájú – termek, akkor az f(t1,t2,,tk) szó egy π fajtájú term.

  3. Minden term az 1–2. szabályok véges sokszori alkalmazásával áll elő.

  4. Ha a PPr predikátumszimbólum (π1,π2,,πk) alakú és t1,t2,,tk – rendre π1,π2,,πk fajtájú – termek, akkor a P(t1,t2,,tk) szó egy elsőrendű formula. Az így nyert formulákat atomi formuláknak nevezzük.

  5. Ha A elsőrendű formula, akkor ¬A is az.

  6. Ha A és B elsőrendű formulák és binér logikai összekötőjel, akkor (AB) is elsőrendű formula.

  7. Ha A elsőrendű formula, Q kvantor és x tetszőleges változó, akkor QxA is elsőrendű formula. Az így nyert formulákat kvantált formuláknak nevezzük.

  8. Minden elsőrendű formula a 4–7. szabályok véges sokszori alkalmazásával áll elő.

Világos, hogy [Vν] minden szava vagy term, vagy formula, hisz a szintaktikai szabályok segítségével előállított szavak egy-egy az 5.1.1. definíció szerinti 1–2. tulajdonságú és az 5.1.2. definíció szerinti 1–4. tulajdonságú szóhalmazt alkotnak, továbbá t[Vν] és f[Vν] a legszűkebb ilyen halmazok, [Vν] pedig ezek uniója.

Hasonlóan, mint az ítéletlogikában, ha egy elsőrendű formula ¬A alakú, negációs, ha (AB) alakú, konjunkciós, ha (AB) alakú, diszjunkciós, ha pedig (AB) alakú, implikációs formula. A xA alakú formulákat univerzálisan, a xA alakú formulákat egzisztenciálisan kvantált formuláknak nevezzük. A QxA kvantált formulában Qx a formula prefixuma, A pedig a formula magja. A negációs, konjunkciós, diszjunkciós, implikációs és kvantált formulák összetett formulák.

Az ítéletlogikában használtuk a prímformula fogalmát. A prímformulákból a ¬,,, logikai összekötőjelek segítségével minden ítéletlogikai formulát fel tudtunk építeni. Egy elsőrendű logikai nyelvben is vannak ilyen formulák: a nyelv atomi formulái és a kvantált formulák. Ezek a formulák az elsőrendű logikai nyelv prímformulái.

5.1.4. PÉLDA. Legyen Vν a {π1,π2},{P,Q,R},{f},{c} halmaznégyes a következő szignatúrával:

v 1

v 2

v 3

P

( π 1 )

f

( π 1 , π 2 , π 2 )

c

( π 1 )

Q

( π 1 , π 2 )

R

( π 2 , π 2 )

Legyenek x,y,z,π1 fajtájú és x˜,y˜,z˜ pedig π2 fajtájú változók. Jelöljük ezt az elsőrendű logikai nyelvet röviden p1-vel. A fejezetben a példákban többnyire az p1 nyelvet használjuk. p1-ben

  • π 1 fajtájú termek: c,x,y,

  • π 2 fajtájú termek: x˜,f(c,x˜),f(x,f(c,x˜)),

  • atomi formulák: P(x),Q(yx˜),R(f(c,x˜),f(x,f(c,x˜))),

  • formulák: x¬x˜Q(y,x˜),(x˜Q(y,x˜)x˜R(f(c,x˜),f(c,x˜))),

  • prímformulák: P(x),Q(y,x˜),x˜Q(y,x˜),x¬x˜Q(y,x˜),

  • nem szavak: f(P(x)),(xy),xP(x,x),x˜(Q(c,x˜)Q(x˜,c)),cP(c),

5.1.5. TÉTEL. (A SZERKEZETI INDUKCIÓ ELVE.)

  • Termekre: [Vν] minden termje T tulajdonságú,

(alaplépés:) ha minden változója és konstansa T tulajdonságú és

(indukciós lépés:) ha a t1,t2,,tk termek T tulajdonságúak, akkor az f függvényszimbólum felhasználásával előállított f(t1,t2,,tk) term is T tulajdonságú.

  • Formulákra: [Vν]minden formulája T tulajdonságú,

(alaplépés:) ha minden atomi formula T tulajdonságú és

(indukciós lépések:)

(i1) ha az A formula T tulajdonságú, akkor ¬A is T tulajdonságú,

(i2) ha az A és a B formulák T tulajdonságúak és binér logikai összekötőjel, akkor (AB) is T tulajdonságú és

(i3) ha az A formula T tulajdonságú, Q kvantor és x individuumváltozó, akkor QxA is T tulajdonságú.

A tétel igazolása az ítéletlogikában bebizonyított 4.1.4. tételéhez hasonló, így a bizonyítást az olvasóra bízzuk.

A szerkezeti indukció elve segítségével [Vν] termjeinek, illetve formuláinak számunkra érdekes tulajdonságait fogjuk könnyen igazolni. Ennek az elvnek a felhasználásával bizonyítható a következő fontos állítás is.

5.1.6. TÉTEL. (AZ EGYÉRTELMŰ ELEMZÉS TÉTELE.)

  • [ V ν ] minden termjére a következő állítások közül pontosan egy igaz.

    1. A term változó.

    2. A term konstans.

    3. A term az egyértelműen meghatározható [Vν]-beli t1,t2,,tk termek és az fFn függvényszimbólum felhasználásával előállított f(t1,t2,,tk) alakú term.

  • [ V ν ] minden formulájára a következő állítások közül pontosan egy igaz.

    1. A formula az egyértelműen meghatározható [Vν]-beli t1,t2,,tk termek és a PPr predikátumszimbólum felhasználásával előállított P(t1,t2,,tk) alakú atomi formula.

    2. A formula egy egyértelműen meghatározható [Vν]-beli formula negáltja.

    3. A formula az egyértelműen meghatározható [Vν]-beli A,B formulák és binér logikai összekötőjel felhasználásával előállított (AB) alakú formula.

    4. A formula az egyértelműen meghatározható [Vν]-beli A formula, Q kvantor és x változó felhasználásával előállított QxA alakú formula.

BIZONYÍTÁS. A termekre és a formulákra vonatkozó szerkezeti indukció elve segítségével könnyen be lehet látni, hogy [Vν]

  • minden kifejezése pontosan ugyanannyi nyitó zárójelet, mint záró zárójelet tartalmaz,

  • egyetlen termjének sincs olyan valódi kezdőszelete, mely maga is term lenne,

  • egyetlen formulájának sincs olyan valódi kezdőszelete, mely maga is formula lenne.

Innen a bizonyítás a 4.1.5. tétel bizonyításához hasonló gondolatmenettel folytatható, amit az olvasóra bízunk.

Elsőrendű logikai formulákra általánosítva fogjuk használni a közvetlen részformula és részformula fogalmát, és bevezetjük a közvetlen részterm és részterm fogalmakat is.

5.1.7. DEFINÍCIÓ. [ V ν ] -ben

  1. egyetlen konstansnak és változónak sincs közvetlen résztermje,

  1. az f(t1,t2,,tk) term közvetlen résztermjei a t1,t2,,tk termek,

  1. egy atomi formulának nincs közvetlen részformulája,

  1. a ¬A egyetlen közvetlen részformulája az A formula,

  1. az (AB) formula közvetlen részformulái az A és a B formulák,

  1. a QxA közvetlen részformulája az A formula.

5.1.8. DEFINÍCIÓ.

  • Egy term résztermjeinek halmaza a legszűkebb olyan halmaz, melynek

    1. a term eleme és

    2. ha egy term eleme, akkor eleme a term összes közvetlen résztermje is.

  • Egy formula részformuláinak halmaza a legszűkebb olyan halmaz, amelyiknek

    1. a formula eleme és

    2. ha egy formula eleme, akkor eleme a formula összes közvetlen részformulája is.

5.1.9. PÉLDA. Az 5.1.4. példabeli f(x,f(c,x˜)) term közvetlen résztermjei: x és f(c,x˜), résztermjeinek halmaza:

{ f ( x , f ( c , x ˜ ) ) , x , f ( c , x ˜ ) , c , x ˜ } .

A x¬x˜Q(y,x˜) formula egyetlen közvetlen részformulája: ¬x˜Q(y,x˜), részformuláinak halmaza:

{ x ¬ x ˜ Q ( y , x ˜ ) , ¬ x ˜ Q ( y , x ˜ ) , x ˜ Q ( y , x ˜ ) , Q ( y , x ˜ ) } .

5.1.10. DEFINÍCIÓ. Egy formula azon részformuláit, amelyek prímformulák és amelyekből a formula csupán a ¬,,, logikai összekötőjelek segítségével felépíthető, a formula prímkomponenseinek nevezzük.

Ha egy formulának nincs kvantált részformulája, azaz a formula kvantormentes, akkor prímkomponensei pontosan az atomi részformulái. Ha a formulának van kvantált részformulája, azaz a formula kvantoros, akkor prímkomponensei között legalább egy kvantált formula is lesz. Ha egy kvantált formula prímkomponense a formulának, akkor az ő (prímformula) részformulái nem prímkomponensek, mivel nem tudjuk a kvantált formulát csupán a ¬,,, logikai összekötőjelek segítségével felépíteni belőlük.

5.1.11. PÉLDA. A x¬x˜Q(x,x˜) formula egyetlen prímkomponense önmaga. Ugyanakkor például a (¬x˜(Q(x,x˜)R(x˜,x˜))Q(x,x˜)) prímkomponensei a x˜(Q(x,x˜)R(x˜,x˜)) és a Q(x,x˜) formulák. Felhívjuk a figyelmet arra, hogy Q(x,x˜) is prímkomponens annak ellenére, hogy részformulája a másik prímkomponensnek, hisz a részformulák között az implikáció közvetlen részformulájaként is szerepel.

5.1.12. DEFINÍCIÓ.

  • Egy tterm szerkezeti fája egy olyan véges rendezett fa, melynek csúcsai termek,

    1. gyökere t,

    2. a f(t1,t2,,tk) termet tartalmazó csúcsának pontosan k gyermeke van, ezek rendre a t1,t2,,tk termek,

    3. levelei pedig változók vagy konstansszimbólumok.

  • Egy C formula szerkezeti fája egy olyan véges rendezett fa, melynek csúcsai formulák,

    1. gyökere C,

    2. a ¬A csúcsának egy gyermeke van, az A formula,

    3. az (AB) csúcsának két gyermeke van, rendre az A és a B formulák,

    4. egy QxA csúcsának is egy gyermeke van, az A és

    5. levelei atomi formulák.

5.1.13. PÉLDA. Term és elsőrendű formula szerkezeti fája.

Figure 5.1. Term szerkezeti fája

Term szerkezeti fája

Figure 5.2. Elsőrendű formula szerkezeti fája

Elsőrendű formula szerkezeti fája

A termekhez és elsőrendű formulákhoz is – azok szerkezete szerinti rekurzióval – egyértelműen rendelhetünk különböző dolgokat.

5.1.14. TÉTEL. (A SZERKEZETI REKURZIÓ ELVE.)

  • Termekre: pontosan egy olyan t[Vν]-n értelmezett függvény van, melynek

    (alaplépés:) értékeit rögzítjük t[Vν] változóin és konstansain, majd megmondjuk, hogy értéke

    (indukciós lépések:) az f(t1,t2,,tk) termre az -nek a t1,t2,,tk termeken felvett értékeiből hogyan származtatható.

  • Formulákra: pontosan egy olyan f[Vν]-en értelmezett függvény van, melynek

    (alaplépés:) értékeit rögzítjük f[Vν] atomi formuláin és megmondjuk, hogy értéke

    (indukciós lépések:)

    (r1) a ¬A formulára az A-n felvett értékéből,

    (r2) az (AB) formulára az A-n és a B-n felvett értékeiből, illetve

    (r3) a QxA formulára az A-n felvett értékéből hogyan származtatható.

A szerkezeti rekurzió elvének bizonyítása mind termekre, mind formulákra hasonló, mint ahogy azt az ítéletlogikában láttuk, így az olvasóra bízzuk.

Egy termben szereplő függvényszimbólumok számát a term funkcionális összetettségének, egy formulában szereplő logikai szimbólumok számát pedig a formula logikai összetettségének nevezzük. Felhasználva a szerkezeti rekurzió elvét az összetettséget a következőképpen definiálhatjuk:

5.1.15. DEFINÍCIÓ.

  • Definiáljuk a ˜:t[Vν]N0 függvényt a következőképpen:

    1. ha t változó vagy konstansszimbólum, ˜(t) legyen 0,

    2. ˜ ( f ( t 1 , t 2 , , t k ) ) legyen ˜(t1)+˜(t2)++˜(tk)+1.

Ekkor a tt[Vν] termhez rendelt ˜(t) függvényértéket a t term funkcionális összetettségének nevezzük.

  • Definiáljuk a :f[Vν]N0 függvényt a következőképpen:

    1. ha A atomi formula, (A) legyen 0,

    2. ( ¬ A ) legyen (A)+1,

    3. ( A B ) legyen (A)+(B)+1,

    4. ( Q x A ) pedig legyen (A)+1.

Ekkor az Af[Vν] formulához rendelt (A) függvényértéket az A formula logikai összetettségének nevezzük.

5.1.16. PÉLDA. Például az f(x,f(c,x˜)) term funkcionális összetettsége 2, a

( x ˜ Q ( y , x ˜ ) x ˜ R ( f ( c , x ˜ ) , f ( c , x ˜ ) ) )

formula logikai összetettsége 3.

Az ítéletlogikában definiáltuk a logikai összekötőjel hatáskörének és a fő logikai összekötőjelnek a fogalmát. A fogalmak változtatás nélkül kiterjeszthetők a kvantorokra is. Most egészítsük ki a logikai összekötőjelek közötti erősorrendet azzal, hogy a kvantorokat is besoroljuk. A kvantorok legyenek a negációval azonos prioritásúak, így a prioritás csökkenő sorrendben:

{ , , ¬ } , , , .

A formulákban mindig a nagyobb prioritású logikai jelek értelmezését végezzük el hamarabb, azonos prioritás esetén a feldolgozás jobbról balra sorrendben történik. Így azokat a zárójeleket, melyek ezt a sorrendet jelölnék ki, most is elhagyhatjuk.

Szabad és kötött változók

Egy elsőrendű logikai nyelvben azokat a kifejezéseket, amelyekben nincs individumváltozó, alapkifejezéseknek nevezzük. Így beszélhetünk alaptermekről, alapatomokról és alapformulákról. A nyelv nem alapkifejezéseiben tehát van legalább egy változó. Ugyanaz a változó természetesen egy logikai kifejezésben többször is előfordulhat. Nem alapkifejezésekre jó példák a kvantoros formulák, hisz bennük a prefixumban a kvantor után egy individuumváltozót mindenképpen le kell írni.

Vizsgáljuk most egy elsőrendű logikai nyelv kifejezéseiben a változók különböző előfordulásait. Egy kvantált formulában a kvantor a prefixumban megnevezett változó bizonyos előfordulásaira hatást fejt ki. Ez a hatás a változó-előfordulás státusának megváltozásában nyilvánul meg. Egy kifejezésben egy x változó egy adott előfordulásának kétféle státusát különböztetjük meg. Az x változó adott előfordulása a K kifejezésben kötött, ha egy őt megnevező kvantor hatáskörében van. Az x változó adott előfordulása szabad, ha nem kötött. Egy kvantor a prefixumban megnevezett és a hatáskörében levő, ott még szabad előfordulású változókat köti.

5.1.17. DEFINÍCIÓ.

  1. A termek és az atomi formulák minden változójának minden előfordulása szabad.

  2. A ¬A formulában egy változó-előfordulás pontosan akkor kötött, ha az A-ban van és ott kötött.

  3. Az (AB) formulában egy változó-előfordulás kötött, ha ez az előfordulás A-ban van és ott kötött, vagy B-ben van és ott kötött.

  4. A QxA formulában x minden előfordulása kötött. A Q kvantor teszi kötötté (köti) x valamely előfordulását, ha ez az előfordulás A-ban még szabad. Egy az x-től különböző változó valamely előfordulása kötött, ha A-ban kötött.

Ha egy változónak egy kifejezésben van szabad előfordulása, akkor ezt a változót a kifejezés paraméterének, a kifejezést pedig paraméteres kifejezésnek nevezzük. Egy K kifejezés paramétereinek a halmazára Par (K)-val fogunk hivatkozni. Ha egy kifejezésben nincs paraméter, azaz nincs benne szabad előfordulású változó, akkor vagy egyáltalán nincs benne változó, tehát alapkifejezés, vagy minden változó-előfordulás kötött benne. A paramétermentes kifejezéseket zárt kifejezéseknek nevezzük. A zárt termek nyilván alaptermek és a zárt atomi formulák alapatomok. Az összetett zárt formulák között már vannak – változó-előfordulást tartalmazó – nem alapformulák is, ezek a változó-előfordulások azonban mind kötöttek, tehát ezek a formulák mind kvantoros formulák.

5.1.18. PÉLDA. Vizsgáljuk megint az p1 nyelv kifejezéseit.

  • Alapkifejezések például a c term, a P(c) atomi formula vagy a P(c)¬P(c) formula, hiszen nincs bennük változó-előfordulás.

  • Nem alapformulára példa a x˜(Q(x,x˜)Q(y,x˜)) formula. Benne x˜ előfordulásai az kvantor által kötöttek, az x és az y előfordulásai szabadok. Tehát a formula paraméteres, paraméterei x és y.

  • A x˜(xQ(x,x˜)Q(c,x˜)) formula szintén nem alapformula, viszont az kvantor által kötött x˜ előfordulások mellett az x előfordulásai is kötöttek egy kvantor által, más változó-előfordulás pedig nincs benne. A formula zárt formula vagy mondat.

  • A x(P(x)xQ(x,x˜)) formula szintén paraméteres, az x˜ szabadon fordul elő benne. Az x előfordulásai itt is kötöttek, de a P(x)-beli x előfordulást és a Q(x,x˜)-beli x előfordulást két különböző kvantor köti.

Az Ar nyelvben az N0 univerzum elemei közötti (xy) relációt a

z ( x + z = y ) , u ( x + u = y ) , w ( x + w = y )

formulák bármelyikével kifejezhetjük. Úgy tűnik, a kvantor által kötött változókat – jelentésváltozás nélkül – átnevezhetjük. Azonban ez nem mindig igaz, mert például a

x ( x + x = y )

formula viszont y párosságát fejezi ki. A jelentésváltozás oka az, hogy az előző formulákban az x változó szabad előfordulása ez utóbbi formulában kötötté vált. A kötési viszonyok azért változtak meg, mert a prefixumban x-et neveztük meg, és a kvantor a hatáskörében x összes előfordulását köti.

5.1.19. DEFINÍCIÓ. A QxA formulában a Q kvantor által kötött x változó átnevezéséről beszélünk, amikor

  1. a Qx prefixumban x helyett egy vele megegyező fajtájú y változót nevezünk meg, majd

  2. A -ban az x változó minden szabad előfordulását y-ra cseréljük ki (a kapott formulát jelöljük A(xy)-nal),

és így a Qy(A(xy)) formulát kapjuk. Ha a QxA formulában

  1. y nem paraméter és

  2. x egyetlen előfordulása sem esik y-t megnevező kvantor hatáskörébe,

akkor a Q kvantor által kötött x változó szabályosan végrehajtott átnevezésével nyerjük QxA-ból a Qy(A(xy)) formulát.

5.1.20. PÉLDA. A

x ˜ ( R ( x ˜ , y ˜ ) R ( y ˜ , x ˜ ) )

formulából az kvantor által kötött x˜ szabályosan végrehajtott átnevezésével nyertük a

z ˜ ( R ( z ˜ , y ˜ ) R ( y ˜ , z ˜ ) )

formulát. Az kvantor által kötött változó új nevének y˜-t nem választhatjuk, mert y˜ a kvantor hatáskörében is előforduló paramétere a formulának.

Azt mondjuk, hogy két formula kongruens, ha egymástól csak kötött változók szabályosan végrehajtott átnevezésében különböznek. Azt, hogy A kongruens A-vel, AA-vel jelöljük.

5.1.21. DEFINÍCIÓ.

  1. Egy atomi formula csak önmagával kongruens.

  2. ¬ A ¬ A , ha AA.

  3. ( A B ) ( A B ) , ha AA és BB.

  4. Q x A Q y A , ha A(xz)A(yz) minden olyan z változóra, amely különbözik a QxA-ban és a QyB-ben előforduló összes változótól.

5.1.22. PÉLDA. A

x ( x ˜ Q ( x , x ˜ ) x ˜ ¬ ( Q ( x , x ˜ ) Q ( y , x ˜ ) ) )

formulával kongruens például a

z ( y ˜ Q ( z , y ˜ ) z ˜ ¬ ( Q ( z , z ˜ ) Q ( y , z ˜ ) ) )

formula, ugyanakkor nem kongruens vele a

y ( x ˜ Q ( y , x ˜ ) x ˜ ¬ ( Q ( y , x ˜ ) Q ( x , x ˜ ) ) )

formula, hisz míg az eredeti formulának y a paramétere, ez utóbbinak x.

Világos, hogy minden A,B,C[Vν] formula esetén AA, ha AB, akkor BA és ha AB és BC, akkor AC, azaz az formulák közötti binér reláció ekvivalenciareláció. Ez a reláció az [Vν] elemeinek egy osztályozását generálja, az egymással kongruens formulákat a logikában nem tekintjük lényegében különbözőnek.

5.1.23. DEFINÍCIÓ. Egy formulát változóiban tisztának nevezünk, ha benne minden prefixumban a formula

  1. paramétereitől és

  2. bármely másik prefixumban megnevezett változótól

különböző változó van megnevezve.

5.1.24. TÉTEL. Legyen A formula és Vx változóknak véges halmaza. Ekkor konstruálható olyan változóiban tiszta A formula, hogy

  1. A A és

  2. A -ben minden prefixum Vx-beli változótól különböző változót nevez meg.

BIZONYÍTÁS. Nevezzük a bizonyítás során [Vν] egy A formuláját ismét jónak, ha konstruálható vele kongruens olyan változóiban tiszta A formula, hogy A-ben mindegyik kvantor egy – tetszőlegesen rögzített – Vx változóhalmaz változóitól különböző változót nevez meg. A szerkezeti indukció elve segítségével igazolni fogjuk, hogy minden [Vν]-beli formula jó.

(alaplépés:) Ha A atomi formula, akkor A legyen maga A. Egy atomi formula változóiban tiszta, önmagával kongruens és kvantormentes, tehát [Vν] minden atomi formulája jó.

(indukciós lépések:) Tegyük fel, hogy az A formula jó, azaz konstruálható vele kongruens olyan változóiban tiszta A formula, hogy A-ben az összes kvantor a Vx-beli változóktól különböző változót nevez meg. Ekkor egyrészt ¬A¬A, másrészt ¬A változóiban tiszta és benne minden prefixumban Vx-beli változótól különböző változó van, tehát ¬A-hoz ¬A a megkonstruálni kívánt formula, azaz ¬A is jó. Az (i1) indukciós feltétel teljesül.

Tegyük fel most azt, hogy az A és a B formulák jók, és legyen VB a B-beli változók halmaza. A jósága miatt konstruálható vele kongruens olyan változóiban tiszta A formula, hogy minden A-ben lévő kvantor a VxVB változóhalmaz változóitól különböző változót tartalmaz. Jelölje VAA változóinak halmazát. Legyen B a B-vel kongruens olyan változóiban tiszta formula, melyben minden egyes kvantor a VxVBVA-beli változókból különböző változót nevez meg. Ekkor az AB formulával ( tetszőleges binér logikai összekötőjel) kongruens AB formula változóiban tiszta, és minden prefixumában Vx-beli változóktól különböző változó van, azaz AB is jó. Az (i2) indukciós feltétel is teljesül.

Lássuk utoljára azt be, hogy ha A jó, Q kvantor és x tetszőleges változó, akkor QxA is jó. Legyen y az x-szel azonos fajtájú, QxA-ban és Vx-ben nem szereplő változó. Ha A jó, A(x||y) is jó, tehát van olyan A(x||y)-val kongruens és változóiban tiszta A, melynek minden prefixumában Vx{y}-beli változótól különböző változó fordul elő. Ekkor QxA-val kongruens és változótiszta QyA, továbbá mindegyik kvantora Vx-beli változótól különböző változót nevez meg. Az (i3) indukciós feltétel is teljesül.

Az alaplépésben és az indukciós lépésekben megfogalmazott feltételek teljesülnek, tehát a szerkezeti indukció elve szerint minden [Vν]-beli formula jó.

5.1.25. PÉLDA. A

x ˜ Q ( x , x ˜ ) x x ˜ ¬ ( Q ( x , x ˜ ) R ( y ˜ , x ˜ ) )

formula nem változóiban tiszta, a vele kongruens

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

formula viszont már az.

Termhelyettesítés

5.1.26. DEFINÍCIÓ. Egy olyan θ:Vxt[Vν] függvényt, ahol Vx a nyelv változóinak tetszőleges véges halmaza és θ minden változóhoz a változó fajtájával megegyező fajtájú termet rendel, az [Vν] nyelv termhelyettesítésének nevezünk.

Ha Dom (θ)=, a termhelyettesítést üres termhelyettesítésnek nevezzük és ε-nal jelöljük. Ha Dom (θ)={x1,x2,,xk} és θ(xi)=ti minden i=1,2,,k-ra (k1), θ-t megadhatjuk

  • táblázattal:

θ = ( x 1 x 2 x k t 1 t 2 t k )

  • vagy felsorolással:

θ = ( x 1 , x 2 , , x k t 1 , t 2 , , t k )

Egy θ termhelyettesítést alaphelyettesítésnek fogunk nevezni, ha Rng (θ) minden termje alapterm. θx pedig azt a termhelyettesítést jelöli, melyre Dom (θx)=Dom (θ){x} és minden zDom (θx) esetén θx(z)=θ(z).

Az [Vν] nyelvnek legyen K valamely kifejezése, θ pedig egy termhelyettesítése. Minden egyes xDom (θ) változó minden egyes K-beli szabad előfordulását helyettesítsük egyidejűleg a θ(x) termmel. Ilyenkor azt mondjuk, hogy a θ termhelyettesítést a K kifejezésben végrehajtottuk, és az eredményképpen kapott kifejezést (Kθ)-val jelöljük. Most megadjuk a fogalom pontos induktív definícióját.

5.1.27. DEFINÍCIÓ. Az [Vν] nyelvnek legyen θ tetszőleges termhelyettesítése.

  1. Ha cCnst, akkor (cθ)c.

  2. Ha x változó, akkor (xθ){x,haxDom (θ)θ(x),haxDom (θ)

  3. ( f ( t 1 , t 2 , , t k ) θ ) f ( ( t 1 θ ) , ( t 2 θ ) , , ( t k θ ) )

  4. ( P ( t 1 , t 2 , , t k ) θ ) P ( ( t 1 θ ) , ( t 2 θ ) , , ( t k θ ) )

  5. ( ¬ A θ ) ¬ ( A θ ) .

  6. ( ( A B ) θ ) ( ( A θ ) ( B θ ) ) , ahol binér logikai összekötőjel.

  7. ( Q x A θ ) Q x ( A θ x ) , ahol Q kvantor.

5.1.28. megjegyzés. Nem minden termhelyettesítést fogunk alkalmazni a logikában. Tekintsük ugyanis most újból az Ar nyelvben az N0 univerzum elemei közötti (xy) relációt kifejező

z ( x + z = y )

formulát. Tegyük fel, hogy szeretnénk kifejezni az (xyz) összefüggést, ami első ránézésre úgy tűnik, hogy az y változónak az yz termmel való helyettesítésével nyerhető. Azonban az így nyert

z ( x + z = y z )

formula nem a kívánt relációt jelenti, és csupán az x és az y változók a paraméterei, z nem. A problémát az okozza, hogy az yz termben előforduló z szabad változó bekerült a z-t megnevező egzisztenciális kvantor hatáskörébe, így kötött változó lett belőle. Ezt a jelenséget változóütközésnek nevezzük, és úgy fogjuk elkerülni, hogy a formulánkban előbb – megfelelő módon – szabályosan átnevezzük a kvantor által kötött változót (például u-ra), és csak utána írjuk be az yz termet az y változó helyére. Eredményül a kívánt jelentésű

u ( x + u = y z )

formulát kapjuk.

Jelöljük ki tehát egy kifejezés számára azokat a termhelyettesítéseket, amelyek végrehajtása nem okoz változóütközést. A θ termhelyettesítés megengedett a K kifejezés számára, ha minden xDom (θ) esetén x minden K-beli szabad előfordulása kívül esik a θ(x) term valamennyi változóját megnevező kvantor hatáskörén.

5.1.29. DEFINÍCIÓ.

  1. Termek és atomi formulák számára minden termhelyettesítés megengedett.

  2. ¬ A számára egy termhelyettesítés megengedett, ha megengedett A számára.

  3. ( A B ) számára egy termhelyettesítés megengedett, ha megengedett A és B számára is.

  4. Q x A számára egy θ termhelyettesítés megengedett, ha

    1. egyetlen zPar (QxA)Dom (θ) változó esetén sem fordul elő x a θ(z) termben,

    2. θ x pedig megengedett A számára.

5.1.30. PÉLDA. Az p1-beli x˜R(x˜,f(x,x˜))xQ(x,f(x,x˜)) formula számára az

( x y x ˜ y x f ( y , y ˜ ) )

termhelyettesítés megengedett, az

( x y x ˜ y x f ( x , y ˜ ) )

termhelyettesítés pedig nem megengedett, mert a helyettesítendő szabad előfordulású x˜ az x-et kötő hatáskörében van, és a helyére beírandó f(x,y˜) termben is előfordul az x változó.

Legyen K egy kifejezés és θ egy termhelyettesítés. Konstruáljunk meg egy K-val kongruens olyan K formulát, amely számára θ megengedett. Ekkor a (Kθ) kifejezés a θ termhelyettesítés K-ban való szabályos végrehajtásának eredménye. Jelölése: [Kθ].

5.1.31. DEFINÍCIÓ.

  1. Ha K term vagy atomi formula, akkor [Kθ](Kθ).

  2. [ ¬ A θ ] ¬ [ A θ ]

  3. [ ( A B ) θ ] ( [ A θ ] [ B θ ] )

    1. Ha egyetlen zPar (QxA)Dom (θ) változó esetén sem fordul elő a θ(z) termben x, akkor [QxAθ]Qx[Aθx].

    2. Ha van olyan zPar (QxA)Dom (θ) változó, hogy x paraméter θ(z)-ben, akkor válasszunk egy új változót – például u-t –, mely nem fordul elő sem QxA-ban, sem Rng (θ) termjeiben, és

[ Q x A θ ] Q u [ A ( x u ) θ x ] .

5.1.32. PÉLDA. Az p1-beli x˜R(x˜,f(x,x˜))xQ(x,f(x,x˜)) formulában az

( x y x ˜ y x f ( x , y ˜ ) )

termhelyettesítés szabályos végrehajtásának eredménye a

x ˜ R ( x ˜ , f ( y , x ˜ ) ) z Q ( z , f ( z , f ( x , y ˜ ) ) )

formula.

Egy [Vν] logikai nyelv termhelyettesítései halmazán vezessük be a következő műveletet:

5.1.33. DEFINÍCIÓ. Legyenek

θ = ( x 1 x 2 x k t 1 t 2 t k ) és η = ( y 1 y 2 y s 1 s 2 s )

az [Vν] nyelv termhelyettesítései. θ és ηkompozícióján a

( θ η ) = ( x 1 x 2 x k y i 1 y i 2 y i j ( t 1 η ) ( t 2 η ) ( t k η ) s i 1 s i 2 s i j )

termhelyettesítést értjük, ahol {yi1,yi2,,yij}=Dom (η)Dom (θ) és Dom (θη)=Dom (θ)(Dom (η)Dom (θ)).

5.1.34. PÉLDA. Legyenek

θ = ( x y x ˜ y x f ( x , y ˜ ) ) és η = ( x y x ˜ y ˜ z ˜ c z y ˜ x ˜ f ( x , x ˜ ) )

p 1 termhelyettesítései. Ekkor

( θ η ) = ( x y x ˜ y ˜ z ˜ z c f ( c , x ˜ ) x ˜ f ( x , x ˜ ) )

és

( η θ ) = ( x y x ˜ y ˜ z ˜ c z y ˜ f ( x , y ˜ ) f ( y , f ( x , y ˜ ) ) ) .

A fenti példa mutatja, hogy a kompozíció művelete egy nyelv termhelyettesítéseinek halmazán nem kommutatív. Be lehet ugyanakkor látni, hogy a kompozíció műveletével ez a halmaz neutrális elemmel rendelkező félcsoport.

5.1.35. LEMMA. Legyenek θ és η az [Vν] nyelv termhelyettesítései. Ekkor tetszőleges t[Vν] term esetén

( t ( θ η ) ) = ( ( t θ ) η ) .

BIZONYÍTÁS. Nevezzük a bizonyítás során egy t termet jónak, ha (t(θη))=((tθ)η). A szerkezeti indukció elve segítségével igazolni fogjuk, hogy minden [Vν]-beli term jó.

(alaplépés:) Ha a term konstans, nyilván a termhelyettesítések eredménye maga a konstans, tehát a konstanstermek jók. Ha változó, például x, három eset lehetséges:

  • x Dom  ( θ ) Dom  ( η ) : Ekkor a termhelyettesítések eredménye maga a változó, tehát az ilyen változóterm jó.

  • x Dom  ( η ) Dom  ( θ ) : Egyrészt (xθ)=x, ezért ((xθ)η)=(xη)=η(x), másrészt (x(θη))=η(x), mivel Dom (θη)-ba az x közvetlenül az η termhelyettesítésből került be. Tehát ezek a változótermek is jók.

  • x Dom  ( θ ) : Ebben az esetben (xθ)=θ(x), tehát ((xθ)η)=(θ(x)η), és a kompozíció definíciója alapján szintén (x(θη))=(θ(x)η), azaz ezek a termek is jók.

(indukciós lépés:) Tegyük most fel, hogy az f(t1,t2,,tk) termbeli t1,t2,,tk termek jók. Ekkor a termhelyettesítés induktív definíciója alapján

( ( f ( t 1 , t 2 , , t k ) θ ) η ) = = ( f ( ( t 1 θ ) , ( t 2 θ ) , , ( t k θ ) ) η ) = f ( ( ( t 1 θ ) η ) , ( ( t 2 θ ) η ) , , ( ( t k θ ) η ) ) .

Mivel a t1,t2,,tk termek jók, ezért ((tiθ)η)=(ti(θη)) minden i=1,2,,k-ra, tehát

f ( ( ( t 1 θ ) η ) , ( ( t 2 θ ) η ) , , ( ( t k θ ) η ) ) = f ( ( t 1 ( θ η ) ) , ( t 2 ( θ η ) ) , , ( t k ( θ η ) ) ) .

Most újból a termhelyettesítés induktív definícióját alkalmazva (visszafele) kapjuk, hogy

f ( ( t 1 ( θ η ) ) , ( t 2 ( θ η ) ) , , ( t k ( θ η ) ) ) = ( f ( t 1 , t 2 , , t k ) ( θ η ) ) .

Tehát az f(t1,t2,,tk) term is jó.

Az alaplépésben és az indukciós lépésekben megfogalmazott feltételek teljesülnek, tehát a szerkezeti indukció elve szerint minden [Vν]-beli term jó.

5.1.36. TÉTEL. Az [Vν] nyelv tetszőleges θ, η és ζ termhelyettesítései esetén

(1)

( ( θ η ) ζ ) = ( θ ( η ζ ) )

( a   k o m p o z í c i ó   a s s z o c i a t í v )

(2)

θ ε = ε θ = θ

( ε   n e u t r á l i s   e l e m )

BIZONYÍTÁS. (1) bizonyításához legyenek

θ = ( x 1 x 2 x k t 1 t 2 t k ) , η = ( y 1 y 2 y l s 1 s 2 s l ) , ζ = ( z 1 z 2 z m q 1 q 2 q m )

az [Vν] nyelv tetszőleges termhelyettesítései. Ekkor mivel

( θ η ) = ( x 1 x 2 x k y i 1 y i 2 y i j ( t 1 η ) ( t 2 η ) ( t k η ) s i 1 s i 2 s i j ) ,

ahol {yi1,yi2,,yij}=Dom (η)Dom (θ), ezért ((θη)ζ) az alábbi termhelyettesítés:

( x 1 x k y i 1 y i j z i 1 z i j ( ( t 1 η ) ζ ) ( ( t k η ) ζ ) ( s i 1 ζ ) ( s i j ζ ) q i 1 q i j ) ,

ahol {zi1,,zij}=Dom (ζ)Dom (θη). Továbbá

( η ζ ) = ( y 1 y 2 y l z n 1 z n 2 z n o ( s 1 ζ ) ( s 2 ζ ) ( s l ζ ) q n 1 q n 2 q n o ) ,

ahol {zn1,zn2,,zno}=Dom (ζ)Dom (η). De a zn1,zn2,,zno változók közül csak a zi1,,zij változók, továbbá az y1,y2,,yl változók közül pedig csak az yi1,,yij változók nincsenek Dom (θ)-ban ezért (θ(ηζ)) az alábbi termhelyettesítés:

( x 1 x k y i 1 y i j z i 1 z i j ( t 1 ( η ζ ) ) ( t k ( η ζ ) ) ( s i 1 ζ ) ( s i j ζ ) q i 1 q i j ) .

Az 5.1.35. lemmát felhasználva innen közvetlenül adódik (1). (2) bizonyítását pedig az olvasóra hagyjuk.

Az ítéletlogikában már találkoztunk a formulahelyettesítés fogalmával. Az elsőrendű logikában is élünk hasonló lehetőséggel. Most megadjuk az elsőrendű formulákban a formulahelyettesítés pontos definícióját.

Legyen F az [Vν] nyelv egy formulája és x1,x2,,xk(k0) rendre π1,π2,,πk fajtájú különböző változók. Az x1x2xkF kifejezést (π1,π2,,πk) alakú formális predikátumnak, az x1,x2,,xk változókat pedig a formális predikátum kijelölt változóinak nevezzük. Ha k=0, a formális predikátum alakja (), és nincsenek kijelölt változói.

5.1.37. DEFINÍCIÓ. Legyen A egy elsőrendű formula, F egy (π1,π2,,πk) alakú x1x2xkF formális predikátum, P pedig egy (π1,π2,,πk) alakú predikátumszimbólum. Az A formulában a P predikátumszimbólum F formális predikátummal való szabályos helyettesítésének az eredményét jelölje A(PF).

  1. Ha A atomi formula, legyen Q(t1,t2,,tn).

    1. Ha Q különbözik P-től, akkor A(PF) változatlanul A.

    2. Ha Q és P megegyezik (természetesen ebben az esetben k=n), akkor A(PF)F(x1,x2,,xkt1,t2,,tk).

  2. Legyen A a ¬B negáció, ekkor A(PF)¬(B(PF)).

  3. Legyen A a (BC) formula, ahol binér logikai összekötőjel. Ekkor A(PF)B(PF)C(PF).

  4. Legyen A a QxB kvantált formula. Két esetet különböztetünk meg:

    1. ha xPar (F){x1,x2,,xk}, akkor A(PF)Qx(B(PF)).

    2. ha xPar (F){x1,x2,,xk}, akkor válasszunk egy új változót – például u-t –, mely nem fordul elő sem A-ban, sem F-ben, és legyen A(PF)Qu(B(xu)(PF)).

5.1.38. PÉLDA. Legyen Vν a {π},{P,Q,R},{f,g,h}, halmaznégyes a következő szignatúrával:

v 1

v 2

P

( π )

f

( π , π )

Q

( π , π )

g

( π , π , π )

R

( π , π , π )

h

( π , π , π , π )

Legyenek x,y,z,π fajtájú változók. Jelöljük ezt az elsőrendű logikai nyelvet p2-vel.

Az p2 nyelvben az R(x,y,x)zP(z) formulában a P predikátumszimbólum z¬xQ(x,z) formális predikátummal való szabályos helyettesítésének az eredménye, azaz (R(x,y,x)zP(z))(Pz¬xQ(x,z)), az

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

formula. Ha pedig a zyQ(g(x,z),y) formulában a Q predikátumszimbólumot helyettesítjük az xyR(x,y,z) formális predikátummal, akkor a

u y R ( g ( x , u ) , y , z )

formulát kapjuk.

Feladatok

5.1.1. FELADAT. Termek-e az p2 nyelvben a következő szavak:

  1. f ( g ( x , y ) )

  2. g ( f ( z ) , h ( x , x , x ) )

  3. f ( g ( x ) , h ( x , y , z ) )

  4. f ( x ) g ( x , y )

5.1.2. FELADAT. Adjuk meg azoknak az p2-beli termeknek a halmazát, melyek egyetlen változót, az x-et és egyetlen függvényszimbólumot,

  1. az f-et

  2. a g-t

tartalmazzák.

5.1.3. FELADAT. Soroljuk fel a következő p2-beli termek közvetlen résztermjeit, résztermjeit, adjuk meg szerkezeti fájukat, és határozzuk meg a funkcionális összetettségüket.

  1. h ( x , f ( y ) , z )

  2. g ( g ( x , f ( y ) ) , f ( z ) )

  3. g ( h ( x , y , z ) , f ( g ( x , x ) ) )

  4. f ( h ( g ( x , f ( y ) ) , y , f ( y ) ) )

5.1.4. FELADAT. Atomi formulák-e az p2 nyelvben a következő szavak:

  1. Q ( f ( y ) , h ( y , z , z ) )

  2. R ( x , g ( x , y ) )

  3. R ( P ( x ) , f ( y ) , x )

  4. f ( h ( x , y , z ) )

5.1.5. FELADAT. Formulák-e az p2 nyelvben a következő szavak:

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

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

  3. ¬ x x P ( y )

  4. z ( R ( x , y , h ( x , y , z ) ) P ( z ) )

5.1.6. FELADAT. Soroljuk fel az alábbi p2-beli formulák közvetlen részformuláit, részformuláit, adjuk meg szerkezeti fájukat és logikai összetettségüket.

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

  2. x R ( x , y , z ) ¬ ( P ( g ( x , y ) ) z P ( z ) )

  3. x ¬ ( P ( f ( x ) ) Q ( x , y ) ) z R ( z , z )

  4. x P ( x ) x y ( P ( x ) P ( y ) R ( x , y , x ) )

5.1.7. FELADAT. Melyek részformulái az alábbiak közül a p2-beli

z ( x Q ( x , z ) ( z x Q ( x , z ) z Q ( x , z ) ) )

formulának?

  1. x Q ( x , z )

  2. x Q ( x , z ) z x Q ( x , z )

  3. z x Q ( x , z ) z Q ( x , z )

  4. x Q ( x , z ) z Q ( x , z )

5.1.8. FELADAT. Adjuk meg az alábbi p2-beli formulák prímkomponenseit.

  1. x Q ( x , z ) z Q ( x , z )

  2. x Q ( x , z ) z x Q ( x , z )

  3. z ( x Q ( x , z ) ( z x Q ( x , z ) z Q ( x , z ) ) )

  4. x Q ( x , z ) ( z x Q ( x , z ) z Q ( x , z ) )

5.1.9. FELADAT. Az p2 nyelv következő formuláiban állapítsuk meg a kvantorok hatáskörét, majd döntsük el a változókról, hogy melyik előfordulásuk szabad és melyik kötött.

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

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

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

  4. y z ( R ( x , y , z ) x Q ( z , x ) )

5.1.10. FELADAT. Döntsük el p2 következő formuláiról, hogy kongruensek-e.

  1. z ( x R ( z , x , v ) v ( Q ( v , u ) w R ( v , w , x ) ) )

  2. x ( w R ( x , w , v ) w ( Q ( w , u ) v R ( w , v , x ) ) )

  3. x ( w R ( x , w , u ) v ( Q ( v , u ) w R ( v , w , x ) ) )

  4. z ( x R ( x , z , v ) w ( Q ( w , u ) v R ( w , v , x ) ) )

  5. v ( w R ( v , w , x ) x ( Q ( x , u ) w R ( v , w , x ) ) )

5.1.11. FELADAT. Változóikban tiszták-e az alábbi p2-beli formulák? Amelyik nem, ahhoz adjunk meg vele kongruens, változóiban tiszta formulát.

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

  2. x ¬ R ( x , v , w ) z y ( Q ( y , z ) R ( u , y , z ) )

  3. x z ( P ( x ) Q ( x , f ( z ) ) ) y Q ( x , y )

  4. x R ( x , y , z ) x y ( P ( y ) R ( x , y , z ) )

5.1.12. FELADAT. Megengedettek-e az p2 nyelvbeli alábbi termhelyettesítések? Végezzük el a termhelyettesítéseket szabályosan.

  1. ( y R ( x , y , z ) ) ( x g ( x , y ) )

  2. ( y R ( x , y , z ) ) ( y g ( x , y ) )

  3. ( y Q ( x , y ) P ( x ) ) ( x g ( x , z ) )

  4. ( y Q ( y , z ) y Q ( x , y ) ) ( x z y g ( x , y ) y z )

5.1.13. FELADAT. Bizonyítsuk be, hogy a θ termhelyettesítés megengedett a K kifejezés számára, ha

  1. θ = ( x 1 x 2 x k x 1 x 2 x k ) ;

  2. Dom  ( θ ) Par  ( K ) = ;

  3. K -ban nincsenek az Rng (θ)-beli termekben előforduló változók;

  4. θ alaphelyettesítés.

5.1.14. FELADAT. Határozzuk meg az alábbi termhelyettesítések kompozícióját.

  1. ( x y z v z x f ( z ) f ( x ) ) é s ( x y z z x y )

  2. ( x y z z x y ) é s ( x y z v z x f ( z ) f ( x ) )