Az informatika logikai alapjai PTI BSc nappali szakosok számára g 2. verzió, október 9

Az informatika logikai alapjai PTI BSc nappali szakosok számára g 2. verzió, 2009. október 9. Vályi Sándor

NyF TTIK Matematikai és Informatikai Intézet

2009 ®szi szemeszter

Az 1. verzióbeli részek apróbb javításokon estek keresztül, kérem, gyeljék! (A hibákat javítottam.) 1

Miért tanulunk logikát? A számítástudomány

(computer science)

alapvet® része.

Alkalmazásai:

• ismeretek formális, deklaratív leírása  természetes nyelvi állítások formalizálása  mesterséges ágensek környezetleírása  áramkörök leírása (specikációja)  szemantikus web (az internetes tartalmak metaadatainak formalizálása)

2

• ismereteken végzett következtetések formalizálása, automatizálása

 automatizált következtetés (gépi bizonyítás)  szabály alapú rendszerek  robotika  szoftverrobotok ismeretszerzése következtet® eljárásokkal

• számítástudomány alapeszköze  algoritmuselmélet (milyen függvények kiszámíthatók?)  bonyolultságelmélet (mennyi er®forrás szükségeltetik az adott feladat megoldásához?)

 programok jelentésének leírása (szemantika )  programok helyességének bizonyítása (verkáció)

• programozás logikai nyelveken  Horn-logika, Prolog, Erlang  szabály alapú rendszerek (szakért®i rendszerek, CLIPS)

Az ismeretek, amire építünk  legalábbis párhuzamosan használjuk

3

A Diszkrét matematika c. tárgy keretében tanulják:

Nem csak a fogalmak deníció, hanem alapvet® tulajdonságaik, összefüggéseik is Halmaz, halmaz eleme, halmazok megadása elemfelsorolással és hozzátartozási feltétel megadásával, halmaz része, egyenl® halmazok, üres halmaz, diszjunkt halmaz, m¶veletek halmazokkal: unió, metszet, különbség, komplementer. Venn-diagrammok. Rendezett pár, rendezetlen pár, Descartes- (direkt) szorzat, rendezett

n-es, relációk, üres reláció, reláció aritása, binér reláció,

binér relációk tulajdonságai: reexív,irreexív, szimmetrikus, antiszimmetrikus, aszimmetrikus, tranzitív, dichotom, trichotom, ekvivalenciareláció, ekvivalenciaosztályok, gyenge/er®s rendezési

4

reláció, teljes rendezési reláció, rendezett halmaz részhalmazának innuma és szuprémuma.

n-változós függvény, értelmezési tartomány, értékkészlet, elem függvény általi képe, elem függvény általi ®sképe, szürjektív, injektív és bijektív függvények. Injektív függvény inverze, m¶veletek (operátorok). A természetes, az egész, a racionális és a valós számok halmazai és m¶veletei, tulajdonságaik. Véges és végtelen sorozatok, összef¶zési m¶veleteik. Két halmaz mikor egyenl® számosságú, mikor kisebb az egyik halamz számossága a másikénál, véges és végtelen halmazok. Fa, fa csúcsa, fa gyökere, levelei, csúcsok mélysége, él, csúcs ®se, csúcs utódai, ág a fában, bináris fa.

Az ismeretek, amire építünk  legalábbis párhuzamosan használjuk II. A Formális nyelvek és automaták c. tárgy keretében tanulják: Véges ábécé, bet¶, szó (véges jelsorozat), m¶veletek szavakkal: összef¶zés. Szó kezd®szelete(prexe), végszelete, részszava.

5

Az ismeretreprezentáció típusai Ismeretreprezentáció = ismeretábrázolás típusai:

• deklaratív  állításokkal írjuk le, milyen tények állnak fenn • strukturális(szerkezeti)  matematikai (vagy más, pl. informatikai, grakus) strukturákat írunk le

• vizuális • procedurális (eljárásokkal írjuk le ismereteinket)

6

• objektumorientált  a deklaratív és a procedurális keveréke, sok esetben az emberi gondolkodásunkhoz közel álló, természetes ismeretleírási mód

Az ismeretreprezentáció típusai Az ember bels® ismeretreprezentációja még intenzíven kutatott terület

(cognitive science)

Mindenesetre az ismeretek közlésének alapvet® eszköze: a deklaratív típusú ismeretek (állítások) átadása

7

Példa logikai ismeretreprezentációra

A wumpus-világbéli ágensünk feladata: a fenti pályán megtalálni az aranyat. A körülményeket el®ször természetes nyelven írjuk le:

8

A wumpus-világ körülményei

Az ágensünknek a fent megadott 4x4-es pályán kell megtalálnia az aranyat, bizonyos feltételek mellett:

9

csapdák (pit), szörny (wumpus) vannak a pályán, a csapdák 4szomszédjaiban szell® érz®dik, a szörnnyel szomszédos szobákban b¶z érzékelhet®, az arany ragyogásként érzékelhet®, egyetlen nyilunk van, azt egy irányban tudjuk kil®ni, s csak a szomszédos szobában van hatása: megöli a szörnyet ( a b¶z mindenhol elt¶nik), ha elhunyt a szörny, akkor halálsikolyt hallat: ezt mindenhol hallani, ha a szörnyhöz lépünk, meghalunk.

Cél : az arany megtalálása Er®források: lépésszám korlátozott, egy nyilunk van, egy életünk van

Érzékel®k: b¶z, szell®, ragyogás, sikoly, falnak-ütközés Akciók: balra fordul, jobbra fordul, lép, megfog

A wumpus-világ logikai leírása (nulladrend¶ logikával) Csi,j jelentse azt, hogy csapda van az [i, j] pozíción. Szi,j jelentse azt, hogy szell® van a [i, j] szobában ¬Cs1,1 ∨ Sz1,2 ∨ Sz2,1 A csapdák szelll®t okoznak a szomszédos szobákban

Sz1,1↔(Cs1,2 ∨ Cs2,1) Sz2,1↔(Cs1,1 ∨ Cs2,2 ∨ Cs3,1) A szoba

akkor és csak akkor

szell®s, ha valamelyik szomszédban

csapda van

10

A wumpus-világ logikai leírása nulladrend¶ logikával nagyon körülményes . . . Minden

i, j -re ezeket külön meg kell ismételni, pl.: Sz4,3↔(Cs4,2 ∨ Cs4,4 ∨ Cs3,3) Sz3,3↔(Cs3,2 ∨ Cs3,4 ∨ Cs2,3 ∨ Cs4,3) ...

11

A wumpus-világ logikai leírása els®rend¶ logikával nagyon természetes: . . . ∀i, j (Szi,j ↔(Csi,j−1 ∨ Csi,j+1 ∨ Csi−1,j ∨ Csi+1,j ))

(az egyszer¶ség kedvéért eltekintünk a határvonalon lév® szobáktól)

12

A wumpus-példa egyedüli célja: A logikai ismeretreprezentáció szemléltetése.

További használat: gyakorlaton.

13

Egyszer¶ / összetett ismeret-reprezentáció • Egyszer¶: csak egy típust engedünk meg, minden egyed ugyanannak az osztálynak eleme

 Els®rend¶ logika, Prolog, szabályrendszerek, leíró logikák  Formális nyelvtanok

14

• Összetett: többféle típusú objektumaink vannak  Típusos els®rend¶ logika, másodrend¶ logika, típuselméleti logika

 Objektum-orientált programok modelljei  És ennek el®dei: típushierarchia (taxonomikus háló), szemantikus hálók, keretek (frame-ek)

Ebben a félévben csak a típusus els®rend¶ logikáig jutunk.

A logika tudományának f® feladata és tanult részei A

helyes következtetés fogalmának

leírása

A helyes következtetés törvényeinek

megállapítása

Szintaxis: a formulák, mint jelsorozatok vizsgálata Szemantika: hogyan f¶zünk jelentést a formulákhoz Bizonyításelmélet: hogyan érvelhetünk helyesen és teljes rendszerben, esetleg automatizáltan

Nem f® feladat a logikai fejtör®k vizsgálata, bár ahhoz is ad hasznos eszközöket, fogalmakat.

15

A következtetés megfogalmazásai Meglév® ismeret

⇒ új ismeret

Feltételek (premisszák) Hipotézisek

⇒ következmény

⇒ konklúzió

Logikai következtetés: HA a premisszák igazak, AKKOR a konklúzió is igaz.

16

Logikai következmény Olyan következmény, ami csupán a logikai szavak jelentése miatt áll fenn.

Ha A vagy B , akkor C . Nem igaz C . -

A nem igaz. Logikai szavak itt: nem . . . , . . . vagy . . . , ha . . . akkor . . .

17

Másik példa logikai következményre Minden magyar szereti az anyját. Bárki anyja n®. Van szép magyar n®.  Van szép n®, aki szeret egy n®t. Az ebben szerepl® állítások logikai szerkezete már nehezebben felismerhet®, ezzel foglalkozik majd az els®rend¶ logika.

(Minden . . . , van olyan . . . ) Ha kicseréljük a

magyar, szép, anyja, n®

szavakat hasonló nyelv-

tani szerep¶ szavakra, a következtetés helyes marad!

18

Másik példa logikai következményre Minden ember halandó. Szókratész ember. Szókratész halandó. Ha kicseréljük az

ember, halandó, Szókratész

szavakat hasonló

nyelvtani szerep¶ szavakra, a következtetés helyes marad!

minden

szó logikai.

Minden kutya ugat. Vahur kutya.  Vahur ugat.

19

A

Ezzel szemben, bár mind a premisszák, mind a konklúzió igaz a szokásos jelentésében, mégsem helyes logikai következtetés az alábbi. Minden bogár rovar. A futrinka rovar.  A futrinka bogár. Ugyanis, ha a benne szerepl® szavaknak más a jelentésük, de a logikai szerkezet változatlan marad, lehet, hogy a premisszák igazak maradnak, de konklúzió hamis lesz, pl. Minden hüll® gerinces. A béka gerinces.  A béka hüll®. Ezek szerint, a Minden A egyben B is. g B tulajdonságú.  g A tulajdonságú. logikai szerkezet nem helyes következtetési forma.

20

A köznapi következtetéseink tartalmazzák a logikaiakat, de vannak másféle következtetéseink is. Bálint vére Csillának. Csilla anyja Dávidnak.  Bálint anyai nagybátyja Dávidnak. A n®k szeretik a szép ruhákat.  Eszter szereti a szép ruhákat. Gabi maláriában szenvedett. Gabi kinint kap gyógyszerül.  Gabi meggyógyul. Ezek a következtetések a mindennapi életben megállják a helyüket, de csak azért, mert valamilyen implicit háttérismeret van a birtokunkban, ami nincs odaírva, de amelyekkel kiegészítve a következmény már logikai. A második példában: Eszter n®, a harmadikban: A kinin 100%-osan gyógyítja a maláriát. Az els® példa feltételeinek kiegészítését az olvasóra bízzuk.

21

Állítás (propozíció)

Olyan kijelent® mondat, ami egyértelm¶ jelentéssel bír és igazságértékkel rendelkezik.

22

Állítás

Nem állítás

A Tisza hazánk legnagyobb folyója.

A Duna dél felé folyik.

3+2>5 minden x ∈ N-re: x + 2 > x

x+2>y x := x + 1

Volt olyan francia király, aki kopasz volt.

A francia király kopasz.

Az

x+2 > y az úgynevezett

paraméteres állítások

kategóriájához

tartozik.

23

1. feladat  Kijelentéslogikai kiolvasás Állítások-e az alábbi természetes nyelvi mondatok?

a. Kett® meg kett® az négy. b. Kett® meg kett® az öt. c. Kett® meg kett® az négy? d. Ha kett® meg kett® az öt, akkor süt a nap. e. Süt a nap. f. Egészségtelenül táplálkozik, aki keveset mozog. g. Mindenki, aki keveset mozog és egészségtelenül táplálkozik, végül kövér lesz. h. Egészségesen táplálkozok. i. Néha nem táplálkozok egészségesen. j. Nem tudom, hogy egészségtelenül táplálkozok-e. k. Most nem mondok igazat. l. Nem tudom, hogy mit tudok.

24

Logikai összeköt® szavak A logikai következmények a logikai szavak tulajdonságain múlnak: mik ezek? Amit már ismerünk középiskolából: Név

Jel

Kiolvasás

konjunkció diszjunkció negáció implikáció ekvivalencia

∧ ∨ ¬ → ↔

. . . és . . . . . . vagy . . . nem igaz, hogy . . . ha . . . , akkor . . . . . . akkor és csak akkor, ha . . .

Ezekkel állításokból újabb, bonyolultabb állításokat lehet összeállítani.

25

2. feladat  Propozicionálisan összetett állítások kiolvasása Olvassa ki a következ® állításokat, ha lan szám és

P azt rövidíti, hogy x párat-

Q azt rövidíti, hogy x egyjegy¶ szám (nemnegatív

egész).

¬P ¬(P ∧ Q) (P →Q) ¬(P ∨ Q)

(P ∧ Q) (P ∨ Q) ((P ∨ Q)→(P ∧ Q)) ((P →Q)→P )

26

3. feladat - Propozicionális formalizálás Írja fel logikai összeköt® jelekkel a következ® természetes nyelvi összetett állításokat: Nem P , de Q. P lehetetlen. Nem P , se nem Q. Nem igaz, hogy akár P , akár Q igaz. Sem P , sem P ellentéte. Kizárt, hogy P és Q mind igaz. P , feltéve, hogy Q P csak akkor, ha Q. Ha P , akkor Q, de csakis akkor. Nem igaz, hogy P és Q. P -nek szükséges feltétele Q. P szükséges feltétele Q-nak Vagy P és Q, vagy nem P és nem Q.

27

4. feladat  természetes nyelvi állítás tagadása 1.6. Melyik tagadása a következ® állításnak? Ha az a egész szám 5-tel osztható,akkor 0-ra végz®dik. a) Ha az a szám nem osztható 5-tel, akkor nem is végz®dik 0-ra. b) Nem igaz, hogy az a szám nem osztható 5-tel, vagy 0-ra végz®dik. c) Az a szám nem osztható 5-tel és nem is végz®dik 0-ra. d) Az a szám osztható 5-tel, és mégsem végz®dik 0-ra. e) Ha az a szám osztható 5-tel, akkor nem végz®dik 0-ra. Formalizálja az állításokat! Logikai értéktáblázattal ellen®rizze döntését!

28

5. feladat  természetes nyelvi állítás tagadása Keresse meg a Nem igaz, hogy Gerg® tud összeadni és osztani. állítással egyez® jelentés¶ állításokat! a) Gerg® nem tud összeadni és osztani. b) Gerg® tud összeadni, de osztani nem. c) Gerg® nem tud összeadni vagy nem tud osztani. d) Gerg® tud összeadni vagy osztani.

29

6. feladat  természetes nyelvi állítás tagadása Mely állítások értelme egyezik meg a Nem igaz, hogy az ABC háromszög derékszög¶ vagy tompaszög¶. állítással? a) Az ABC háromszög nem derékszög¶ vagy nem tompaszög¶. b) Az ABC háromszög nem derékszög¶, és nem is tompaszög¶. c) Nem igaz, hogy az ABC háromszög derékszög¶ és tompaszög¶. d) Ha az ABC háromszög nem derékszög¶, akkor nem is tompaszög¶.

30

7. feladat  Propozicionális kiolvasás Jelölje

I ,B ,J rendre a következ® természetes nyelvi állításokat:

I - Id®t fordítok a tanulásra. B - Fel bírom fogni a tananyagot. J - Jelest kapok logikából. Olvassa ki az alábbi formulákat! a.

(I ∧ ¬J)

b.

e.

((I ∧ B) → J)

h.

(I→(¬J→¬B))

k.

I→¬I

n.

(I→J)↔(¬I→¬J)

ö.

I→((¬I↔J)→(B ∨ (I ∧ J)))

l.

¬(I ∧ J) f.

c.

(J↔(I ∧ B) i.

g.

(¬I ∧ ¬B)↔¬J

(I→B)→(B→I)

d.

¬(I ∧ ¬J)

m.

(I→J)

¬J→(¬I ∨ ¬B) j.

(I↔¬B)→¬I

(I→B)→((B→J)→(I→J)

o.(I→J)↔(¬J→¬I)

31

8. feladat  Nulladrend¶ formalizálás

Az alábbi t.ny. mondatok mindegyikének határozza meg az atomi kijelentéseit és írja le az eredeti mondatot ezekb®l összeállított formulaként! a. Kati sem a zöld, sem a kék színt nem szereti. b. Ha fáradt vagy éhes vagyok, nem tudok tanulni. c. Ha fáradt vagy éhes vagyok, nem tudok tanulni, feltéve, ha nem nagyon sürg®s a dolog. c1. Nem igaz, hogy nem vagyok okos. c2. Nem Endre locsolta le Cecíliát. d. Csak akkor megyek haza, ha végeztem a tanulással. e. Ha végeztem a tanulással és nincs még éjszaka, nem taxival megyek haza. f. Ha a szakszervezet vagy a vállalatvezetés makacs, a sztrájk akkor és csak akkor állítható meg, ha a kormány beavatkozik, de nem küld katonaságot az üzembe. g. Nem Endre locsolta le Cecilt, éppen fordítva.

32

Az els®rend¶ logika további logikai jelei Amint láttuk a wumpus-pédában, hasznos lehet, s®t, az érdemi munkához szükséges az állítások nomabb szerkezetének vizsgálata is. A természetes nyelv eszközeinek egy sz¶k készletét veszzük mintának.

33

Az els®rend¶ nyelv eszköztára I. Objektumok leírására

tulajdonnév: konstans (Bodri, Napóleon III.  π, 0) köznév: változó (egy halmaz elemeit közelebbi meghatározás nélkül nevezi meg) (kutya, ember, él®lény 

x, y )

függvényjelekkel képzett összetett nyelvi szerkezet:

függvényjelekkel képzett összetett kifejezés a függvényjel maga egy nyitott kifejezés (. . . apja  . . . + . . . )

tulajdonsággal való leírás:

deskripció (egyel®re nem vesszük be a logikai eszköztárba) (az öreg király legkisebb unokája) A számítástudományban hasznosabb egyb®l az ún. többtípusos objektumleírást használni, mert a legtöbb programozási nyelvben többféle alaptípus (egész, racionális, karakter, stb.) is bennefoglaltatik. A logikában a különböz® típusokhoz diszjunkt változóhalmazokat rendelünk majd hozzá.

34

A wumpus-példa objektumai Milyen típusú objektumok szerepelnek? Szobák, a wumpus pozíciója, a csapda pozíciója, a kincs pozíciója, a h®s pozíciója s két igen/nem érték: hogy megvan-e a nyíl és él-e még a wumpus. Egy lehetséges reprezentáció szerint az alapobjektumok 1 és 4 közötti egész számok, a többi objektumot ezen számok tulajdonságaiként fogjuk fel. A

2. sor és 3. oszlop metszetében van

a wumpusz, formálisan: wumpusz(2,3), ami egy igazságértéket takar, stb.

35

Másik lehetséges reprezentáció Konstansok:

wumpus, kincs, csapda,

h®s

egy típusból és az

{1, 2, 3, 4} egy másik típus tartománya ezzel az a gond, hogy a csapdák száma nem ismert!

36

Állítások leírása Egyszer¶, logikailag nem összetett állítások: atomi formulák Példa:

Péter szereti Julit, Juli szép,

x
Ezek objektumleírásokat ún. nyitott mondatok jeleivel, prediká-

tumjelekkel kötnek össze atomi formulákká. . . . szereti . . . . . . szép

. . . <. . .

37

Logikailag összetett állítások Név

Jel

Kiolvasás

konjunkció diszjunkció negáció implikáció ekvivalencia

∧ ∨ ¬ → ↔

. . . és . . . . . . vagy . . . nem igaz, hogy . . . ha . . . , akkor . . . . . . akkor és csak akkor, ha . . .

propozicionális logikai (állításlogikai, kijeleknek nevezzük, vagy Boole-logikai jeleknek.

Ezeket az összeköt®ket jelentéslogikai)

38

A Boole-logikai jelek jelentése) logikai jel ismer®s középiskolából

39

Két új (középiskolában nem feltétlenül tanult) logikai jel Név

Jel

Kiolvasás

univerzális kvantor egzisztenciális kvantor

∀x ∃x

minden x-re igaz . . . van olyan x, amire . . .

Itt

x tetsz®leges változó.

A logikai jelek minden tárgykör els®rend¶ logikai megfogalmazásában ugyanazok, csak a tárgykör konstansai, függvényjelei és predikátumjelei változnak. Ezeket a tárgykör

nemlogikai

jelkészletének

is nevezzük.

40

A természetes számok tárgyköre Egy

típus

van, a számok típusa

változók legyenek: tozataik, pl.

x,y ,z ,u,v és természetes számmal indexelt vál-

y312

konstansjelet használunk csak, a 0-t Függvényjeleink : +,∗,s Predikátumjeleink : =; kimaradtak az összehasonlító relációjelek! Egy

Mivel a logikai jelek minden els®rend¶ nyelvben azonosak, így ezzel megadtuk a leírható állítások halmazát is!

41

A wumpus-példa típus van, a sorváltozók legyenek:

Egy

és oszlopindexek (számok) típusa

A

x,y ,z ,u,v és természetes számmal indexelt

változataik, pl.

y312 Konstansjelek : 1, 2, 3, 4 Függvényjeleink : s,p (növelés, csökkentés, 1-változós függvényjelek. Ennyi elég, összeadás, szorzás felesleges)

Predikátumjeleink :

=,<, wumpusz , kincs, csapda, aktpozicio  ezek 2-változós predikátumjelek,

el e a szorny , van e nyil  ezek 0-változós predikátumjelek, csak változóktól függetlenül igazak/hamisak lehetnek.

42

A témakörhöz alkotott els®rend¶ nyelv meghatározása az informatikai modellezés els®, alapvet® lépése Az objektumok szerkezetét, összefüggéseinek struktúráját adjuk ezzel meg. Már itt el lehet rontani: pl. ha a csapdákat csak egy konstansjellel ábrázoltuk volna, determináltuk volna a modelleinket úgy, hogy csak egy csapdát tartalmazhat a pálya.

43

Példa: els®rend¶ nyelv az emberek viszonyainak leírására Legyen

EmbV iszony egy olyan nyelv, amiben x, y, z, ... egyetlen típusú változók, apa(x), anya(x) függvényjelek, c, ÉN konstan-

(x=y), ifjabb(x,y), szereti(x,y), tiszteli(x,y), n®(x), öreg(x), gazdag(x), házastarsa(x,y) predikátumjelek. A nyelv értelmezése sjelek,

mindenki számára nyilvánvaló, ha hozzátesszük, hogy a ma vagy valaha élt emberek halmaza lesz az objektumtartomány. Mi a helyzet az

apa függvénnyel? Van els® ember?  Megint

a nyelv választása már fontos dolgokat meghatároz!

A függ-

vényekkel csínján kell bánni: minden bemen® értékre egyértelm¶ értéket kell produkálnia a függvényjel értelmezésének.

44

SZINTAXIS

45

Az els®rend¶ nyelv deníciója 1. deníció: Minden els®rend¶ nyelv megadható < Srt, Cnst, F n, P r > rendezett 4-es alakjában,

1.

nemüres ábécé, elemei típusokat szimbolizálnak, és minden típushoz egyben Srt megad a megfelel® típushoz rendelt változók végtelen, felsorolható halmazát. 2. Cnst a konstansszimbólumok halmaza, minden konstansjelhez Cnst egyben hozzárendel egy típust is. 3. F n halmaz elemei függvényszimbólumok, minden függvényjelhez F n egyben hozzárendel egy típust is. 4. P r nemüres halmaz, elemei predikátumszimbólumok, minden predikátumjelhez P r egyben hozzárendel egy típust is. Srt

nemüres, mert legalább egy objektumtípusnak lennie kell, és P r sem üres, mert a nem összetett állítások felírásához legalább egy szükséges. F n és Cnst lehet üres. Az els®rend¶ nyelvnek ez a jelkészlete, idegen szóval szignatúrája. Ahányféle jelkészletet választhatunk, annyiféle els®rend¶ nyelvet deniálhatunk. A pontos deníciót lásd a PVK-VM könyv 111. oldalán ( → lsd. kötelez® irodalom) Srt

46

A hozzárendelt típusok Bármely

A

konstanshoz

függvényjelekhez

egyetlen típust rendel hozzá

Cnst.

F n egy pozitív természetes számot (vál-

tozószám) rendel, és a megadott számnyi hosszúságú listáját típusoknak (az egyes argumentumok típusát), végül még egyetlen típust, a függvény kimen® értékének típusát. A

predikátumjelek

esete annyiban különbözik, hogy ott a kimen®

érték típusát nem kell megadnia

P r-nek, mert az minden esetben a logikai igaz/hamis lesz. Tehát minden predikátumjelhez P r egy természetes számot (változószám) rendel (nincs kikötve, hogy pozitív, tehát lehet 0 is!),valamint a megadott számnyi hosszúságú listáját típusoknak (az egyes argumentumok típusát).

47

Példa: az

EmbViszony nyelv,

mint els®rend¶

jelkészlet A nyelvben x, y, z, ... egyetlen típusú változók lesznek, a típus neve legyen e. Bármely konstanshoz egyetlen típust rendel hozzá Cnst. { } a konstansjelek halmaza, mindkett® típusa e. c, ÉN

A függvényjelekhez F n egy természetes számot (változószám) rendel, és a megadott számnyi hosszúságú listáját típusoknak (az egyes argumentumok típusát), végül még egyetlen típust, a függvény kimen® értékének típusát.

Kételem¶ a függvényjelek halmaza, {

apa, anya

}, mindkett® típusa

(e→ e)

Minden predikátumjelhez P r egy természetes számot (változószám) rendel, valamint a megadott számnyi hosszúságú listáját típusoknak (az egyes argumentumok típusát).

{ }a predikátumjelek halmaza, ahol -et írtunk a jel után, azt jeleztük, hogy 2-argumentumú predikátumjelr®l van szó, típussal, ahol -et írtunk a jel után, azt jeleztük, hogy 1-argumentumú predikátumjelr®l van szó, típussal. (x=y), ifjabb(x,y), szereti(x,y), tiszteli(x,y), n®(x), öreg(x), gazdag(x), házastarsa(x,y) (x,y)

(e,e)

(x)

(e)

Ahol a predikátumjelet középre írtuk ( x=y ), ott úgynevezett inx írásmódot használunk, a többinél prex írásmódot.

48

Példa: az

EmbViszony nyelv

formális leírása

A nyelvben x, y, z, ... egyetlen típusú változók lesznek, a típus neve legyen e. Bármely konstanshoz egyetlen típust rendel hozzá Cnst. { c, ÉN } a konstansjelek halmaza, mindkett® típusa e. Kételem¶ a függvényjelek halmaza, {apa, anya}, mindkett® típusa (e→ e) Minden predikátumjelhez P r egy természetes számot (változószám) rendel, valamint a megadott számnyi hosszúságú listáját típusoknak (az egyes argumentumok típusát). {(x=y), ifjabb(x,y), szereti(x,y), tiszteli(x,y), n®(x), öreg(x), gazdag(x), házastarsa(x,y)} a predikátumjelek halmaza. Ezt a nyelvet formálisan a következ®képp fogjuk leírni: < {e(x,y,z,...)}, {c(e), EN (e)}, {apa(e→e), anya(e→e)}, {=(e,e),inf ix, if jabb(e,e), szereti(e,e), tiszteli(e,e), no(e), oreg (e), gazdag (e), hazastarsa(e,e)} >

Ez az írásmód még az olvasónak kedvez, nem egy az egyben vihet® át programozási nyelv adatszerkezetévé. De könnyen megtehet®. 49

Kifejezések (term-ek) 2.

deníció:

Egy

< Srt, Cnst, F n, P r > els®rend¶ jelkészlet

feletti egyszer¶ term-ek a változók és a konstansok.

Típusuk

a jelkészletben megadott. Az összetett term-ek

f (t1, . . . , tn) alakúak, ahol f egy F n-beli

függvényjel valamilyen

(π1, . . . , πn → π) típussal, és t1, . . . , tn már meglév® term-ek, rendre π1 , . . . , πn típussal. Ekkor az új term π típusú lesz. Term-ek az egyszer¶ term-ekb®l az összetétel szabályának véges számú alkalmazásával el®álló jelsorozatok.

Megjegyzés: Ezen jelsorozatok ábécéje a jelkészlet ábécéje, kib®vítve a '(',

')', ',' karakterekkel. 1. állítás: A termek halmaza a kib®vített jelkészlet, mint ábécé feletti szavak azon legsz¶kebb halmaza, amely tartalmazza a változókat és a konstansokat, és zárt a típushelyes összetételre (azaz ahogy fentebb megadtuk).

50

Példa Az

EmbViszony

nyelv egyszer¶ termjei

ÉN, c, x, y, z, . . . míg

összetett termjei pl.:

apa(x) , apa(N ), anya(y), anya(apa(c)), stb. A nyelv ez volt: < {e(x,y,z,...)}, {c(e), EN (e)}, {apa(e→e), anya(e→e)},

{=(e,e),inf ix, if jabb(e,e), szereti(e,e), tiszteli(e,e), no(e), oreg (e), gazdag (e), hazastarsa(e,e)} >

51

Az

Példa az aritmetika

Ar

Ar

0, x, y, z, u, v, w. . . és

nyelv egyszer¶ termjei

nyelvének term-jeire a változók

indexelt verziói. Összetett termjei pl.:

(x + y) , s0, (x ∗ (y + s0)), ((x12 ∗ (y + s0)) + (y3 ∗ sy)), stb. Az

Ar nyelv ez volt: < {sz (x,y,z,u,v,w,x1,...)}, {0(sz)}, {+(sz,sz→sz),inf ix, s(sz→sz), ∗(sz,sz→sz),inf ix}, {=(sz,sz),inf ix} >

52

Szintaktikai fogalmak a termekr®l 3. deníció: Egy egyszer¶ termnek nincsenek közvetlen résztermjei. Az összetett f (t1 , . . . , tn ) term közvetlen résztermjei a t1 , . . . , tn termek. Egy term résztermjei: önmaga, közvetlen résztermjei és a közvetlen résztermjeinek résztermei.

Pontosabban megfogalmazva: Egy adott term résztermjeinek a halmazát

úgy deniáljuk, mint a jelsorozatok azon legsz¶kebb részhalmazát, ami tartalmazza a termet magát, közvetlen résztermjeit, valamint igaz az rá, hogy ha egy termet tartalmaz, akkor annak összes közvetlen résztermjét is tartalmazza. Változókat használva az értelmezés megkönnyítésére: Egy t term résztermjeinek a halmazát úgy deniáljuk, mint a jelsorozatok azon legsz¶kebb részhalmazát, ami tartalmazza t-t, t közvetlen résztermjeit, valamint igaz az rá, hogy ha egy s termet tartalmaz, akkor s összes közvetlen résztermjét is tartalmazza.

53

A szerkezeti indukció elve termekre 2. állítás: Ha T jelsorozatok egy tulajdonsága, és

1. minden

c ∈ Cnst teljesíti T -t 2. minden v változó teljesíti T -t 3. valahányszor, amikor t1 , . . . , tn termek mindegyike teljesíti T t, ezen termek típusa rendre π1 , . . . , πn és f (π1 ,...,πn −π) ∈ F n, annyiszor f (t − 1, . . . , tn ) is teljesíti a T tulajdonságot

akkor minden term teljesíti a

T tulajdonságot.

Megjegyzés: A teljes indukció elvének felel meg fa szerkezet¶ adatokon.

54

Példa szerkezeti indukcióval igazolt állításra 3. állítás: a) Minden term ugyanannyi kezd®, mint csukó zárójelet tartalmaz. b) Bármely term, mint jelsorozat bármely kezd®szelete legalább annyi nyitó zárójelet tartalmaz, mint csukót. c) Bármely

t termre igaz: vagy változó, vagy konstans, vagy léteznek olyan t1 , . . . , tn termek, rendre π1 , . . . , πn típussal és létezik olyan f (π1 ,...,πn →π) ∈ F n, amire t = f (t1 , . . . , tn ). (A termek egyértelm¶ elemzésének tétele)

55

A term szerkezeti fája Rendezett fa: összefügg® és körmentes irányított gráf. Véges fának létezik egyamely egyértelm¶ gyökere, annak nincsúgy®se,nevezzük, minden levél. egyéb csúcsnak van egy egyértelm¶ szül®je, csúcsnak nincs gyermeke, Emlékeztet®:

(((2+2)+(2+2))+(3+3))

4. deníció: Egy term szerkezeti fája egy olyan véges rendezett fa, amelynek

gyökerében maga a term áll, s minden csúcspontjában egy term áll. Ha egy csúcsban az f (t1, . . . , tn) összetett term áll, akkor a csúcsnak pont n darab gyereke van, amiben éppen t1, . . . , tn állanak. Ha egy csúcsban egyszer¶ term áll, akkor az levél. 4. állítás: Minden termhez egyértelm¶en rendelhet® egy kifejezésfa (kölcsönösen egyértelm¶ leképezés).

Itt még a gyermekek sorrendjét is megemlíthetnénk, a pontosság kedvéért.

56

Termek szerkezeti rekurziójáról szóló állítás Lehetséges úgy deniálni egy termeket illet® fogalmat, hogy a fogalmat direkt meghatározzuk az egyszer¶ termeken, míg az

f (t1, . . . , tn) összetett termre vonatkozó fogalmat a t1, . . . , tn termekre vonatkozó hasonló fogalmak segítségével építünk fel.

57

Példa szerkezeti rekurzióval deniált fogalmakra  rthz(t) :=

 f o(t) :=

{t} {t} ∪ rthz(t1 ) ∪ . . . ∪ rthz(tn )

ha t egyszer¶ ha t = f (t1, . . . , tn) összetett term

0 1 + max{f o(ti ) | ti résztermje t-nek}

ha t egyszer¶ ha t összetett

Megjegyzés: f o(t) egy számot ír le, mégpedig a függvényalkalmazások egymásbaágyazásának t-béli maximális értékét. ( A leghosszabb ág hossza a szerkezeti fában a gyökért®l számítva.) Úgy hívjuk, hogy funkcionális összetettség.

58

Kifejezések II. (formulák) 5.

deníció:

Egy < Srt, Cnst, F n, P r > els®rend¶ jelkészlet feletti atomi formulák P (t1 , . . . , tn ) alakúak, ahol P egy P r -beli predikátumjel valamilyen (π1 , . . . , πn ) típussal, és t1 , . . . , tn már meglév® term-ek, rendre π1 , . . . , πn típussal. Bármely A, B formulákra és v változóra formula a következ® jelsorozatok bármelyike: (A ∧ B), (A ∨ B), (A→B), (A↔B), ¬B , ∀vA, ∃vA. Ezeket nevezzük logikailag összetett formuláknak. Formulák az atomi formulákból a logikai összetételek véges számú alkalmazásával el®álló jelsorozatok.

Megjegyzés: Ezen jelsorozatok ábécéje a jelkészlet ábécéje, kib®vítve a '(', ')', ',' '∧', '∨', '→', '↔, '¬', '∀','∃' karakterekkel. 5. állítás: A formulák halmaza a kib®vített jelkészlet, mint ábécé feletti szavak azon legsz¶kebb halmaza, amely tartalmazza az atomi formulákat, és zárt a logikai összetételre (azaz ahogy fentebb megadtuk).

59

Példa EmbViszony nyelv atomi formulái pl. szereti(EN,EN), szereti(EN,anyja(x)), no(anyja(apja(y))), szereti(apja(x),anyja(y)) . . . Az

míg összetett formulái pl.: (

szereti(x, y) ∧ ¬szereti(x, anyja(y))) , ∀x szereti(x, anyja(x)), (∀x∃y szereti(y, x)→∀x∃y szereti(anyja(y), apja(x))) stb. Az illet® nyelv ez volt: < {e(x,y,z,...)}, {c(e), EN e}, {apa(e→e), anya(e→e)},

{=(e,e),inf ix, if jabb(e,e), szereti(e,e), tiszteli(e,e), no(e), oreg (e), gazdag (e), hazastarsa(e,e)} >

60

Példa az aritmetika Az

Ar

Ar

nyelvének formuláira

nyelv atomi formulái

(0 = s0), (x = (ssss0 + s0)), (sy = sx), . . . Összetett formulái pl.:

∀x((x + x) = 0) , ((s0 = x) ∧ ¬(s0 = x)), ∀x∀y (((x ∗ (y + s0)) = sss0)→(x = y)), stb. Az

Ar nyelv ez volt: < {sz (x,y,z,u,v,w,x1,...)}, {0(sz)}, {+(sz,sz→sz),inf ix, s(sz→sz), ∗(sz,sz→sz),inf ix}, {=(sz,sz),inf ix} >

61

Szintaktikai fogalmak a formulákról 6. deníció:

Az Az Az Az Az Az Az

atomi formuláknak nincsenek közvetlen részformulái. összetett (A ∧ B) formula közvetlen részformulái épp az A és B formulák. összetett (A ∨ B) formula közvetlen részformulái épp az A és B formulák. összetett (A→B) formula közvetlen részformulái épp az A és B formulák. összetett (A↔B) formula közvetlen részformulái épp az A és B formulák. összetett ∀vA formula közvetlen részformulája az egyetlen A formula. összetett ∃vA formula közvetlen részformulája az egyetlen A formula.

7. deníció: Egy adott formula részformuláinak a halmazát úgy deniáljuk, mint a jelsorozatok azon legsz¶kebb részhalmazát, ami tartalmazza a formulát magát, közvetlen részformuláit, valamint igaz az rá, hogy ha egy formulát tartalmaz, akkor annak összes közvetlen részformuláját is tartalmazza.

62

A szerkezeti indukció elve formulákra 6. állítás: Ha T jelsorozatok egy tulajdonsága, és

1. minden atomi formula teljesíti

T -t 2. mindahányszor, amikor A és B formulák teljesítik T -t és v egy változó, akkor (A ∧ B), (A ∨ B), (A→B), (A↔B), ¬B , ∀vA, ∃vA is teljesíti T -t

akkor minden formula teljesíti a

T tulajdonságot.

Megjegyzés: A teljes indukció elvének felel meg fa szerkezet¶ adatokon. (Teljes felszállás a szerkezeti fán. . . )

63

Példa szerkezeti indukcióval igazolt állításra

7. állítás: a) Minden formula ugyanannyi kezd®, mint csukó zárójelet tartalmaz. b) Bármely formula, mint jelsorozat bármely kezd®szelete legalább annyi nyitó zárójelet tartalmaz, mint csukót. c) Bármely A formulára igaz: vagy A atomi formula, vagy egyértelm¶en léteznek olyan B és C formulák, amelyekre A = B ∧ C , vagy egyértelm¶en léteznek olyan B és C formulák, amelyekre A = B→C , vagy egyértelm¶en léteznek olyan B és C formulák, amelyekre A = B ∨ C , vagy egyértelm¶en léteznek olyan B és C formulák, amelyekre A = B↔C , vagy egyértelm¶en létezik olyan B formula, amelyre A = ¬B , vagy egyértelm¶en létezik olyan B formula és v változó, amire A = ∀v B , vagy egyértelm¶en létezik olyan B formula és v változó, amire A = ∃v B . (A formulák egyértelm¶ elemzésének tétele)

64

A formula szerkezeti fájáról

8. deníció: Egy fa szerkezeti fája egy olyan véges rendezett fa, amelynek

gyökerében maga a formula áll, s minden csúcspontjában egy formula áll. Ha egy csúcsban az A ∧ B összetett formula áll, akkor a csúcsnak pont 2 darab gyereke van, amiben éppen A és B állanak. Ha egy csúcsban atomi formula áll, akkor az levél.

Itt még a gyermekek sorrendjét is megemlíthetnénk, a pontosság kedvéért.

8. állítás: Megjegyzés: Minden termhez egyértelm¶en rendelhet® egy szerkezeti fa (kölcsönösen egyértelm¶ leképezés).

65

Formulák szerkezeti rekurziójáról szóló állítás Lehetséges úgy deniálni egy, a formulákat érint® fogalmat, hogy a fogalmat direkt meghatározzuk az atomi formulák esetére, míg az összetett formulára vonatkozó fogalmat a fogalomnak a közvetlen részformulákra vonatkozó hasonló fogalmak segítségével adjuk meg.

66

Példa szerkezeti rekurzióval deniált fogalmakra, formulák esetén   {A} rf (t) := {A} ∪ rf (B) ∪ rf (C)  {A} ∪ rf (B) ( lo(t) :=

0 1 + max({lo(B), lo(C)}) 1 + lo(B)

ha A atomi ha A-nak épp ha A-nak épp

B B

és C a két közvetlen részformulája az egyetlen közvetlen részformulája

haha -nak atomiéppformula és a két közvetlen részformulája ha -nak az egyetlen közvetlen részformulája éppen A A A

B

C

B

Megjegyzés: lo(A) egy számot ír le, mégpedig a logikai összeköt®jelek alkalmazásai egymásbaágyazásának A-béli maximális értékét. ( A leghoszszabb ág hossza a szerkezeti fában a gyökért®l számítva.) Úgy hívjuk, hogy logikai összetettség. rt(A) pedig az A formula összes részformuláinak halmazát adja meg.

67

Zárójelelhagyási megállapodások

A könnyebb olvashatóság kedvéért , amikor emberi kommunikáció során formulákat, termeket írunk, a rengeteg zárójelpár közül néhányat elhagyhatunk. A következ® megállapodások betartásával a rövidített verzióból egyértelm¶en visszaállítható az eredeti kifejezés. 1. Kifejezés küls® zárójelpárját elhagyhatjuk 2. Megállapítunk egy precedenciasorrendet∗: a leger®sebbek a függvényjelek aztán a predikátumjelek aztán a ∀, ∃ és a ¬ következik (ezek hárman egyforma er®sek) ∧ és ∨ → ↔

* amelyik er®sebb, az köt er®sebben 3. Azonos precedenciájú jelek közül a baloldali lesz az er®sebb

68

9. feladat Milyen volt az ítéletlogikai formula zárójelelhagyás el®tt?

a.

A ∧ B→¬C→¬A↔¬A

b.

¬A ∧ ¬B→(¬C→B↔¬A)→¬B

c.

(A ∧ B ∨ A ∧ ¬A ∧ B ∨ ¬B) ∧ A

69

10. feladat Részformulája-e az alábbi formula

a.

¬A→B

b.

A→B

c.

¬B

d.

A∧B

¬A→B ∨ (A ∧ B→¬C)-nek?

Sorolja fel a fenti formula összes részformuláját!

70

11. feladat Legyen

L12 nyelv: < {t1(x,y,z,...) , t2(α,β,γ,...) }, {c1(t1) , c2(t2) }, {f (t1→t1) , g (t2→t1) , h(t2,t1→t1) , i(t2→t2) }, {P (t1) , Q(t1,t2) , R(t2,t2) }, S (t2) >.

nyelv formulája-e a következ® jelsorozat ( zárójelelhagyási szabályokat megengedve)? L12

a. f.

P (α) b. P (x) c. S(α, β) d. R(α→β) (S(α)→P (y)) g. Q(c1, c2)→Q(P (x), c2) h. f (x) j. P (f (f (x))) k. P (Q(x, α))

e.

S(α)→P (y)→S(x, y, x) Q(c2, c1)↔Q(c1, c1) i.

nyelvnek termje-e a következ® jelsorozat? Ha igen, mi a típusa, mik a változói és mi a funkcionális összetettsége? L12

a. g.

x b. f (x) f (g(f (c2)))

c. g(x) d. f (g(c2)) e. g(f (g(c2))) f. h. h(i(α), h(c2, x)) i. h(i(i(c2)), h(c2, g(c2)))

g(f (g(c1)))

71

12. feladat Legyen Geom nyelv a következ®: < {p(A,B,C,...), e(e,f,g,...), s(a,b,c,...)}, ∅, ∅, (p,e),inf ix (p,s),inf ix {∈1 , ∈2 , =(p,p),inf ix} >.

Geom nyelv formulája-e a következ® jelsorozat ( zárójelelhagyási szabályokat nem megengedve)?

a.

A ∈1 e b. (e ∈1 A) c. (A ∈1 e) d. (A ∈2 e) e. (A ∈1 A) f. (A ∈2 a) g. (A ∈1 e)→(B ∈2 e) h.

((A ∈1 e)→(B ∈2 e)) i. ((A ∈1 e)→(B ∈2 a)) j. ∀A(¬(A ∈1 e)) k. ∀B¬(A ∈1 e) l. ∀A∃B(A ∈1 e) m. ∀A∃A(A ∈1 e) n. ∀A(B ∈1 f )

72

13. feladat Adjunk meg olyan els®rend¶ nyelvet (jelkészletet), amelynek formulája lehet a következ® jelsorozat!

a.

P (x)

b.

P (x)→Q(y, f (x, y))

c.

Q(R(α, x), y)

d.

∀αf (α)

Innent®l kezdve, ha nem adom meg, hogy mely nyelv termjeir®l és formuláiról van szó, akkor úgy kezd®dik a feladat, hogy meg kell határozni egy alkalmas nyelvet!

73

14. feladat Írjuk fel az alábbi

L12-formulák teljes zárójeles alakját! Mik az

egyes formulák részformulái? Mennyi a logikai összetettségük?

a.

Q(f (g(c2)), c2) b. ∃x ¬ Q(x, β) c. ∃x ¬ Q(x, β)→ ∀α R(α, β) d. ¬ P (c1)→ ¬ S(α) ∨ S(α) ∨ S(β) → P (x) ∨ P (y)

74

Termek és formulák szabad és kötött változó-el®fordulásai   ha t változó {t} szv(t) := ∅ ha t konstansjel  szv(t ) ∪ . . . ∪ szv(t ) ha t = f (t , . . . , t ) n n 1 1  A = P (t1 , . . . , tn ) szv(t1) ∪ . . . ∪ szv(tn) szv(A) :=

haha haha

szv(A) ∪ szv(B) szv(A) szv(B) \ {v}

, vagy

atomi,

A = B ∧ C A = B ∨ C A = B→C A = ¬B A = ∀v B A = ∃v B

vagy

A = B↔C

9. deníció: Kvantornak nevezzük a ∀-t és a ∃-et. Kvantor hatásköre egy

formulában: az a részformula, amire rátettük a formula szerkezeti fájának konstrukciójakor. Kötött változóel®fordulás: ami olyan kvantor hatáskörébe esik, ami épp arra a változóra vonatkozik. Szabad változóel®fordulás: Ami nem kötött. Formula szabad változói: azon változók halmaza, aminek van a formulában szabad el®fordulása. Más néven: formula paraméterei.

9. állítás:

szv(A)

minden

A

formula esetén épp

maza. Bizonyítás: szerkezeti indukcióval

A

szabad változóinak hal-

75

15. feladat Tekintsük a következ®

L12-formulákat!

Mik a szerepl® kvan-

torok hatáskörei? Mik az egyes formulákban el®forduló szabad változók?

a. b. c. d. e.

∃x ¬ Q(x, β)→ ∀α R(α, β) ¬ P (c1)→ ¬ S(α) ∨ S(α) ∨ S(β) → P (x) ∨ P (y) ∀x(∃xP (x) → Q(x, c2)) ∀x(∃α(Q(x, α)→¬S(β)) ≡ ∀y(P (y)→∃α¬∃βQ(y, α) ∧ R(β, α))) ∀x(∃α(Q(x, α)→¬S(β)) ≡ ∀y(P (y)→∃α¬∃β(Q(y, α) ∧ R(β, α))))

76

16. feladat Írjuk fel az alábbi

Geom-formulák teljes zárójeles alakját! Mik a

szerepl® kvantorok hatáskörei? Mik a szabad változók? a.

¬ A ∈1 e b. A = B ∧ ¬ B ∈1 e c. ¬ A = B ∨ ¬ ∀ C C = A d. ∀ A (A ∈2 a→∃ e A ∈1 e→B ∈2 a) e. ∀ e (∃ A A ∈1 e ∨ ∃ B ¬ B ∈2 a)→A = B

77

17. feladat Írjuk fel az alábbi

Ar-formulák teljes zárójeles alakját!

szerepl® kvantorok hatáskörei? forduló szabad változók?

Mik a

Mik az egyes formulákban el®-

Használjuk azt az információt, hogy

a precedenciában leger®sebbek a függvényjelek, aztán a predikátumjelek, aztán

{∃, ∀}, ¬, {∧, ∨}, →, ↔, valamint a függvényjeleken belül is megállapítottunk egy precedenciasorrendet: itt S a leger®sebb, aztán × jön, végül +. a.

∀x∃x Sx = y b. ∀x∃y ¬ Sx = SSy c. ∀x∃y Sz = y d. ∀x¬∃y Sx = y ∨ y + z = x e. x + Sy × Sz + SS0 + y × z = x × x→Sx × y = S(x × y) f. ∀x (¬ x × Sx = Sx × y ∨ x = S0)→∃y (Sy = S0 ∧ x × x = y)

78

SZEMANTIKA

79

Az els®rend¶ nyelv interpretációja intuitív módon

1. megadunk minden típushoz egy alaphalmazt, 2. a konstansokhoz a megfelel® típusú alaphalmazból kijelölünk egy egyedet, 3. a függvényjelekhez megfelel® típusú függvényt, 4. a predikátumjelekhez megfelel® típusú relációt rendelünk.

Röviden: típushelyesen értelmezzük a szóbanforgó nyelv jelkészletének elemeit.

80

Az els®rend¶ nyelv interpretációja  példa Példa:

Legyen

L1

nyelv:

< {t1(x,y,z,...) , t2(α,β,γ,...) }, {c1(t1) , c2(t2) }, {f 11(t1→t1) , f 221(t2,t2→t1) , f 212(t2,t1→t2) , f 22(t2→t2) }, {P 1(t1) , P 12(t1,t2) , P 22(t2,t2) }, P 2(t2) >.

típus változóinak értékei a természetes számok halmazából kerülhetnek ki, t2 típus változóinak értékei a magyar nyelv bet¶ib®l és egyéb írásjeleib®l alkotott jelsorozatokból kerülhetnek ki, c1 a 4-t jelölje, c2 az "aabx" jelsorozatot, f 11 minden természetes számhoz a négyzetét rendelje, f 221 bármely két szóhoz a mindkét szóban jelenlév® bet¶k számát rendelje, f 212 egy adott w szóhoz és adott n számhoz w-nek az n hosszú kezd®szeletét rendelje, ha n nem nagyobb, mint w hossza, egyébként magát w-t, míg f 22 minden szóhoz a fordítottját rendelje. Ezennel értelmeztük L1 termjeit. IP r (P 1)(n) akkor és csak akkor legyen igaz, ha n páros. IP r (P 12)(n, w) akkor és csak akkor legyen igaz, ha n kisebb, mint w hossza. IP r (P 22)(w1, w2) akkor és csak akkor legyen igaz, ha w1 rövidebb, mint w2. IP r (P 2)(w) akkor és csak akkor legyen igaz, ha w önmaga megfordítása. Mindezek megadása együtt jelenti azt, hogy megadtuk L1 egy interpretációját. t1

81

Az els®rend¶ nyelv interpretációja

nyelv egy interpretációja alatt a következ® matematikai objektumot értjük: I =< ISrt, ICnst, IF n, IP r > rendezett 4-est, ahol L =< Srt, Cnst, F n, P r >

1.

egy olyan függvény, ami Srt minden eleméhez egy nemüres halmazt rendel, 2. ICnst egy olyan függvény, ami Cnst minden eleméhez egy neki megfelel® típusú elemet rendel, azaz, ha c(τ ) ∈ Cnst, akkor ICnst(c) eleme ISrt(τ )nak. 3. IF n egy olyan függvény, ami F n minden függvényjeléhez egy neki megfelel® típusú függvényt rendel, ami az alaphalmazok megfelel® Descartes-szorzatán operál. Azaz, ha f (τ ,...,τ →τ ) ∈ F n, akkor IF n(f ) egy olyan függvény lesz, ami ISrt(τ1) × . . . × ISrt(τn)-b®l ISrt(τ )-ba képez. 4. ISrt egy relációt rendel bármelyik predikátumjelhez. Pontosan: ha P (τ ,...,τ ) ∈ P r, akkor IP r (P ) egy olyan függvény lesz, ami ISrt (τ1 ) × . . . × ISrt (τn )-b®l az igazságértékek {i, h} halmazába képez. ISrt

1

n

1

n

ISrt (t)-t röviden tI -nek fogjuk jelölni, ha t típus. Ha c konstans, cI -vel jelöljük ICnst(c)-t, hasonlóan, ha f függvényjel, f I -vel jelöljük IF n(f )-t és ha P predikátumjel, P I -vel jelöljük IP r (P )-t.

82

Változóértékelés Ha egy nyelvnek meg is adtuk az interpretációját, akkor a szabad változót tartalmazó formulák jelentése még mindig határozatlan: Pl.

L1 említett interpretációjában az még a paraméterek értékét®l függ, hogy P (x, c) igaz lesz-e vagy hamis. Azt I megadta, hogy mit jelent P és c, de az interpretáció nem mondja meg a változók értékét.

10. deníció: Ha L nyelvnek I egy interpretációja, akkor egy

I feletti változóértékelésnek egy olyan Ω függvényt nevezünk, amely értelmezési tartománya L nyelv változóinak halmaza, és értékkészlete része az ISrt képei uniójának ( a típusokhoz tartozó alaphalmazok uniója), és ha v az τ típusú változó, akkor Ω(v) ∈ ISrt(τ ).

83

Értékelt termek interpretációbeli értéke |t|I,Ω-t fogjuk deniálni, t term I interpretációbeli értékét Ω változóértékelés mellett.

11. deníció:

|t|I,Ω =

   ICnst(t)

ha

  

ha

Ω(t) (IF n(f ))(|t1|I,Ω, . . . , |tn|I,Ω)

Megjegyzés: Ez tipikus szerkezeti rekurziós deníciója a

t konstansjel ha t változó

összetett term fogalomnak.

t = f (t1 , . . . , tn )

| . . . |I,Ω

84

Értékelt formulák interpretációbeli igazságértéke

kAkI,Ω-t fogjuk deniálni, A formula I interpretációbeli igazságértékét Ω változóértékelés mellett. 12. deníció:

haha atomi formula haha haha ésés      ha    ahol egy típusú változó és   ahol egy típusú változó és ahol -t -gyel és -t -val tekintjük megegyez®nek. a leképezés egy helyen való módosítot verzióját jelenti, amely csak -n felvett értékében különbözik az eredeti -tól, és -t vesz föl, azaz . Megjegyzés: Ez tipikus szerkezeti rekurziós deníciója a fogalomnak. 85

kAkI,Ω =

i

 (IP r (P ))(|t1 |I,Ω , . . . , |tn |I,Ω )    min{kBkI,Ω , kCkI,Ω }     max{kBkI,Ω , kCkI,Ω }   max{1 − kBkI,Ω, kCkI,Ω}

1

A = P (t1 , . . . , tn ) A=B∧C A=B∨C A = B→C A = B↔C kBkI,Ω = kCkI,Ω A = B↔C kBkI,Ω 6= kCkI,Ω A = ¬B v τ A = ∀vB v τ A = ∃vB

1 0 1 − kBkI,Ω min{kBkI,Ω@(v→d) |d ∈ ISrt (τ )} max{kBkI,Ω@(v→d) |d ∈ ISrt (τ )} h

Ω@(v → d)

0

d

d

Ω

Ω

Ω@(v → d)(v) = d

k . . . kI,Ω

Interpretációban igaz értékelt formula 13. deníció: Azt mondjuk, hogy I interpretációban igaz az A formula a

Ω értékelés mellett, ha kAkI,Ω = 1. Természetesen,

hamis értékelt formula az, ami nem igaz. Ezt úgy is fogjuk jelölni, hogy pedig

I |= AΩ, ha nem teljesül, akkor

I |6 =AΩ-t írunk.

86

Matematikai struktúra vagy modell

14. deníció: Matematikai struktúrának, vagy modellnek, vagy röviden,

struktúrának nevezünk egy olyan objektumot, ami egy vagy több halmazból, és ezeken a halmazon értelmezett függvények és relációk egy sorozatából áll. Például, bármely nyelv bármely interpretációja struktúra, s®t, minden struktúrához kitalálható olyan nyelv, ami alapján a nyelv interpretálható. Ezt úgy is fogjuk nevezni, hogy a struktúra az adott nyelv modellje. Például, a (Z, +, ∗) struktúra interpretáció egy olyan nyelv számára, ahol van egy típus, 2 darab 2-változós függvényjel és egy = nev¶, 2-változós predikátumjel (ez utóbbi mindig kell, ha függvényjelek vagy konstansok vannak a jelkészletben), ahol az =-nek a szokásosan kell lennie interpretálva, egyenl®ségként. Megjegyzés: a diszkrét matematikában azokat a struktúrákat nevezik algebrai struktúrának, ahol más predikátumjel nincs, csak az =, és az is szokásosan van interpretálva. Ilyen értelemben mondjuk azt pl., hogy

(Z, +, ∗) |= ∀x∀z∃y x + y = z .

87

Legyen a következ® nyelv: . nyelv interpretációját a következ®kkel adjuk meg, ahol egy jel interpretáltját -mel fogjuk jelölni. , , , n ha halmaz minden elemére egyébként halmaz minden , elemére , n 10 egyébként ha halmaz bármely , elemeire interpretációsa táblázata: 01 10 23 01 40 88 < {t(x,y,z,...) }, {c(t) , d(t) }, {f (t→t) , g (t,t→t) }, {P (t) , Q(t,t) , R(t,t) } >

L1

L1

M

j

MSrt (t) = {0, 1, 2, 3, 4}

˜ cM := 2 d˜M := 3 A

a

A

ab

A

ab

P˜

P˜

f˜(a) :=

a + 1, 0

a<4

˜ (g)(a, b) := |a − b| ˜ R(a, b) :=

,

a+b=3

˜ jM

interpretációs táblázata: 0 1 2 3 4 01 10 01 10 00 11 23 01 01 00 00 10 4 11111  Mennyi az alábbi értékelt termek értéke? a.   b.  Mely értékelt  formulák igazak -ben? a.   b.   c.   d. e.f. g. ˜ Q

˜ Q

g(g(c, d), f (d))

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

y 3

M

x R(x, y) 2 y R(x, y) 2

y 3 z 2

x 1

x y R(x, y)→R(y, x) 2 1 y ∀xR(x, y) 2 ∃y∀xR(x, y) ∃y∃xR(x, y) ∃y∀x(R(x, y) ∨ R(y, x))

h.i. j.k. l. Van-e olyan értékelés, ami igazzá teheti az alábbi formulákat ebben a modellben? a.c. b. d. e. f. g. ∃y∀xR(x, y)→∀x∃yR(x, y) ¬∀x∀yR(x, y)→∀x∀yR(x, y) ∀x(¬existsyQ(x, y) ∧ P (x)→∃z(R(z, z) ∧ R(z, x))) ∀xR(x, f (x)) ∃x∀y(R(f (x), f (y)) ∧ ¬R(x, y))

∀xR(y, x) ∀x¬R(y, x) R(y, x) ∧ R(x, y) R(y, x) ∧ ¬R(x, y) ¬∃yR(x, f (y)) R(x, c) ∧ ¬∃yR(x, y)

R(g(x, x), x)

Hogyan módosulnak a válaszok az el®bbi feladat kérdéseire, ha az predikátumjel fent adott interpretációja helyett mást választunk, a következ®ket: n 10 egyébként ha a. Az alaphalmaz halmaz bármely , elemeire n 10 egyébként ha b. Az alaphalmaz halmaz bármely , elemeire n 10 egyébként ha osztja -t c. Az alaphalmaz halmaz bármely , elemeire R

ab

˜ R(a, b) :=

,

a+b≤3

ab

˜ R(a, b) :=

,

a=3∨b≤2

ab

˜ R(a, b) :=

,

a

b

89

18. feladat: Formulák igazságértéke a wumpus-világ egy modelljében

90

A wumpus-példa, ismétlés típus van, a sorváltozók legyenek:

Egy

és oszlopindexek (számok) típusa

A

x,y ,z ,u,v és természetes számmal indexelt

változataik, pl.

y312 Konstansjelek : 1, 2, 3, 4 Függvényjeleink : s,p (növelés, csökkentés, 1-változós függvényjelek. Ennyi elég, összeadás, szorzás felesleges)

Predikátumjeleink :

=,<, wumpusz , kincs, csapda, aktpozicio  ezek 2-változós predikátumjelek,

el e a szorny , van e nyil  ezek 0-változós predikátumjelek, csak változóktól függetlenül igazak/hamisak lehetnek.

91

19. feladat: Formulák igazságértéke a wumpus-világ egy modelljében

Ezen ábra alapján leírható a wumpusz-nyelv egy Iwumpus modellje. Ebben igazak-e az alábbi formulák, a mellettük adott értékeléssel? a.



x y csapda(x, y) 1 2



b.

∀x¬csapda(x, x)()

∀x∃y¬csapda(x, y)()

92

20. Igazságértékek meghatározása II. A ma él® emberek interpretációjában, ha R 2-változós predikátumjel, és RI (e, f ) azt jelenti, hogy e szül®je f -nek, akkor igaz-e?

∀x∃yR(x, y) ∃xR(x, x) ∃x∃y(R(x, y) ∧ ¬R(y, x)) ∀x(R(x, x)→∃yR(y, x))

∀x∀yR(x, y) ∃x∃y(R(x, y) ∧ R(y, x)) ∀x∀y(R(x, y) ∧ ¬R(y, x)) ∀x(∃yR(y, x)→R(x, x))

∃x∀yR(x, y) ∃x∃y(R(x, y) ∨ R(y, x)) ∀x∀y(R(x, y)→¬R(y, x)) ∀x¬R(x, x)

93

21. Igazságértékek meghatározása III. Az egész számok körében, ha R 2-változós predikátumjel, és RI (n, m) azt jelenti, hogy n osztja m-et, akkor igaz-e?

∀x∃yR(x, y) ∃xR(x, x) ∃x∃y(R(x, y) ∧ ¬R(y, x)) ∀x(R(x, x)→∃yR(y, x))

∀x∀yR(x, y) ∃x∃y(R(x, y) ∧ R(y, x)) ∀x∀y(R(x, y) ∧ ¬R(y, x)) ∀x(∃yR(y, x)→R(x, x))

∃x∀yR(x, y) ∃x∃y(R(x, y) ∨ R(y, x)) ∀x∀y(R(x, y)→¬R(y, x)) ∀x¬R(x, x)

94

22. feladat Adjunk olyan paramétermentes formulát, amit az egyik modell igazzá tesz, a másik hamissá:

1.

(Z, +) és (N, +) 2. (Z, +) és (Z, ∗) 3. (Z∗) és (Q, ∗) 4. (Q, ∗) és (R, ∗)

95

A formula igazságértéke csak a paraméter-változók értékét®l függ 10. állítás: Ha két,I interpretáció feletti Ω és Φ igazságértékelés (mint függvény) felvett értéke megegyezik egy v.

K kifejezés (term

formula) összes paraméterén, akkor a formula két értékelés

utáni igazságértéke megegyezik, azaz kAkI,Ω = kAkI,Φ teljesül minden olyan

Ω és Φ változóértékelés esetén, ahol bármely v ∈ szv(A) esetén Ω(v) = Φ(v), ha K = A formula, és termekre hasonlóan.

Bizonyítás:

A formula szerkezete szerinti indukcióval.

96

Kvantorátjelölés egy formulában

Legyen Q valamelyik kvantor. Egy QxA formulának QyB formula egylépéses kvantorátjelölt variánsa, ha B az A-ból úgy kapható meg, hogy A-ban x összes szabad el®fordulását y-ra cserélem. Másféle egylépéses variánsa QxAnak nincsen. Egy (A B) formulának egylépéses variánsai pontosan a (Av B v ) alakú formulák, ahol Av az A-nak egy variánsa, míg B v meg B -nek egy variánsa (ahol lehet ∧, ∨, →, ↔). hasonló módon, ¬A egylépéses variánsai épp A egylépéses variánsainak negációi. A formulák halmazán a most deniált egylépéses variancia relációjának reexív, tranzitív lezártja ( a legsz¶kebb olyan b®vítése, ami reexív és tranzitív) az akárhány-lépéses variancia-reláció. Ha két formula ilyen relációban áll, úgy is mondjuk, egymás variánsai. (Könnyen belátható, hogy szimmetrikus, s®t, ekvivalenciarelációról van szó az adott nyelv formuláinak halmazán.)

11. állítás: : Ugyanazon interpretáció és változóértékelés mellett, variáns

formulák egyforma igazságértéket vesznek föl. Formálisan, ha A és B nyelvnek variáns formulái, I interpretációja L-nek és Ω változóértékelés felett, akkor kAkI,Ω = kBkI,Ω.

97

L I

Változótisztasági lemma 15. deníció: Egy formula változótiszta, ha bármely két kvantorja különböz® változókat köt, valamint nem fordul el® benne ugyanazon változó szabadon is és kötötten is.

12. állítás: (változótisztasági

lemma) Megadható olyan algorit-

mus, ami tetsz®leges input formulához egy olyan variánsát konstruálja, ami változótiszta.

98

Termhelyettesítés 16.

deníció: A termhelyettesítés az egy olyan Θ függvény,

aminek értelmezési tartománya változók egy véges részhalmaza, értékkészlete része a termek halmazának, és ha

x τ típusú változó, akkor Θ(x) pedig ugyanilyen típusú term. Ha K egy kifejezése L nyelvnek, x1 , . . . , xn változók és t1 , . . . , tn rendre azonos típusú termek, akkor

K

x1 . . . x n t1 . . . tn

!

KΘ-nal jelöljük azt a kifejezést, amit K -ban a változók szabad el®fordulásainak Θ alapján történ® szimultán átcserélésével kapunk. Ezt Θ K -ra való alkalmazása eredményének is nevezzük. Szerkezeti rekurziós deníciót lásd a PVK-VM könyv 5.1.27-es deníciójában.

99

Termhelyettesítés okozta változóütközés, megengedett helyettesítés 17. deníció: Egy Θ termhelyettesítés akkor okoz változóütközést

K kifejezés számára, ha K -ban van olyan Qv1A kvantor, amelynek A hatáskörében el®fordul wgy v2 változó szabadon, amelyre az áll, hogy Θ(v2 ) term szabad változói közül legalább egy szabadon el®fordul A-ban. Úgy is mondjuk, hogy Θ K számára nem megengedett.

13. állítás: Termek számára minden termhelyettesítés megengedett. Kvantormentes formula számára minden helyettesítés megengedett. Ha

Θ bármely változó helyére paramétermentes termet helyettesít,

szintén triviálisan megengedett.

100

Állítás a megengedett helyettesítések és a szemantikai érték kapcsolatáról

14. állítás: (Termhelyettesítés utáni értékr®l)

a) Ha

interpr., Ω változóértékelés, x ∈ dom(Θ), akkor I

t

term,

Θ

termhelyettesítés, amiben

I,Ω ) I,Ω I,Ω@(x→|Θ(x)| |tΘ| = |t| ,

b) Ha

interpr., Ω változóértékelés, A formula, Θ termhelyettesítés, amiben {x} = dom(Θ) és Θ megengedett A számára akkor I

I,Ω ) I,Ω I,Ω@(x→|Θ(x)| kAΘk = kAk .

101

Termhelyettesítés szabályos végrehajtása 18.

deníció:

A formula számára Θ helyettesítés nem megengedett, akkor a Θ szabályos végrehajtásának eredménye azt jelenti, hogy Θ végrehajtása el®tt A formulának keresünk egy olyan B variánsát, ami számára Θ már megengedett, és BΘ lesz a szabályos végrehajtás eredménye A-n. Jelben is megkülönböztetjük ezt a m¶veletet, A[Θ]-val jelöljük. Megjegyzés:

Ha

Igazából nem egyértelm¶ a m¶velet eredménye,

csak variancia erejéig.

102

23. feladat Változótiszták-e az alábbi formulák? Ha nem, tegye azzá ®ket!

a.

P (x, f (y))→∀y∃zQ(x, y, z) b. Q(x) ∨ ∃xQ(y)→P (y, x) c. ∃y∀zR(z, y)→∀z∃xR(z, x) d. ∃y(∀zR(z, y) ∧ ¬P (z))→∀z(∃xR(z, x) ∨ ¬Q(x, f (x), y))

103

24. feladat Megengedettek-e az alábbi helyettesítések? Hajtsuk ®ket végre szabályosan!

y a. ∀xP (x, y) f (z,x))



b.



(∀xP (x, y)→∃yP (y, g(x)))

x y f (x, y) g(x)

!

c.

(∀x(P (y, x) ∨ ∃z(R(z, f (y))→∃yR(g(w, y), x)))→∃wP (w, x)) ! x y w g(w, x) f (x) g(y)

d.

Az

x|z ∧ y|z ∧ ∀w(x|w ∧ y|w→z|w) formulát rövidítsük mint lkkt(x, y, z). Mit jelent ezek után lkkt(x + y, w ∗ 2, (x + w)2)?

104

25. feladat  természetes nyelvi álítások els®rend¶ formalizálása

Legyen egy olyan nyelv, amiben egyetlen típusú változók, függvényjelek, , konstansjelek, predikátumjelek. A nyelv modellje mindenki számára nyilvánvaló: az emberek halmaza lesz az objektumtartomány (ma él® vagy valaha élt). Adjunk olyan formulákat ezen a nyelven, amelyek ebben az interpretációban leírják az alábbi természetes nyelvi állításokat! Figyeljünk a megjelen® szabad változókra! A már deniált rövidítéseket lehet használni! öreg. nem öreg, ha van gyermeke. nem öreg de nincsen gyermeke. nem házas. nem n®s. fér. Minden ember öreg. Minden fér öreg. Minden öreg fér gazdag. Bármely fér gazdag, de nem óreg. Bármelyik fér, aki nem gazdag, az öreg. Bármelyik fér gazdag, ha nem öreg. Minden ember gazdag, ha nem öreg. 105 L

c ÉN gazdag(x), házastarsa(x,y)

x x x x x x

x, y, z, ... apa(x), anya(x) (x=y), ifjabb(x,y), szereti(x,y), tiszteli(x,y), n®(x), öreg(x),

Mindenki gazdag, aki senkit nem tisztel. Mindenkit tisztelek, aki gazdag. Van ember, akit és is tisztel. Nincs ember, aki öreg és nem gazdag egyszerre. Nincs ember, akit nem tisztelek. Minden öreget tisztelnek. Mindenki tisztel mindenkit. Mindenki tisztel valakit. Senki sem tisztel mindenkit. Senki sem tisztel senkit. Mindenki tiszteli valamelyik öreg embert. Valaki tisztel minden n®t. Semmilyen n® sem tisztel minden fért. testvére -nak. nagyszül®je -nak. -nek van nála atalabb testvére. -nek van -nél atalabb testvére. Mindenkinek van nála id®sebb testvére. Aki tiszteli a szüleit, az tiszteli más szüleit is. Mindenki ifjabb az apukájánál. Mindenki ifjabb bárkinek az apukájánál. Mindenki ifjabb valakinek az anyukájánál. Mindenki ifjabb valakinek valamelyik szülejénél. AAzn®ket tisztel®k szeretik az anyukájukat. -nél atalabbak kivételével senki sem tiszteli -et. x

x x x x

w

y

y

z

x

x

Azugyanazokat öcséim tisztelik a n®ket. az embereket szereti, akiket . Nincs két ember, aki ugyanazokat az embereket szeretné. Nincs két n®, aki ugyanazokat az embereket szeretné. Nincs két n®, aki ugyanazokat a férakat szeretné. csak akkor szereti -et, ha szereti ®t. csak azokat szereti, akik szeretik ®t. Az apám csak a nála atalabb n®ket szereti. Ifjabb vagyok bárkinél, aki tiszteli, de nem szereti a nála id®sebb férakat. Ha szereti azokat az embereket, akik szeretik ®t, akkor az ®t szeret® emberek nem szeretik azokat, akik nem szeretik -et!!! unokatestvére -nak. sógorn®je -nak. nagybátyja -nak. rokona -nak. (Erre nem sok id®t szabad szánni, max. 5 percet! ) x

y

y y

x

x

x

x

w v x

y

y

y

x

y

26. feladat  Jelkészlet meghatározása és formalizálás

Határozzunk meg egy alkalmas els®rend¶ nyelvet, amelyen formalizálhatók a következ® t.ny. mondatok! Mindenki okos. Minden ember okos. Minden okos jogász becsületes. AMinden csoportjogász minden tagja okos. okos. Nem a jogászok a legokosabbak. Az id®s jogászok nem a legokosabbak a jogászok között. Akik okosabbak a jogászoknál, azok csalók. Épp azok okosabbak a jogászoknál, akik csaló maózók. Mindenki okosabb néhány jogásznál. Minden bíró jogász. Vannak ügyesked® jogászok. Nincs ügyesked® bíró. Bizonyos bírók id®sek, de életer®sek. AA bíró sem nem id®s, sem nem életer®s. bírók kivételével minden jogász ügyesked®. Néhány olyan jogász, aki politikus, nem képvisel®. Minden id®s képvisel® jogász. Nincs olyan n®, aki jogász és képvisel®. Vannak olyan jogász n®k, akik nem politikusok, de háztartásbeliek. 106

Jen® tisztel minden n®t. Minden n® tiszteli Jen®t. Ha egy n® nem tiszteli Jen®t, akkor egyetlen fért sem tisztel. ABizonyos Jen®t tisztelo n®ket minden fér tiszteli. jogászok csak bírókat tisztelnek. Van olyan bíró, aki tisztel néhány n®t. Megszámlálhatóan végtelen halmaz minden részhalmaza véges vagy megszámlálhatóan végtelen.

27. feladat  Tagadás, els®rendben Tagadjuk a következ® formulákat úgy, hogy negáció hatáskörében csak atomi formula állhasson.

a.

∃x(A(x) ∨ B(x))

b.

∀x(A(x)→¬B(x))

c.

∀x(A(x)→∃yR(x, y))

d.

∃x(¬A(x)↔∃y¬B(y))

107

28. feladat  természetes nyelvi tagadás, els®rendben Tagadjuk a következ® kejelentéseket úgy, hogy a "nem minden" és a "nincs" logikai szavak, se szinonimáik ne szerepeljenek bennük. a. Minden szarka farka tarka. b. Mindenki tisztel valakit. c. Mindenki tisztel mindenkit. d. Minden jogász, aki n®, becsületes. e. Megszámlálható halmaz minden részhalmaza véges vagy megszámlálható.

108

Az alapvet® szemantikai fogalmak

19. deníció: Egy formulát kielégíthet®nek nevezünk, ha van olyan inter-

pretáció és értékelés, amely igazzá teszi. Egy formula logikai törvény, ha minden interpretáció és értékelés igazzá teszi. Ha A egy formula, |= A-val jelöljük azt, ha A logikai törvény. (|= - ez egy metanyelvi jel. A logikai törvény szinonimái: tautológia, azonosan igaz vagy logikailag érvényes formula.) egy formulát kielégíthetetlennek mondunk, ha nincs interpretáció és értékelés, ami igazzá tenné.

20. deníció: Két formula logikailag ekvivalens, ha bármely modell és értékelés egyszerre teszi ®ket igazzá ill. hamissá. Ha A és B formulák, azt a (metanyelvi) állítást, hogy A és B logikailag ekvivalensek, A ∼ B -vel jelöljük.

21. deníció: Egy

formulahalmaznak logikai következménye egy A formula, ha minden olyan interpretáció és értékelés, ami igazzá teszi Γ minden elemét, az A-t is igazzá teszi. Ennek jelölése: Γ |= A. (Szinonimái: Γ implikálja A-t, Γ maga után vonja A-t, stb.) Megjegyzés:

Γ

A jel metanyelvünkön polimorf, többes alakú. |=

109

Az alapvet® szemantikai fogalmak: példák Kielégíthet®, de nem logikai törvény:

P (x), P (x) ∧ ¬P (y), ∃x (P (x) ∧ Q(x)). Ellentmondásos:

P (x) ∧ ¬P (x), (P →Q) ∧ P ∧ ¬Q.

Logikai törvény:

|= P ∨ ¬P , P →P , |= ∀xP (x) → ∃xP (x).

Ekvivalencia:

A ∧ B ∼ B ∧ A, ¬(A ∧ B) ∼ ¬A ∨ ¬B , ¬∀xP (x) ∼ ∃x¬P (x). Következmény:

{A ∧ B} |= B , {A ∨ B, ¬A} |= B , {∀xR(x, x)} |= ∀x∃yR(x, y).

110

Alapvet® megállapítások az alapvet® szemantikai fogalmak közötti összefüggésekr®l Legyen

15.

A, B formula.

állítás:

A akkor és csak akkor kielégíthet®, ha A nem

ellentmondásos.

16. állítás: A akkor és csak akkor ellentmondásos, ha ¬A logikai törvény.

17.

állítás:

A akkor és csak akkor kielégíthet®, ha ¬A nem

logikai törvény.

Bizonyítások: mind triviális. Megjegyzés: Tehát elég egy formula logikai törvény mivoltát tudni eldönteni, és ezzel a kielégíthet®séget és az ellentmondásosságot is el tudnánk dönteni.

111

Az ekvivalencia, következmény és a törvények kapcsolata

18. állítás: Legyen

és B két formula. A ∼ B ⇔ |= A↔B , azaz A és B akkor és csakis akkor ekvivalensek logikailag, ha a ketejükb®l ekvivalenciajellel összerakott formula logikai törvény. A

19. állítás: Legyen Γ véges formulahalmaz, elemei G1, . . . , Gn, és A formula.

Ekkor Γ |= A ⇔ |= G1 ∧ . . . ∧ Gn→A. Azaz a {G1, . . . , Gn} |= A következmény akkor és csak akkor áll fenn, amikor a G1 ∧ . . . ∧ Gn→A formula logikai törvény.

20. állítás: Legyen A és B két formula.

Ekkor A ∼ B ⇔ {A} |= B és {B} |= A, azaz A és B akcsakkor ekvivalensek, ha A-nak A következménye.

B

következménye,és

B -nek

is

Bizonyítások: mind triviális. Megjegyzés: Tehát elég egy formula logikai törvény mivoltát tudni eldönteni, és ezzel az ekvivalenciát és a következményt (véges feltételhalmaz esetére) is el tudnánk dönteni.

112

Néhány logikai törvény I. - ítéletlogika

Jelölési különbség: -et helyettesítsük -pel. A kép részlet a [PVK-VM]-b®l. ⊃

→

113

Kis feladatok

22. deníció: Egy formulahalmaz kielégíthetet®, ha van olyan interpretáció és értékelés, ami minden elemét igazzá teszi. Kielégíthetetlen, ha nem kielégíthet®.

1. Bizonyítsa be, hogy kielégíthetetlen halmazban minden interpretáció és értékelés esetén van azokra hamis elem! 2. Bizonyítsa be, hogy kielégíthetetlen formulahalmaz bármely b®vítése kielégíthetetlen! 3. Igaz-e, hogy minden kiellégíthetetlen formulahalmaznak van kielégíthet® része? 4. Igaz-e, hogy minden kiellégíthetetlen formulahalmaznak van nemüres kielégíthet® része? 5. Igaz-e, hogy minden kielégíthet® formulahalmaznak van kielégíthetetlen b®vítése? 6. Igaz-e, hogy bármely kielégíthet® formulahalmaznak van kielégíthet® b®vítése? 7. Igaz-e, hogy bármely kielégíthetetlen formulahalmaz bármely nemüres része kielégíthetetlen?

114

Kis feladatok Γ

és 1. 2. 3. 4. 5. 6. 7. 8.

∆

formulahalmazt jelöl,

G1 ,

...,

Gn , A

és

B

formulák.

Az üres formulahalmaz kielégíthet® vagy sem? Igazolja, hogy Γ |= A akcsakkor, ha Γ ∪ {¬A} kielégíthetetlen. Igazoljuk, hogy kielégíthetetlen formulahalmaznak bármilyen formula következmény Bizonyítsuk be, hogy egy érvényes formula bármilyen formulahalmaznak következménye. Igazolja, hogy {G1, . . . , Gn} |= A ⇔ {G1 ∧ . . . Gn} |= A. Igazolja, hogy {G} |= A ⇔ |= G→A. Igazolja, hogy Γ ∪ {A} |= B ⇔ Γ |= A→B (szemantikus dedukciótétel) Igazoljuk a szemantikus vágás-tételt: Ha Γ ∪ {A} |= B és ∆ |= A, akkor Γ ∪ ∆ |= B .

115

Kis bizonyítanivalók

1. 2. 3. 4. 5. 6. 7.

ekvivalenciareláció. Ha A és B variánsai egymásnak, akkor A ∼ B . Ha A ∼ A0 és B ∼ B 0, akkor A ∧ B ∼ A0 ∧ B 0. Ha A ∼ A0 és B ∼ B 0, akkor A ◦ B ∼ A0 ◦ B 0, ahol ◦ ∈ {∧, ∨, →, ↔}. Ha A ∼ A0, akkor ¬A ∼ ¬A0. Ha A ∼ A0, akkor QxA ∼ QxA0, ahol Q ∈ {∀, ∃}. Ha egy A formulában egy részformuláját egy, a részformulával vele ekvivalens formulára cserélünk szabályos helyettesítéssel, akkor A-val ekvivalens formulát kapunk. Biz: szerkezeti indukcióval ∼

116

Itéletlogikailag érvényes formula 23.

deníció:

Egy els®rend¶ B formulának az A1 , . . . , Ak a prímkomponensei, ha k ≥ 1, A1 , . . . , Ak mindegyike vagy atomi formula vagy kvantort f® logikai jelként tartalmazó formula, és B ezekb®l a formulákból csak az ítéletlogikai jelek (∧, ∨, →, ↔, ¬) segítségével épül föl.

24. deníció: Egy els®rend¶ B formulát ítéletlogikailag érvényes formulának mondunk, ha az a formula, amelyet prímkomponenseinek különböz® nullaváltozós predikátumjelekre való cseréjével kapunk, logikai törvény. Ezt a tulajdonságot |=0 -val jelezzük: az ítéletlogikát nulladrend¶ logikának is nevezzük. Ilyenkor persze B logikai törvény is. Viszont nem minden érvényes formula érvényes ítéletlogikailag is. Pl. ∀x(P (x)→P (x)) is ilyen.

117

Megjegyzés:

Ilyenkor

B érvényes volta csupán az ítéletlogikai

jelek tulajdonságain múlik.

Hasonlóan deniálhatjuk az ítélet-

logikai következményt és ekvivalenciát.

21. állítás: Eldönthet®, hogy egy adott formula ítéletlogikailag érvényes-e.

Eldönthet®, hogy adott ítéletlogikai következmény

ill. ekvivalencia fenáll-e.

Bizonyítás:

a gyakorlaton tanult igazságtáblás módszer m¶ködik.

118

Példa ítéletlogikailag érvényes formulára

A

⊃ jelentése: →. Részlet [PVK-VM]-b®l. Ebben a könyben

tautologikusan igaz

formulának hívják ezen formulákat.

119

Ítéletlogikai ekvivalenciák

120

Ítéletlogikai kiszámítási törvények

121

Ítéletlogikai ekvivalenciák III.

122

Ítéletlogikai ekvivalenciák IV.

123

Helyes ítéletlogikai következtetések

124

Kvantoros logikai törvények I.

125

Kvantoros logikai törvények II.

Par(A) := szv(A)

126

Kvantoros logikai törvények III.

127

29. feladat: kielégíthet®ség Kielégíthet®ek a következ® halmazok? Válaszunkat indokoljuk!

1. 2. 3. 4. 5. 6. 7. 8. 9.

{P (x), ¬P (y)} {P (x), ¬P (x)} {∀xP (x), ∃x¬P (x)} {∀xP (x), ∃y¬P (y)} {∀xP (x), ¬P (y)} {∃xP (x), ¬P (y)} {P (x1), P (x2), P (x3), . . .} ∪ {∃x1¬P (x1)} {x > 0, x > s0, x > ss0, x > sss0, . . .} {R(x, c), R(x, f (c)), R(x, f (f (c))), . . .} E két utóbbi mindkett® egyformán kielégíthet®  az egyes formulák megfelelnek egymásnak, csak más predikátumjeleket használnak!

128

30. feladat: kielégíthet®ség Kielégíthet®ek a következ® halmazok? Válaszunkat indokoljuk! 3.

{∀xP (x), ∃x¬P (x)}

Ez nem kielégíthet®, mert az els® formula azt mondja, hogy az alaphalmaz minden eleme teljesíti P I -t, míg a második azt, hogy van olyan, ami nem.

129

31. feladat: kielégíthet®ség Kielégíthet®ek a következ® halmazok? Válaszunkat indokoljuk!

{∃xP (x), ¬P (y)} Ez kielégíthet®, mert a következ® interpretáció és értékelés igazzá teszi mindkét elemét: az alaphalmaz legyen {1, 2}, és P I a következ® táblázattal adott: n P I (n) 1 i 2 h

130

32. feladat: kielégíthet®ség Mutassuk meg, hogy a következ® formulák kielégíthet®k:

∀xP (f (x)) ∧ ¬∀xP (x)

∀x∃yR(x, y) ∧ ¬∀y∃xR(x, y)

∃y∀xR(x, y)

∀x(P (x) ∨ Q(x)) ∧ ¬∀xP (x) ∧ ∀xQ(x)

∀x¬R(x, x) ∧ ∀xyz(R(x, y) ∧ R(y, z)→R(x, z)) ∧ ∀x∃yR(x, y) ∀x(P (x) ∨ Q(x)) ∧ ∀x(P (x) ∧ Q(x)→T (x)) ∧ ∀x¬xT (x)

131

33. feladat Érvényes formulák Érvényesek-e (azaz logikai törvények-e) az alábbi formulák? Ha igen, ítéletlogikailag érvényesek? Ha nem érvényesek, mutassuk meg, hogy a tagadásuk kielégíthet®!

∀x(P (x)→Q(x)) ∧ ∀xP (x)→∀xQ(x) ∀x(P (x)→Q(x)) ∧ ∃xP (x)→∀xQ(x) ∀x(P (x)→Q(x)) ∧ ∃xP (x)→∃xQ(x) ∃x(P (x) ∧ Q(x))→∀x(P (x)→Q(x))

132

34. feladat Helyes következtetési formák

Jelölés: Az egyszer¶bb írásmód kedvéért A1 , . . . , Ak |= B -t írunk.

{A1 , . . . , Ak } |= B

helyett csak

Helyesek az alábbi következtetések? Ha igen, ítéletlogikailag érvényesek? Ha nem érvényesek, mutassuk meg, hogy a feltételek ∪ következmény tagadása halmaz kielégíthet®. ∀x(P (x)→Q(x)), ∀xP (x) |= ∀xQ(x) ∀x(P (x)→¬Q(x)), ∃xP (x) |= ∃xQ(x) ∀xP (x) ∨ Q(x)), ∀xP (x) |= ∀xP (x) ∀x(P (x)→¬Q(x)), ∃xQ(x) |= ∃x¬P (x) ∀x(P (x)→Q(x)), ∃x(Q(x) ∧ T (x)) |= ∃x(P (x) ∧ T (x))

133

Ekvivalens formulák Ekvivalensek-e logikailag, s ha igen, ítéletlogikailag is ekvivalensek? Ha nem, adjunk interpretációt és értékelést, ahol az egyik igaz, a másik hamis.

∀xP (x) és ∃xP (x) ∀xP (x) és ∀yP (y) ∀xP (x) és ¬∃¬yP (y) ∀xP (x)↔P (x) ∀x(P (x)↔P (x)) ∀xP (x)↔∀xP (x)

134

Ítéletlogikai törvények alkalmazásai: diszjunktív és konjunktív normálforma 25. deníció: Literál: atomi formula vagy tagadott atomi formula.

P vagy ¬P alakú, ahol P atomi formula.

26. deníció: elemi konjunkció literálok konjunkciója, lehet 1elem¶ is.

L1 ∧ . . . ∧ Ln alakú, ahol Li-k mindegyike literál, és

n ≥ 1. 27.

deníció: diszjunktív normálforma elemi konjunkciók dis-

zjunkciója, lehet 1-elem¶ is.

K1 ∧ . . . ∧ Km alakú, ahol Ki-k mindegyike elemi konjunkció, és m ≥ 1.

135

A diszjunktív normálforma jellemz®je 22. állítás: Egy formula akcsakkor van diszjunktív normálformában, ha a következ®k mindegyikét teljesíti: 1. kvantormentes, 2. nincs benne se

↔, se → logikai összeköt®, 3. nincs ¬(X ∧ Y ), ¬(X ∨ Y ), ¬¬X alakú részformulája 4. nincs X ∧ (Y ∨ Z) és (Y ∨ Z) ∧ X alakú részformulája 23.

állítás:

Minden kvantormentes formulához algoritmikusan konstruálható vele ítéletlogikailag ekvivalens diszjunktív normálformájú formula. Biz: Az el®z® állításból és a következ® oldalon bemutatott ekvivalenciák véges számú alkalmazásával következik, ha gyelembe vesszük azt, hogy részformulát ekvivalens részformulár acserélve ekvivalens formulát kapunk.

136

A d.n.f-hez szükséges ekvivalenciák

137

A konjunktív normálforma 28.

deníció:

A konjunktív normálforma analóg módon, el-

emi diszjunkciók konjunkciójaként értelmezend®. Hasonló állítás mondható ki rá:

adható algoritmus, ami tetsz®leges kvantor-

mentes formulához konstruál egy azzal ekvivalens, de már konjunktív normálformájú formulát.

138

35. feladat: Diszjunktív normálformák alkalmazása az áramkörök leírásában Adjunk olyan áramkört, ami egy forrásból, kapcsolókból (P,Q,R) és egy fogyasztóból(lámpa) áll, és akkor és csakis akkor világít, ha P, Q, R közül kett® van bekapcsolva. Adjunk olyan áramkört, ami egy forrásból, kapcsolókból (P,Q) és egy fogyasztóból(lámpa) áll, és bármelyik kapcsolóján mozdítok, a világítás értéke is változni fog. Ezen feladatok megoldhatók a diszjunktív normálforma alapján. Ezt az igazságtábla alapján is megszerkeszthetjük.

139

Prenex normálforma 29.

deníció: prenex normálforma: Els®rend¶ formulák egy-

fajta alakja, ahol minden kvantor megel®z a szerkezeti fában minden ítéletlogikai jelet (azaz Boole-jelet:

∧, ∨, ¬, →, ↔).

24. állítás: Minden els®rend¶ formulához konstruálható olyan, vele ekvivalens formula, ami már prenex alakú.

Biz :

Az algoritmus lefutása a formula változótiszta alakra hozása

után a kvantorok egyoldalú kiemelése szabályok véges számú alkalmazását jelenti.

140

36. feladat: Hozzuk prenex alakra a következ® formulákat!

∀x¬∀¬yR(y, x)→∃y∀xR(x, y) ∃z(∀x¬∃yT (y, x, z)→∃z∀x(R(x, y) ∨ ¬∃yR(y, x)))

141

BIZONYÍTÁSELMÉLET

142

Tabló-módszer

30. deníció: Min®sített formulának nevezzük a tA és f A jelsorozatokat, ahol A formula,

tA

azt fejezi ki, hogy

A igaz,

t és f pedig jelek, min®sít® jelek. f A pedig azt, hogy A hamis.

143

Tabló-kalkulus

31.

deníció:

Kalkulusnak nevezünk bármely, formulák (ál-

talánosabban, jelsorozatok) átalakítására szolgáló bármely szabályrendszert. A formális nyelvek tárgyból megismert

szer

egy formája.

32.

deníció:

formális rend-

T véges fagráfot tablónak nevezzük egy G

min®sített formulákból álló halmaz számára, ha

1. Minden csúcsában min®sített formulák véges, nemüres halmaza áll 2. Gyökerében éppen a G elemeib®l álló halmaz található 3. Bármely elágazás a következ®kben megadott szabályok egyike szerint alakul:

144

A tabló-kalkulus szabályai

145

Zárt tabló

33. deníció: Zártnak nevezzük a tablót, ha minden ágán van olyan formula, hogy

tA

és

fA

is eleme az ág csúcsaihoz rendelt

formulahalmazok uniójának.

34. deníció: A G min®sített formulahalmaz cáfolható, ha van olyan T tabló G számára, aminek minden eleme zárt.

35. deníció: Γ formulahalmaz cáfolható, ha a G = {tA|A ∈ Γ} min®sítettformula-halmaz cáfolható.

25. állítás:

(A tablókalkulus helyességi tétele)

halmaz cáfolható, akkor nem kielégíthet®.

Ha

Γ formula-

146

36. deníció: Legyen G min®sített formulák egy halmaza. G-t kielégíthet®nek nevezzük, ha vna olyan interpretáció és értékelés, amiben G

t-vel

jelzett formulái igazak, míg a

f -val

min®sítettek

hamisak.

Azt, hogy G teljesül egy interpretációban, bizonyos

értékelés mellett, hasonló elv alapján deniáljuk.

26.

állítás:

(Segédtétel) Ha egy tablóban egy ág(on lév®

min®sített formulák uniója) kielégíthet® és valamely szabály alapján kiterjesztjük az ágat, akkor a kiterjesztett ágak legalább egyikének is kielégíthet®nek kell maradnia.

147

A segédtétel esetei (néhány):

1. Ha

Γ kielégíthet® és tartalmaz egy t(A ∨ B) alakú formulát, akkor Γ ∪ {tA} kielégíthet® vagy Γ ∪ {tB} kielégíthet®. 2. Ha Γ kielégíthet® és tartalmaz egy f (A ∨ B) alakú formulát, akkor Γ ∪ {f A, f B} kielégíthet®. 3. Ha Γ kielégíthet® és tartalmaz egy f ¬A alakú formulát, akkor Γ ∪ {tA} kielégíthet®. 4. Ha Γ kielégíthet® és tartalmaz egy f (A→B) alakú formulát, akkor Γ ∪ {tA, f B} kielégíthet®.

148

A segédtétel esetei (kvantorok):

1. Ha

Γ kielégíthet® és tartalmaz egy t ∀xA alakú formulát, akkor Γ ∪ {tA(x||s)} kielégíthet®, bármilyen s term esetén, ahol || a szabályos helyettesítés jele. 2. Ha Γ kielégíthet® és tartalmaz egy f ∃xA alakú formulát, akkor Γ ∪ {f A(x||s)} kielégíthet®, bármilyen s term esetén, ahol || a szabályos helyettesítés jele.

149

A segédtétel esetei (kvantorok 2.)

1. Ha

Γ kielégíthet® és tartalmaz egy f ∀xA alakú formulát, akkor Γ ∪ {f A(x||y)} kielégíthet®, bármilyen y változó esetén,

amelyik nem szerepel szabadon az ág egyetlen formulájában sem. 2. Ha

Γ kielégíthet® és tartalmaz egy t ∃xA alakú formulát, akkor Γ ∪ {tA(x||y)} kielégíthet®, bármilyen y változó esetén, amelyik nem szerepel szabadon az ág egyetlen formulájában sem.

150

A helyességi tétel következményei: a tabló-kalkulus alkalmazásai

27. állítás: Ha{f A} cáfolható, akkor A logikai törvény. 28.

állítás: Ha {f (A↔B)} cáfolható, akkor A és B ekvi-

valensek.

29. állítás: Ha {tA1, . . . , tAn, f B} cáfolható, akkor az

{A1, . . . , An} |= B következmény fennáll.

151

Gödel teljességi tétele a tabló-kalkulusra 30. állítás: Bármely logikai törvény cáfolható tabló-kalkulussal, aza ha

A logikai törvény, akkor {f A} cáfolható.

A bizonyítást nem vesszük, bonyolultsága miatt. Egy bizonyítás megtalálható tabló-kalkulus esetére Bell és Machover A course in mathematical logic c. 1977-es könyvében. Hasonló tételt Kurt Gödel bizonyított be el®ször, az 1930-as évek elején, de más kalkulusra. 31. állítás:

(A Gödel-féle teljességi tétel más, ekvivalens alakjai)

(i) Ha egy

A1, . . . , An |= B következmény fennáll, akkor {tA1, . . . , tAn, f B} cáfolható (ii) 32. állítás: Ha A és B ekvivalensek, akkor {f (A↔B)} cáfolható.

152

Feladatok tabló-kalkulusra Bizonyítsuk be, hogy az el®adás korábbi részében felsorolt logikai törvények, ekvivalenciák és következmények fennállnak.

153

Kiemelt feladatok

(A01) (A02) (A03) (A04) (A05) (A06) (A07) (A08) (A09) (A10) (A11) (A12) (A13) (A14)

A→(B→A) ((A→(B→C))→((A→B)→(A→C)) (A→B)→((A→¬B)→¬A) ¬¬A→A A→(B→A ∧ B) A ∧ B→A A ∧ B→B (A→C)→((B→C)→(A ∨ B→C)) A→A ∨ B B→A ∨ B ∀xA→A(x||s), ahol s tetsz®leges term ∀x(C→A(x))→(C→∀xA(x)), ahol x nem A(x||s)→∃xA, ahol s tetsz®leges term ∀x(A(x)→C)→(∃xA(x)→C), ahol x nem

szabad C -ben szabad C -ben

33. állítás: Az ilyen alakú formulák mindegyike logikai törvény.

154

Az axiomatikus levezetési kalkulus Miért vizsgálunk más levezetési kalkulust is?

Mert a tabló-módszer cáfoló módszer, és sokszor bizonyítani szeretnénk, nem cáfolni A bizonyítás közelebb áll a mindennapos gondolatmenetünkhöz Jó, ha sokféle formalizmust ismerünk Az elméleti kutatások könnyebbek technikailag Történetileg ez az els® Ezt fejlesztjük tovább programhelyesség-bizonyítási rendszerré

Kifejleszt®k: Frege (1800-as évek vége), Hilbert (német, 1900-as évek eleje). Úgy is hívjuk ezt a kalkulust, hogy Hilbert-stílusú rendszer. 155

Az axiomatikus levezetési kalkulus jellemz®i

 sok axióma, kevés szabály ( a tabló-kalkulus tele volt szabályokkal, axióma csak egy volt benne: tA és f A egy ágon együtt lehetetlen).  bizonyítási rendszer, nem cáfoló.

156

A logikai axiómák 37. deníció: A logikai axiómák az (A1)  (A14) sémák valamelyikére illeszked® formulák. Megjegyezhetjük, hogy végtelen sok konkrét axióma van, bár véges sok axiómaséma.

Például, ha R 2-változós predikátumjel és f 1-változós függvényjel, akkor ∀xR(y, f (x)) ∧ ∃yR(y, x)→∀xR(y, f (x)) (A06) és ∀xR(y, f (x))→R(y, f (f (y))) (A11) is axiómák.

157

Gyakorlat Az adott formula logikai axióma-e?

1.

∀x(P (x) ∧ P (y)→P (y)) 2. ∀xP (x) ∧ ∀yP (y)→∀yP (y) 3. ∀xP (x) ∨ ∀yP (y)→∀yP (y)

158

Eldönthet® problémák 38. deníció: Bármely formális nyelv esetén egy eldöntési problémának

nevezzük annak eldöntését, hogy adott input szó eleme-e a nyelvnek. Adott probléma algoritmikusan eldönthet®, ha tudunk adni algoritmust, ami megoldja.

(Az algoritmus fogalmát jelen kurzusban nem deniáljuk. A programozás 1.ben deniált C-programok fogalma jó közelítését jelenti. Majd a számításelmélet nev¶ tárgyban fogjuk deniálni.)

159

Egy eldönthet® probléma 34. állítás: Eldönthet®, hogy adott input formula axióma-e.

A bizonyításhoz megjegyezzük, hogy a formula axióma-voltának megállapításához elég a szerkezeti fa néhány fels® élét megvizsgálni, akármilyen hosszú formula esetén, ennek felépítésére pedig vettünk algoritmust a gyakorlaton ( a szerkezeti elemzés egyértelm¶ségének megállapításakor).

160

Axiomatikus levezetési fa 39. deníció:

formula Γ formulahalmazból való levezetési fájának ( röviden, levezetésének) nevezünk egy olyan véges fát, amelyre teljesül: 1. 2. 3. 4. A

B

Minden csúcsban egy formula áll A gyökérben B áll A levelekben a logikai axiómákon kívül csak Γ elemei állhatnak Az elágazások a következ® két levezetési szabály szerint alakulhatnak: A→B

A (gen) B ∀xA ahol x nem szabad a (gen) alkalmazása feletti levelekben lév® nem logikai axiómák egyikében sem. (mp)

mp = modus ponens, leválasztás, gen = generalizálás, általánosítás, nem-logikai axiómák: elemei. Az axiomatikus levezetési fában alul áll az, ami következik, felül az, amib®l következik. Azaz felül a levelek, alul a gyökér. 161 Γ

Axiomatikus levezethet®ség 40. deníció: Azt mondjuk, hogy Γ formulahalmazból (az axiomatikus kalkulusban) levezethet®

B formula, ha van B -nek Γ-ból

való levezetési fája. Jelölése:

Γ ` B.

Példa: A tetsz®leges formula.

(A01) A→(A→A)

(A01) A→((A→A)→A)

(A02) (A→((A→A)→A))→((A→(A→A))→(A→A)) (A→(A→A))→(A→A) A→A

Ebben a levezetésben 2-szer használtuk a modus ponenst. A levelekben csak logikai axiómák vannak, így igazoltuk, hogy ∅ ` A→A. Jelölés: ` A : ⇔ ∅ ` A.

162

Az axiomatikus levezetési kalkulusr®l A levezetései nem mindig a természetes gondolkodásunk szerint formálódnak. Például az

A→A formula inkább axiómának volna

gondolható. Ezen hibáit nemsokára orvosoljuk. Szokásos elnevezése még: els®rend¶ predikátumkalkulus, függvénykalkulus. A levezetési fa magassága a formulafa magasságát jelenti.

163

Az axiomatikus levezetési kalkulus helyessége 35.

állítás:

Legyen

Γ formulahalmaz, B formula. Ha Γ ` A, akkor Γ |= A, azaz, ha Γ-ból levezethet® B , akkor tényleg következik is bel®le. A bizonyítás a

Γ ` A-t megalapozó levezetési fa magassága sz-

erinti teljes indukcióval.

Az axiómák következnek az üres hal-

mazb®l, mert logikai törvények ( tablö-kalkulussal már igazoltuk),

Γ elemei is következnek Γ-ból, így a 0 hosszúságú levezetési fákkal végeztünk.

164

Az axiomatikus levezetési kalkulus helyessége II. Ha

Γ ` B adott levezetésében B -t modus ponens-szel kaptuk egy A és egy A→B formulából, akkor ezen formuláknak van legalább 1-gyel rövidebb bizonyítása. Használjuk az indukciós hipotézist, tehát tudjuk, hogy

Γ |= A és Γ |= A→B . De ekkor Γ |= B is

teljesül, könnyen belátható. A másik eset, ha Ekkor

B = ∀xA és B -t a (gen) szabállyal kaptuk A-ból.

x nem szerepel a fa szabályalkalmazás feletti részének lev-

eleiben lév® nem-logikai axiómákban szabad változóként. Jelöljük el

Γ ezen formuláinak halmazát Γ0-val. Ekkor nemcsak Γ ` A-t tudjuk, hanem Γ0 ` A-t is. Az indukciós hipotézis miatt Γ0 |= A. Mivel Γ0 -ban nem is szerepel x szabadon, így Γ0 |= ∀xB , és végül Γ |= ∀xB is adódik.

165

Dedukciótétel az axiomatikus levezetési kalkulushoz 36. állítás: (Dedfukciótétel). Γ ∪ {A} ` B akkor és csak akkor teljesül, ha

Γ ` A→B , ahol Γ formulahalmaz, A és B pedig for-

mulák. A bizonyítás hosszú, de nem nehéz.

⇐ irány: Γ ` A→B ⇒ Γ ∪ {A} ` B , mivel a feltételek csak b®vültek. Γ ∪ {A} ` A is teljesül, mert A eleme a baloldalnak is. (mp) alkalmazásával kész.

⇒ irány  ez a nehezebb.

166

Dedukciótétel bizonyítása ⇒

⇒ irány: nem vesszük.

167

A természetes levezetés formalizmusa A dedukciótétel segítségével sok segédtételt bebizonyíthatunk, amiket kés®bb a levezetések során alkalmazhatunk. Ebben a formalizmusban nem csak a levezetés folyamán keletkez® újabb és újabb formulákat írjuk be a levezetési fába, hanem mindig, újra és újra leírjuk, aktuálisan milyen feltételeink vannak - ez azért jó, mert a mindennapos levezetéseinkben is élünk id®leges feltételezésekkel. pl. "tegyük fel, hogy van egy megoldásunk. Ekkor el® tudunk állítani egy olyan megoldást is, ami..." Ezek adminisztrálására is jó ez a formalizmus. A hibája, hogy a feltételeket sokszor kell ismételnünk.

168

A természetes levezetési technika fogalmai

41. deníció: Természetes levezetési fa: véges fa, a csúcsokban ún.

szekventekkel. A szekvent egy jelsorozat típusú objektum, a ` jelet midenképp tartalmazza, és ennek jobboldalán egy formulát, míg a baloldalán véges számú formulát, vessz®kkel elválasztva. A bebizonyított/bebizonyítandó következmények leírására szolgál. Formálisan: A1, . . . , An ` B alakú jelsorozat, ahol n ≥ 0 és A1 , . . . , An , B mindegyike formula. A levelekben axiómaszekventek állhatnak, amelyek olyanok, hogy 1. a jobboldali formula szerepel baloldalon, vagy 2. ` A alakú, ahol A, mint formula, logikai axióma (A01A14). A levezetési fát a gyökerében álló szekvent levezetésének hívjuk. Az elágazások a következ® szabályok mentén lehetségesek:

169

A természetes levezetés szabályai I. - ítéletlogikai szabályok Γ`A Γ`B (∧-bev) Γ`A∧B Γ`A Γ`B (∨-bev1 ) (∨-bev2 ) Γ`A∨B Γ`A∨B Γ, A ` B (→-bev) Γ ` A→B

Γ, A, B ` C (∧-elim) Γ, A ∧ B ` C Γ, A ` C Γ, B ` C (∨-elim) Γ, A ∨ B ` C Γ`A

Γ ` A→B (→-elim) Γ`B

Γ, B ` A Γ, B ` ¬A (¬-bev) Γ ` ¬A

Γ ` ¬¬A (¬-elim) Γ`A

Γ, B ` A Γ, A ` B (↔-bev) Γ ` A↔B

Γ ` A Γ ` A↔B (↔-elim)1 Γ`B Γ ` B Γ ` A↔B (↔-elim)2 Γ`A

170

A természetes levezetés szabályai II. - kvantoros szabályok Γ`A (∀-bev) Γ ` ∀xA

ahol x nem szabad Γ-ban Γ ` A(x||s) (∃-bev) Γ ` ∃xA

ahol

s

tetsz®leges term

Γ ` ∀xA (∀-elim) A(x||s

ahol

s

tetsz®leges term

Γ, A(y) ` B (∃-elim) Γ, ∃yA(y) ` B

ahol x nem szabad Γ-ban

171

A természetes levezetés szabályai III. - strukturális szabályok Γ, A, B, ∆ ` C (permutálás) Γ, B, A, ∆ ` C Γ, B, B, ∆ ` A (redukció) Γ, B, ∆ ` A

Γ`A (b®vítés) Γ, B ` A Γ`A ∆, A ` B (vágás) Γ, ∆ ` B

Ezen strukturális szabályok biztosítják például, hogy a formálisan lista(sorozat) adatszerkezet, amivel a feltételeket ábrázolhatjuk, lényegében, csak mint halmaz számít. A sorrend és a multiplicitás nem számít. Így ezeket a levezetések írása folyamán nem is említjük, a vágásszabály kivételével.

172

További megengedett szabályok (lásd Vályi-Mecsei'2005) Kényelmesebb

→-elim:

Kontrapozíciók:

Γ, ¬A ` C Γ, B ` C (→-elim2) Γ, A→B ` C

Γ, ¬A ` ¬B Γ, ¬A ` B (cp1 ) (cp2 ) Γ, B ` ¬A Γ, B ` A

Γ, A ` ¬B Γ, B ` A Még kontrapozíciók: (cp3 ) (cp4 ) Γ, B ` ¬A Γ, ¬A ` ¬B ¬¬-bevezetés:

Γ`A (¬¬-bev) Γ ` ¬¬A

Megfordítható

∨-bevezetések:

Γ, ¬A ` B (∨-bev-új1) Γ`A∨B

Γ, ¬B ` A (∨-bev-új2) Γ`A∨B

173

További megengedett szabályok II. (lásd Vályi-Mecsei'2005)

Γ, A ` B Γ, B ` C Lánc-érvelés: (lánc) Γ, A ` C Γ, B ∨ ¬B ` A (vágás-IH) Γ`A Amikor kvantoros logikai következményeket igazolunk, az összes propozicionális logikai törvényt axiómaként használhatjuk: ahol

` A,

A igazságtáblával igazoltan logikai törvény.

174

A természetes levezetési technika helyességi és teljességi tétele 37. állítás:

(helyesség)

Ha a

Γ ` A szekvent természetes lev-

ezetéssel levezethet®, akkor predikátumkalkulusban is levezethet®, és így

38. állítás:

Γ |= A is.

(teljesség)

Ha

Γ ` A levezethet® predikátumkalku-

lusban, akkor ez a szekvent természetes levezetéssel is levezethet®. Bizonyítás: könny¶.

39. állítás: (A három tanult bizonyítási formalizmus ekvivalenciája)

Γ ` A akkor és csak akkor bizonyítható a predikátumkalkulusban, ha Γ ∪ {¬A} cáfolható tablóval.

175

Kompaktsági tétel 40. állítás: (a predikátumkalkulus teljességének következménye)

1. Ha

Γ |= A, akkor van olyan véges Γ0 része Γ-nak, amire szintén Γ0 |= A. 2. Ha Γ nem kielégíthet®, akkor van olyan véges része, ami szintén nem kielégíthet®.

176

Feladatok Adjunk természetes levezetést az el®adás korábbi részében említett törvényekre, ekvivalenciákra és következményekre. A gyakorlatokon kidolgozott példákon kívül más kidolgozott példákat találnak pl. dr. Mihálydeák Tamás honlapján vagy az irodalomjegyzékben megadott Dragálin-Buzási könyvben. http://www.inf.unideb.hu/ mihalydeak/Inf Log 07 08 2.pdf

177

Formális axiomatikus elméletek 42. deníció: Els®rend¶ formális axiomatikus elméletnek nevezzük az olyan pedig

T = (L, Ax) párokat, ahol L egy els®rend¶ nyelv, Ax

L zárt (paramétermentes) formuláinak egy részhalmaza.

Ax-t az elmélet nemlogikai axiómáinak nevezzük.

Megjegyezzük, hogy lehet akár üres is, akár az összes formulák halmaza, és közöttük bármilyen részhalmaz. Ax

43.

deníció:

Azt mondjuk, hogy

elmélet tétele, ha

A formula a T = (L, Ax)

Ax-ból A levezethet®.

178

Eldönthet® elmélet Egy elméletet eldönthet® elméletnek hívunk, ha a tételeinek halmaza algoritmikusan eldönthet®.

41.

állítás:

(A predikátumkalkulus eldönthetetlensége, Church-tétel)

Ha az

L nyelvben van 2-argumentumú reláció vagy függvényjel, akkor az üres elmélet (L, ∅) eldönthetetlen. Más szóval, a logikai törvények halmaza az ilyen nyelven nem eldönthet®. (Miért?)

42. állítás: Ha a nyelvben csak 1-argumentumú predikátumjelek vannak, akkor az adott nyelven vett üres elmélet ( az adott nyelv logikai törvényeinek halmaza) eldönthet®.

179

Példák elméletekre  Peano-aritmetika 44. deníció: Ar nyelven a következ® alakú formulák halmaza a Peano-aritmetika:

1. 2. 3. 4. 5. 6. 7. 8. 9.

∀x x = x ∀xyz(x = y ∧ x = z→y = z) ¬S(x) = 0 ∀xy(S(x) = S(y)→x = y) A(x||0) ∧ ∀x(A(x)→A(x||S(x))→∀xA(x) ∀x x + 0 = 0 ∀xy(x + S(y) = S(x + y)) ∀x x ∗ 0 = 0 ∀xy(x ∗ S(y) = x ∗ y + x)

180

A Peano-aritmetika tételei

1.

∀xy (x = y→y = x) 2. ∀xyz(x = y ∧ y = z→x = z) 3. ∀xy(x = y→z + x = z + y) ... Fermat-tétel.

Jelöljük a Peano-aritmetikáb®l levezethet® zárt formulák halmazát

P A-val.

181

A Peano-aritmetika modelljei 1. A természetes számok halmaza, a szokott m¶veleteivel 2. A kompaktsági tétel értelmében a

P A ∪ {c > 0, c > S(0), c > S(S(0)), . . .} halmaznak van modellje, egy olyan nyelven, ami az aritmetika nyelvét kib®víti a

c konstanssal. ez egy nemstandard modellje a

PA-nak.

182

Gödel nemteljességi tétele 43. állítás: (intuitív, nem-formális megfogalmazásban) Ha egy els®rend¶ elmélet tartalmazza a PA-t, és algoritmikusan felsorolható az axiómáinak halmaza, akkor van olyan formula az elmélet nyelvén, ami se le nem vezethet®, se nem cáfolható ebben az elméletben.

183

Egy eldönthet® elmélet 44. állítás: (Tarski tétele) Ar nyelv R modelljében igaz formulák halmaza eldönthet®. (Van algoritmus, ami elvben minden zárt formulára megválaszolja, hogy igaz-e ebben a modellben, vagy hamis. Megjegyezzük, hogy Tarski tételének következményeként a szokásos geometriai elméletek, mind analitikus, mind szintetikus formájukban eldönthet®k. Pl. az

n-dimenziós euklideszi ill. hiper-

bolikus geometria.

184