S5EC ve KD45-O modal mantıklarının modelleri üzerine

Tam metin

(1)˙ ¨ ¨ UN ¨ IVERS ˙ ˙ T.C. ISTANBUL KULT UR ITES I˙ ˙ IMLER ˙ ˙ US ¨ U ¨ FEN BIL I˙ ENSTIT. S5EC ve KD45-O MODAL MANTIKLARININ MODELLERI˙ ¨ ˙ UZER INE. ¨ ˙ YUKSEK LISANS TEZI˙ ¨ UK ¨ Ay¸se BOL 1009041002. Anabilim Dalı : Matematik - Bilgisayar Programı : Matematik - Bilgisayar Tez Danı¸smanı. : Prof. Dr. C ¸ i˘ gdem GENCER. Temmuz 2013.

(2) ¨ ¨ ONS OZ. Bu ¸calı¸smamın i¸cinde daima yer alan, hi¸cbir yardım teklifimi geri ¸cevirmeyen, zorlandı˘gım zaman beni motive eden, yaptı˘gı yorumlarla bana rehber olan Prof. Dr. C ¸ i˘gdem GENCER’e; sordu˘gum her soruya verdi˘gi tatmin edici cevaplarla beni etkileyen Prof. Dr. Dick de JONGH’a; bu tezin yazımında yardım eden, zor˙ ¨ landı˘gım zamanlarda benimle birlikte d¨ u¸su ¨nen Istanbul K¨ ult¨ ur Universitesi’ndeki ˙ ATES¸’e ve son olarak varlıklarını her zaman yanımda hisarkada¸sım Ilayda setti˘gim aileme te¸sekk¨ ur ederim.. ¨ UK ¨ Ay¸se BOL. Temmuz 2013. ii.

(3) ˙ ¸ INDEK ˙ ˙ IC ILER. ¨ OZET .................................................................... v. ABSTRACT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vi 1 Giri¸s . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 1. ¨ Bilgiler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 On. 3. 2.1. 2.2. Epistemik Mantık . . . . . . . . . . . . . . . . . . . . . . . . . . .. 3. 2.1.1. Epistemik Mantık Sentaksı . . . . . . . . . . . . . . . . . .. 4. 2.1.2. Epistemik Mantık Semanti˘gi . . . . . . . . . . . . . . . . .. 4. 2.1.3. S5EC Sistemi . . . . . . . . . . . . . . . . . . . . . . . . .. 8. KD45 Modal Mantı˘gı . . . . . . . . . . . . . . . . . . . . . . . . .. 9. 2.2.1. KD45 Modal Mantık Sentaksı . . . . . . . . . . . . . . . .. 10. 2.2.2. KD45 Modal Mantık Semanti˘gi . . . . . . . . . . . . . . .. 10. 2.2.3. KD45-O Modal Sistemi . . . . . . . . . . . . . . . . . . . .. 11. 2.2.4. ˙ Modal Modellerde Homomorfizma ve Izomorfizma . . . . .. 13. 3 S5EC ve KD45-O Modal Mantıkları i¸cin Sa˘ glamlık Teoremleri. 15. 3.1. S5EC Modal Mantı˘gında Sa˘glamlık . . . . . . . . . . . . . . . . .. 15. 3.2. KD45-O Modal Mantı˘gında Sa˘glamlık. 17. . . . . . . . . . . . . . . .. 4 S5EC ve KD45-O Modal Mantıkları i¸cin Tamlık Teoremleri . . . 22 4.1. 4.2. Kanonik Model . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 22. 4.1.1. S5EC’nin Kanonik Modeli . . . . . . . . . . . . . . . . . .. 26. 4.1.2. KD45-O’nun Kanonik Modeli . . . . . . . . . . . . . . . .. 28. ¨ Sonlu Model Ozelli˘ gi . . . . . . . . . . . . . . . . . . . . . . . . .. 28. 4.2.1. Sonlu Henkin Yöntemi . . . . . . . . . . . . . . . . . . . .. 29. 4.2.2. S5EC i¸cin Sonlu Henkin Yöntemi . . . . . . . . . . . . . .. 30. 4.2.3. KD45-O i¸cin Sonlu Henkin Yöntemi . . . . . . . . . . . . .. 36. iii.

(4) 4.2.4. Filtreleme Yöntemi . . . . . . . . . . . . . . . . . . . . . .. 42. 4.2.5. S5EC i¸cin Filtreleme Yöntemi . . . . . . . . . . . . . . . .. 44. 4.2.6. KD45-O i¸cin Filtreleme Yöntemi . . . . . . . . . . . . . .. 47. 5 Yeni Sonuclar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 5.1. S5EC Modal Mantı˘gı i¸cin Yeni Sonu¸clar . . . . . . . . . . . . . .. 49. 5.2. KD45-O Modal Mantı˘gı i¸cin Yeni Sonu¸clar . . . . . . . . . . . . .. 52. 6 Sonu¸c . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 KAYNAKLAR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ¨ ˙ ¸ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 OZGEC ¸ MIS. iv.

(5) ¨ Universitesi. :. ˙ ¨ Istanbul K¨ ult¨ ur Universitesi. Enstit¨ us¨ u. :. Fen Bilimleri. Anabilim Dalı. :. Matematik - Bilgisayar. Programı. :. Matematik - Bilgisayar. Tez Danı¸smanı. :. Prof. Dr. C ¸ i˘ gdem GENCER. Tez T¨ ur¨ u ve Tarihi. :. Y¨ uksek Lisans - Temmuz 2013. ¨ OZET S5EC ve KD45-O MODAL MANTIKLARININ MODELLERI˙ ¨ ˙ UZER INE ¨ UK ¨ Ay¸se BOL Bu tezde, S5EC ve KD45-O modal mantıklarının sonlu Henkin ve filtreleme y¨ ontemiyle elde edilen modellerinin izomorf oldu˘ gu ispatlanmı¸stır. Bu ama¸cla S5EC ve KD45-O modal mantıklarının modal tamlı˘ gından ve kanonik modellerinden yararlanılmı¸stır.. Anahtar Kelimeler. :. Epistemik mantık, makul olma, sa˘ glamlık, tamlık, kanonik model, sonlu Henkin y¨ ontemi, filtreleme y¨ ontemi.. v.

(6) University. :. ˙ Istanbul K¨ ult¨ ur University. Institute. :. Institute of Science. Science Programme. :. Mathematics and Computer. Programme. :. Mathematics and Computer. Supervisor. :. Prof. Dr. C ¸ i˘ gdem GENCER. Degree Awarded and Date. :. M.Sc. - July 2013. ABSTRACT ON MODELS OF THE MODAL LOGICS S5EC AND KD45-O ¨ UK ¨ Ay¸se BOL We prove in this thesis that the models for the modal logics S5EC and KD45-O obtained by the finite Henkin method are isomorphic to the ones obtained by the filtration. For that purpose, we use the completeness and canonical models.. Keywords. :. Epistemic logic, plausibility, soundness, completeness, canonical model, finite Henkin method, filtration method.. vi.

(7) ¨ lu ¨m 1 Bo Giri¸s ˙ olarak felsefe alanındaki ¸calı¸smalarda kullanılan modal mantık, g¨ Ilk un¨ um¨ uzde matematik, bilgisayar bilimleri, yapay zeka ve oyun teori gibi alanlarda da kullanılmaktadır. Ge¸cmi¸si antik Yunanlılara kadar dayanmasına ra˘gmen 1918’e kadar modalite alanındaki ¸calı¸smalar informel olarak kalmı¸stır. Modalite kavramlarına formel olarak ilk yakla¸sım, C .I. Lewis’in 1918’deki ¸calı¸smasında, ’zorunluluk’ ve ’olanaklılık’ modal kavramları olarak kar¸sımıza ¸cıkmaktadır [12]. Bu fikre göre bir ϕ form¨ ul¨ u i¸cin ϕ ve ♦ϕ ifadeleri sırasıyla ’ϕ zorunludur’, ’ϕ olasıdır’ olarak ifade edilir. Bu tarihten sonra ba¸ska kavramları da formel olarak ifade etmek i¸cin modal operatörler kullanılmı¸stır. 1930’larda Kurt Gödel, matematiksel ispatlanabilirlik kavramını formelize etmek i¸cin modal operatör kullanmayı tercih etmi¸stir. Burada Gödel, ϕ’yi ϕ’nin matematiksel ispatlanabilirli˘gi olarak, ♦ϕ’yi ise ϕ’nin tutarlılı˘gı olarak yorumlamı¸stır [4]. Lewis ve Gödel’in ¸calı¸smalarını takip eden yıllarda dinamik mantık, zaman mantı˘gı ve epistemik mantık gibi mantıklar, çe¸sitli modaliteleri modal operatörler ¨ gin epistemik mantıkta, semantik olarak operatör¨ arasına eklemi¸slerdir. Orne˘ u gibi ¸calı¸san K operatör¨ u bir ¸seyin bilinmesi olarak ifade edilir [6]. Modal mantı˘gın alt mantıklardan olan epistemik mantık, bilgisayar biliminde bilgi tabanlı programlamanın ana konularından biri haline gelmi¸stir [4]. Bu ¸calı¸smada, epistemik mantı˘gın temel kavramları olan bilgi ve de˘gerleri ele alan S5EC ve KD45-O modal mantıkları incelenmi¸stir. Bu ama¸cla o¨ncelikle Böl¨ um 2’de bu mantıkların dili, form¨ ulleri, aksiyom sistemleri, t¨ uretim kuralları ve modelleri tanımlanmı¸stır. Böl¨ um 3 ve böl¨ um 4’te verilen aksiyom sistemlerinin sa˘glam ve tam olduk1.

(8) ları gösterilmi¸stir. Tamlık ispatında filtreleme ve sonlu Henkin metodları uygulanmı¸stır. Böl¨ um 5’te ise filtreleme ve sonlu Henkin metoduyla elde edilen modellerin izomorf oldukları ispatlanmı¸stır.. 2.

(9) ¨ lu ¨m 2 Bo ¨ Bilgiler On 2.1. Epistemik Mantık. Bu böl¨ umde tezin okunabilirli˘gini kolayla¸stırmak amacıyla bazı temel tanım ve kavramlar verilmi¸stir. Buradaki t¨ um bilgiler [1], [2], [5], [10]’da bulunabilir. Mantı˘gın ve mantıksal formalizmin bilgisayar bilimlerinde, yapay zeka ve ekonomi gibi alanlarda kullanımı son yıllarda b¨ uy¨ uk oranda artmı¸stır. Bu mantıklar orjinal olarak felsefe i¸cin geli¸stirilmi¸s olan mantıklardır. Bu mantıklardan biri olan epistemik mantık, modal mantı˘gın temel kavramları olan zorunluluk ve olanaklılık kavramlarının epistemik anlamda yeniden yorumlanmasıyla elde edilmi¸stir. Bilgi ve de˘gerler kavramlarına dayalı olan epistemik mantık, bu kavramları formel olarak incelemek i¸cin geli¸stirilmi¸stir. Bilgi kavramının formel hale getirilmesi ilk olarak von Wright’ın [15] ¸calı¸smalarında ortaya ¸cıkar ve bu ¸calı¸smalar daha ¸cok sentaks temeline dayanır. Daha sonra Hintikka 1962 yılında yazdı˘gı bir kitapta m¨ umk¨ un d¨ unyalar semanti˘gini kullanarak bilgi kavramına a¸cık bir semantik verenlerden biri olmu¸stur [8]. Ge¸cmi¸si Leibniz’e kadar uzanan ve Hintikka tarafından geli¸stirilip formalizasyonunun da Kripke [11] tarafından yapıldı˘gı m¨ umk¨ un d¨ unyalar kavramı, bilginin formel hale getirilmesinde temel bir rol oynamı¸stır. M¨ umk¨ un d¨ unyalar kavramının altında yatan fikir, bir ki¸sinin ger¸cek bir durumun yanında alternatif ba¸ska durumların (m¨ umk¨ un d¨ unyaların) da var oldu˘gunu d¨ u¸su ¨nmesidir. Buradan, bir ki¸sinin bir ϕ ifadesini bilmesi i¸cin gerek ve yeter ko¸sulun onun m¨ umk¨ un oldu˘gunu d¨ u¸su ¨nd¨ u˘gu ¨ (onun bilgisiyle tutarlı olan) her du¨ gin San Francisco’da ya¸sayan rumda ϕ’nin do˘gru olması olarak ortaya ¸cıkar. Orne˘ bir a ki¸sisinin Londra’daki hava durumu hakkında bir bilgisi yoksa onun i¸cin 3.

(10) m¨ umk¨ un olan bazı d¨ unyalarda ”Londra’da hava g¨ une¸slidir” ifadesi sa˘glanırken, bazı d¨ unyalarda da ”Londra’da hava ya˘gmurludur” ifadesi sa˘glanır. Bu nedenle de bu ki¸sinin Londra’daki havanın g¨ une¸sli oldu˘gunu bildi˘gini söyleyemeyiz. Bununla birlikte e˘ger g¨ uvenilir bir kaynaktan havanın g¨ une¸sli oldu˘gu bilgisini alırsa artık o ”Londra’da hava ya˘gmurludur” ifadesinin sa˘glandı˘gı d¨ unyaları m¨ umk¨ un d¨ unya olarak görmeyecektir [7]. S¸imdi bilgi kavramının formel olarak nasıl ifade edilece˘gini inceleyelim.. 2.1.1. Epistemik Mantık Sentaksı. Epistemik mantı˘gın dili, klasik o¨nermeler mantı˘gının diline K (knowledge) operatör¨ un¨ un eklenmesiyle elde edilir. Tanım 2.1.1. n ∈ N i¸cin P = {pn | n ∈ N } atomik önermeler k¨ umesi ve A = {1, ..., m}, m temsilcilerin bir k¨ umesi olsun. A u ¨zerindeki ϕ, ψ, ... epistemik form¨ ullerin LK k¨ umesi a¸sa˘gıdaki özellikler altında kapalı en k¨ u¸cu ¨k k¨ umedir: (i) p ∈ P ise p ∈ LK , (ii) ϕ, ψ ∈ LK ise (ϕ ∧ ψ), ¬ϕ ∈ LK , (iii) ϕ ∈ LK ise her i ∈ A i¸cin Ki ϕ ∈ LK . Burada Ki ϕ; i ki¸sisi ϕ’yi bilir ¸seklinde yorumlanır. Burada ”ki¸si” bir insan, makine veya bir oyundaki oyuncu da olabilir. Bununla birlikte Ki modal opeˆ i = ¬Ki ¬ϕ; i ki¸sisi ϕ ger¸ce˘ginin do˘gru olabiratör¨ un¨ un dual operatör¨ u olan K lece˘gini d¨ u¸su ¨n¨ ur ¸seklinde yorumlanabilir.. 2.1.2. Epistemik Mantık Semanti˘ gi. Tanım 2.1.2. P atomik önermelerin sayılabilir bir k¨ umesi ve A ki¸silerin sonlu bir k¨ umesi olsun. i ∈ A olmak u ¨zere bir epistemik Kripke model, M = hS, Ri , V i yapısıdır öyle ki (i) S bo¸stan farklı durumlar k¨ umesi, (ii) Ri , S u ¨zerinde eri¸silebilirlik ba˘gıntısı, (iii) V her bir duruma do˘gruluk de˘geri atayan bir fonksiyondur. E˘ger i ki¸sisi iki durumu birbirinden ayırt edemiyorsa iki durum arasında Ri ba˘gıntısı vardır. Bu nedenle bu ba˘gıntıya ayırtedilmezlik ba˘gıntısı da denir. Genel olarak ayırtedilemezlik ba˘gıntısı denklik ba˘gıntısı olarak ele alınır. 4.

(11) ¨ Ornek 2.1.3. Groningen, Liverpool ve Otago (GLO) senaryosunun modelinde ayırtedilemezlik ba˘gıntısını inceleyelim [6]. Bir b ki¸sisi Groningen ¸sehrinde ya¸sasın ve Groningen ile Liverpool ¸sehirlerindeki hava durumu hakkında bir teori olu¸stursun. Buna göre Groningen’de hava ya g¨ une¸slidir (g ile gösterelim) veya de˘gildir (¬g), benzer durum Liverpool i¸cin de ge¸cerlidir: g¨ une¸sli (l) veya de˘gil (¬l). Bu durumda a¸sa˘gıdaki 4 durum ortaya ¸cıkmaktadır. b. . (¬g, l). (g, l) O. b. b. O . . (g, ¬l). b. (¬g, ¬l). T b. J. b. S¸ekil 1. GLO modeli Burada (g,l) durumu hem Groningen’de hem de Liverpool’da havanın g¨ une¸sli oldu˘gu durumu göstermektedir. b, Groningen’de ya¸sadı˘gından buradaki hava durumunu bilir fakat Liverpool’dakini bilemez. Ba¸ska bir de˘gi¸sle (g,l) durumunu (g,¬l) durumundan ayıramazken (¬g,l) durumunu da (¬g,¬l)’den ayıramaz. Tanım 2.1.4. Bir ϕ form¨ ul¨ un¨ un t¨ uretimi ϕ1 , ϕ2 , ..., ϕn = ϕ form¨ ullerinin sonlu dizisidir öyle ki 1 ≤ i ≤ n i¸cin her bir ϕi form¨ ul¨ u ya bir aksiyomdur ya da kendinden önce gelen ϕj (j < i i¸cin) form¨ ullerine bir t¨ uretim kuralı uygulanarak elde edilir. Bir ϕ form¨ ul¨ u, S sisteminin kuralları ve aksiyomları kullanılarak t¨ uretilmi¸sse S ` ϕ yazılır. Bu durumda ϕ’ye S-teoremdir denir. S¸imdi bir epistemik modeli ve bu modelde do˘gruluk kavramını inceleyelim. Tanım 2.1.5. M = hS, Ri , V i bir Kripke model ve s bir durum olmak u ¨zere, epistemik form¨ uller (M, s) ikilisi u ¨zerinde yorumlanırlar. (M, s), s ∈ S anlamındadır. M epistemik bir model ise (M, s) ikilisine bir epistemik durum denir. (M, s) yerine M, s yazılacaktır. M = hS, Ri , V i bir model olmak u ¨zere; M, s’de ϕ do˘grudur ifadesi M, s |= ϕ ¸seklinde yazılır ve a¸sa˘gıdaki gibi tanımlanır: (i) M, s |= p olması i¸cin gerek ve yeter ko¸sul (g.y.k.) s ∈ V (p) olmasıdır. (ii) M, s |= ¬ϕ olması i¸cin (g.y.k.) M, s |= ϕ olmamasıdır. (iii) M, s |= ψ ∧ χ olması (g.y.k.) M |= ψ ve M |= χ olmasıdır. (iv) M, s |= Ki ϕ olması i¸cin (g.y.k.) (s, t) ∈ Ri olan her t i¸cin M, t |= ϕ olmasıdır. ˆ i ϕ olması i¸cin (g.y.k.) (s, t) ∈ Ri en az bir t vardır öyle ki (s, t) ∈ (v) M, s |= K Ri ve M, t |= ϕ’dir.. 5.

(12) ϕ bir epistemik form¨ ul olsun. ϕ’nin bir M = hS, Ri , V i Kripke modelinde ge¸cerli (M, s |= ϕ) olması i¸cin (g.y.k.) her s ∈ S i¸cin M, s |= ϕ olmasıdır. Bununla birlite ϕ’nin ge¸cerli (|= ϕ) olması i¸cin (g.y.k.) her M ve her s ∈ S i¸cin M, s |= ϕ olmasıdır. ϕ form¨ ul¨ u M modelinin bir s durumunda yanlı¸s ise ϕ form¨ ul¨ u s’de yanlı¸stır denir ve M, s 2 ϕ ile gösterilir. ¨ Onerme 2.1.6. Bir S5EC modelde |= ψ ve |= ψ → ϕ ise |= ϕ’dir. ˙ Ispat. M bir S5EC model ve s, bu model u ¨zerinde keyfi bir durumu i¸cin M, s |= ψ → ϕ ve M, s |= ψ olsun. Bu durumda M, s |= ¬ψ ∨ ϕ’dir. Buradan M, s 2 ψ ∨ M, s |= ϕ elde edilir. Bununla birlikte M, s |= ψ oldu˘gundan M, s |= ϕ olur. M ve s keyfi olarak se¸cildiklerinden |= ϕ elde edilir.. . ¨ Ornek 2.1.7. GLO senaryosundaki model M1 olsun. M1 , (¬g, l) |= Kb ¬g ∧ ¬Kb l’dir. ˙ Ispat. M1 , (¬g, l) |= Kb ¬g’dir çu ¨nk¨ u b’nin (¬g, l) durumundan ayırt edemedi˘gi durumlar (¬g, l), (¬g, ¬l)’dir ve M1 , (¬g, l) |= ¬g, M1 , (¬g, l) |= ¬g oldu˘gundan M1 , (¬g, l) |= Kb ¬g’dir. Bununla birlikte yine (¬g, l) durumunun ba˘glantılı oldu˘gu durumlardan bir tanesi (¬g, ¬l) ve M1 , (¬g, ¬l) |= ¬l oldu˘gundan M1 , (¬g, l) |= ¬Kb l’dir. Buradan M1 , (¬g, l) |= Kb ¬g ∧ ¬Kb l olur.. . Bilgi i¸cin aksiyom sistemini tanımlamak i¸cin öncelikle minimal modal mantık K’yi tanımlayalım. Tanım 2.1.8. A = {1, ..., m} olmak u ¨zere, K sistemi a¸sa˘gıdaki aksiyomları i¸ceren ve verilen t¨ uretim kuralları altında kapalı olan bir sistemdir: Aksiyomlar: (A1) B¨ ut¨ un önermesel totolojiler (A2) Ki (ϕ → ψ) → (Ki ϕ → Ki ψ)(i = 1, ..., m) T¨ uretim Kuralları: (R1) Modus Ponens : (R2) Zorunluluk :. ϕ,ϕ→ψ ψ. ve. ϕ ’dir. Ki ϕ. Burada (A2) aksiyomu K aksiyomu olarak adlandırılır ve bu aksiyom bilginin t¨ uretim altında kapalı oldu˘gunu söyler. Bununla birlikte (A1) ve (A2) aksiyomları 6.

(13) bilgi kavramını tam olarak temsil edemez. Bunun i¸cin K sisteminin aksiyomlarına a¸sa˘gıdaki aksiyomlar eklenir: (A3) Ki ϕ → ϕ(i = 1, ..., m) (A4) Ki ϕ → Ki Ki ϕ(i = 1, ..., m) (A5) ¬Ki ϕ → Ki ¬Ki ϕ(i = 1, ..., m) (A3), (A4) ve (A5) aksiyomları sırasıyla T, 4 ve 5 ¸semaları olarak da adlandırılırlar. (A1)-(A5) aksiyomları (R1)-(R3) t¨ uretim kurallarından olu¸san bu mantık S5 mantı˘gı olarak adlandırılır. S5 sistemi, bilgi kavramını temsil etmesi a¸cısından di˘ger sistemlere göre teknik özellikleriyle daha iyi ve yeterli bir sistemdir. S¸imdi de aksiyomlar ile modeller arasındaki ili¸skiyi ifade eden o¨nermeyi verelim. ¨ Onerme 2.1.9. M = hS, Ri , V i Kripke model olmak u ¨zere, (i) M |= A3 ise M yansımalı, (ii) M |= A4 ise M ge¸ci¸sli, (iii) M |= A5 ise M öklidyen’dir. ˙ Ispat. (i) M |= (A3) olsun. Bu durumda her s ∈ S i¸cin M, s |= Ki ϕ → ϕ’dir. ¨ Buradan M, s |= Ki ϕ → M |= ϕ olur. Oyleyse M, s |= Ki ϕ ise M, s |= ϕ’dir. s0 ∈ S ve (s, s0 ) ∈ Ri olsun. O halde model tanımından M, s0 |= ϕ’dir. Bununla birlikte M, s |= ϕ oldu˘gu i¸cin özel olarak s0 , s olarak se¸cilirse (s, s0 ) ∈ Ri olur. Ri yansımalıdır. ¨ (ii)M |= (A4) olsun. Oyleyse her s ∈ S i¸cin M, s |= Ki ϕ → Ki Ki ϕ’dir. ¨ Oyleyse M, s |= Ki ϕ ise M, s |= Ki Ki ϕ’dir. t, m ∈ S ve (s, t), (t, m) ∈ Ri olsun. M, s |= Ki Ki ϕ ise M, t |= Ki ϕ olur. Buradan M, m |= ϕ elde edilir. Bununla birlikte M, s |= Ki ϕ kullanılırsa (s, m) ∈ Ri olur. Ri ge¸ci¸slidir. (iii) M |= (A5) olsun. Bu durumda her s ∈ S i¸cin M, s |= ¬Ki ϕ → Ki ¬Ki ϕ’dir. (s, t), (s, u) ∈ Ri olsun. (t, u) ∈ Ri oldu˘gunu göstermeliyiz. M, s |= Ki ¬Ki ϕ ise M, t |= ¬Ki ϕ’dir. O halde bir t0 ∈ S vardır oÿle ki (t, t0 ) ∈ Ri ve M, t0 |= ¬ϕ’dir. Bununla birlikte M, s |= ¬Ki ϕ ise (s, u) ∈ Ri oldu˘gundan M, u |= ¬ϕ’dir. Bu durumda model olma tanımı kullanılarak t0 , u olarak se¸cilirse (t, u) ∈ Ri olur. O halde Ri o¨klidyendir.. . 7.

(14) Tanım 2.1.10. S5 modal mantı˘gı i¸cin bir Kripke model hS, Ri , V i’de Ri yansımalı, simetrik ve ge¸ci¸slidir.. 2.1.3. S5EC Sistemi. Bir o¨nceki böl¨ umde temel bilgi kavramını inceledik. Bu böl¨ umde ise bilginin grup kavramlarını inceleyece˘giz. Bunlardan ilki, genel bilgi kavramıdır ve E (everyone knows) ile gösterilir. E˘ger ϕ bir B grubunun b¨ ut¨ un ki¸sileri arasında biliniyorsa ϕ genel bilgi (general knowledge) olarak adlandırılır ve EB ϕ ile gösterilir. ˙ Ikinci kavram ortak bilgi (common knowledge) kavramıdır; e˘ger ϕ do˘gru ve grubun b¨ ut¨ un ki¸sileri tarafından biliniyor, bununla birlikte her bir ki¸si di˘gerlerinin ϕ’yi bildi˘gini biliyor ve bu ¸sekilde devam ediyorsa ϕ’ye ortak bilgi denir ve CB ϕ ile gösterilir. A ki¸silerin sonlu k¨ umesi olmak u ¨zere, EB ϕ =. V. i∈A. Ki ϕ,. CB ϕ = ϕ ∧ Eϕ ∧ EEϕ...’dir. ˙ general (koordineli saldırı) örne˘gini inceleyelim. a ve b iki ¨ Ornek 2.1.11. Iki m¨ uttefik general iki da˘gda bekliyor ve d¨ u¸smanları da bu iki da˘gın arasındaki va˙ diden ge¸cecek olsun. Ikisi birlikte aynı zamanda d¨ u¸smanlarına saldırırlarsa sava¸s bu generaller tarafından kazanılacak, sadece bir tanesi saldırırsa kaybedilecektir. General a, b’ye saldırının ne zaman olaca˘gına dair bir ϕ mesajı göndersin ve bu mesaj b tarafından alınsın. Bu durumda hem Kb ϕ hem de Kb Ka ϕ do˘gru olur. Fakat mesajın b’ye ula¸sıp ula¸smadı˘gını a hen¨ uz bilmedi˘ginden Ka Kb ϕ do˘gru de˘gildir. b, mesajı aldı˘gına dair a’ya mesaj göndersin, öyleyse Ka Kb Ka ϕ do˘gru olur. Ancak b mesajın a tarafından alındı˘gından emin de˘gildir dolayısıyla Ka Kb Ka ϕ ger¸ceklenmez. Böylece hi¸cbir zaman CB ϕ kurulamayacaktır. O halde a ve b’nin e¸s zamanlı hareket edebilmeleri i¸cin ortak bilgi gereklidir. S5EC sisteminin dili LKEC , epistemik mantı˘gının diline E ve C operatörlerinin eklenmesiyle elde edilir. Tanım 2.1.12. n ∈ N i¸cin P = {pn | n ∈ N } atomik önermeler k¨ umesi ve A = {1, ..., m}, m temsilcilerin bir k¨ umesi olsun. A u ¨zerindeki ϕ, ψ, ... epistemik form¨ ullerin LKEC k¨ umesi a¸sa˘gıdaki özellikler altında kapalı en k¨ u¸cu ¨k k¨ umedir: (i) p ∈ P ise p ∈ LKEC , (ii) ϕ, ψ ∈ LKEC ise (ϕ ∧ ψ), ¬ϕ ∈ LKEC , (iii) ϕ ∈ LKEC ise her i ∈ A i¸cin Ki ϕ ∈ LKEC , (iv) ϕ ∈ LKEC ise her i ∈ A i¸cin CB ϕ, EB ϕ ∈ LKEC ’dir. Tanım 2.1.13. Bir B grubu i¸cin S bir k¨ ume ve Rb (b ∈ B), S u ¨zerinde bir ba˘gıntı olsun. 8.

(15) (i) REB =. S. b∈B. RB .. (ii) Bir R ba˘gıntısının ge¸ci¸smeli kapanı¸sı en k¨ u¸cu ¨k R+ ba˘gıntısıdır öyle ki (1) R ⊆ R+ ; (2) Her x, y, z i¸cin e˘ger (R+ xy&R+ yz) ise R+ xz’dir. R0 nin yansımalı ve ge¸ci¸smeli kapanı¸sı R∗ ile gösterilir. Tanım 2.1.14. P atomik önermelerin sayılabilir bir k¨ umesi ve A temsilcilerin sonlu bir k¨ umesi olsun. i ∈ A ve p ∈ P olmak u ¨zere S5EC mantı˘gının bir Kripke modeli M = hS, Ri , RE , RC , V i a¸sa˘gıdaki gibi tanımlanır: (i) S bo¸stan farklı durumlar k¨ umesi, (ii) Her i ∈ A i¸cin Ri ⊆ SxS, RE = R1 ∪ ... ∪ Rm , ∗ , RC = RE. (iii) V (p) ⊆ S’dir. Tanım 2.1.15. M = hS, Ri , RE , RB , V i ve s ∈ S olsun. ϕ, bir epistemik form¨ ul olmak u ¨zere, M, s |= Eϕ ⇔ ∀t, (s, t) ∈ REB ise M, t |= ϕ. ∗ ise M, t |= ϕ. M, s |= Cϕ ⇔ ∀t, (s, t) ∈ RE B. Tanım 2.1.16. S5EC sistemi, (A1)-(A5) aksiyomlarına ve (R1),(R2) t¨ uretim kurallarına a¸sa˘gıda verilen aksiyomların ve t¨ uretim kuralının eklenmesiyle elde edilir: (A6) Eϕ ↔ K1 ϕ ∧ ... ∧ Km ϕ (A7) Cϕ → ϕ (A8) Cϕ → ECϕ (A9) (Cϕ ∧ C(ϕ → ψ)) → Cϕ (A10) C(ϕ → Eϕ) → (ϕ → Cϕ) T¨ uretim Kuralları: ϕ (R3) Cϕ. 2.2. KD45 Modal Mantı˘ gı. Bu böl¨ umde bilginin ba¸ska bir bi¸cimi olan de˘ger (inan¸c) kavramını inceleyece˘giz. Plato, bilginin gerek¸celendirilmi¸s do˘gru inan¸c oldu˘gunu iddia etmi¸s ve bu iddia uzun bir s¨ ure felsefeciler tarafından tartı¸sılmı¸stır. Fakat Gettier [9] 1963 9.

(16) yılında yayımladı˘gı makalesinde bu iddiaya kar¸sı örnekler vermi¸stir. Bu tarihten sonra epistemolojide gerek¸celendirilmi¸s do˘gru inan¸c, bilgi i¸cin gerekli olan ko¸sullardan sadece biri olarak ele alınmı¸stır. Bu tanıma dayanarak bilgi ve inan¸c kavramları arasıdaki ili¸skinin Kϕ → Bϕ oldu˘gu gör¨ ul¨ ur. Her ne kadar de˘ger kavramı i¸cin ¸ce¸sitli mantıklar var olsa da bizim ele alaca˘gımız mantıkta inan¸c, do˘gru olması gerekmeyen bilgi olarak dikkate alınacaktır. Buradan yola çıkarak bilgi ve de˘ger arasındaki temel farklılı˘gın bilgide verilen ifadenin do˘gru olması gerekirken, inan¸cta do˘gru olamayabilece˘gi oldu˘gunu gör¨ ur¨ uz. Bu durumda T ¸seması olarak adlandırılan S5 sistemindeki (A3) aksiyomu, Bϕ → ϕ, bu mantıkta ger¸ceklenmez. Bununla birlikte inanılan o¨nermelerin tutarlı olması beklenir, yani aynı anda hem ϕ’ye hem de onun tersi olan ¬ϕ’ye inanılamaz. Bu ise T aksiyomundan daha zayıf bir aksiyom olan D: ¬B ⊥ ile gösterilir. Bu mantı˘gın di˘ger aksiyomları S5 sistemindekiyle benzerdir. Elde edilen bu yeni sistem, KD45 sistemi olarak adlandırılır ki bu sistem zayıf S5 sistemi olarak da ele alınır.. 2.2.1. KD45 Modal Mantık Sentaksı. A ki¸siler k¨ umesi ve i ∈ A olmak u ¨zere, KD45 mantı˘gının dili bilgi mantı˘gının diliyle aynıdır ve burada Ki operatör¨ un¨ un yerine Bi operatör¨ u vardır.. 2.2.2. KD45 Modal Mantık Semanti˘ gi. Form¨ ullerin semanti˘gi bilgi mantı˘gındakiyle aynıdır fakat burada ba˘gıntılar bilgi yerine ki¸silerin de˘gerleri ile ba˘glantılıdır ve Bi operatör¨ un¨ un bir KD45 modelde do˘grulu˘gu a¸sa˘gıdaki gibi tanımlanır: M, s |= Bi ϕ ⇔ (s, t) ∈ Ri olan her t i¸cin M, t |= ϕ. Tanım 2.2.1. KD45 sistemi a¸sa˘gıdaki aksiyomları i¸ceren ve verilen t¨ uretim kuralları altında kapalı olan bir sistemdir: (A1) B¨ ut¨ un önermesel totolojiler (A2) Bi (ϕ → ψ) → (Bi ϕ → Bi ψ)(i = 1, ..., m) (D) ¬Bi (⊥) (A4) Bi ϕ → Bi Bi ϕ(i = 1, ..., m). 10.

(17) (A5) ¬Bi ϕ → Bi ¬Bi ϕ(i = 1, ..., m) T¨ uretim Kuralları: (R1) Modus Ponens : (R2) Zorunluluk :. ϕ,ϕ→ψ ψ. ve. ϕ ’dir. Bi ϕ. Tanım 2.2.2. KD45 modal mantı˘gı i¸cin bir M modeli ge¸ci¸sli, serial ve öklidyendir.. 2.2.3. KD45-O Modal Sistemi. ˙ Insanlar se¸cim yaparken veya karar verirken kendilerinde var olan inan¸clarını (de˘gerlerini) kullanılar. Bir bahis oyununda para yatıraca˘gımız takımı se¸cerken bu takımlardan hangisinin kazanaca˘gına dair olan inancımız daha kuvvetliyse ona para yatırırız. Bir i¸s ba¸svurusunda bulunan adaylardan hangisinin i¸si yapabilece˘gine dair inancımız daha g¨ u¸cl¨ uyse onu se¸ceriz. ˙ Inan¸ cların kar¸sıla¸stırılması i¸cin formel dil olu¸sturmadan o¨nce sıralama kavramına de˘ginelim. ϕ ve ψ iki form¨ ul olmak u ¨zere Bϕ Bψ, ϕ’ye olan inancın ψ’ye olandan daha g¨ uçl¨ u oldu˘gunu göstermektedir. Buradaki Bϕ Bψ yerine ϕ B ψ yazılacaktır. D¨ unyalar arasındaki sıralama, bir yarı lineer sıralama ba˘gıntısı olan ≤ ba˘gıntısı olacaktır. w ≤ v ifadesi, w d¨ unyası v’den daha makuld¨ ur olarak yorumlanacaktır. D¨ unyaların k¨ umeleri arasındaki sıralamada ise yine yarı lineer sıralama ba˘gıntısı olan ≥B ba˘gıntısı kullanılacaktır. Tanım 2.2.3. Atomik önermelerin sayılabilir k¨ umesi Φ verilmi¸s olsun. p ∈ Φ olmak u ¨zere bir ϕ, ψ KD45-O form¨ ullerin LB sonlu k¨ umesi a¸sa˘gıdaki özellikler altında en k¨ u¸cu ¨k k¨ umedir: (i) p ∈ P ise p ∈ LB , (ii) ϕ, ψ ∈ LB ise (ϕ ∨ ψ), ¬ϕ ∈ LB , (iii) ϕ ∈ LB ise Bϕ, U ϕ ∈ LB , (iv) ϕ, ψ ∈ LB ise ϕ B ψ, ϕ <B ψ ∈ LB ’dir. Tanım 2.2.4. S, bo¸stan farklı sonlu durum k¨ umesi; V, do˘gruluk de˘ger ataması fonksiyonu; ≤, S u ¨zerinde tanımlı yarı lineer sıralama ba˘gıntısı ve ≥B , P(S) u ¨zerinde tanımlı yarı lineer sıralama ba˘gıntısı olmak u ¨zere M = hS, ≤, ≥B , V i modeli a¸sa˘gıdaki ko¸sulları ger¸cekleyen bir KD45-O modeldir: (i) X ⊆ Y ise Y ≥ X, 11.

(18) (ii) B, ≤-minimal d¨ unyaların k¨ umesi olmak u ¨zere, e˘ger B ⊆ X ve B * Y ise X >B Y ’dir. Burada >B sıralaması kesin sıralamadır, (iii) X 6= ∅ ise X >B ∅, burada ≤-minimal d¨ unyaların k¨ umesi B = {t | her t0 ∈ S i¸cin t ≤ t0 }’dır [3]. Tanım 2.2.5. Bir KD45-O model M’de ϕ form¨ ul¨ un¨ un do˘gruluk tanımı a¸sa˘gıdaki ¸sekilde verilir: (i) M, s |= p olması i¸cin gerek ve yeter ko¸sul (g.y.k.) s ∈ V (p) olmasıdır. (ii) M, s |= ¬ϕ olması i¸cin (g.y.k.) M, s |= ϕ olmamasıdır. (iii) M, s |= ψ ∨ χ olması (g.y.k.) M |= ψ veya M |= χ olmasıdır. (iv) M, s |= Bi ϕ olması i¸cin (g.y.k.) her ≤-minimal d¨ unya t i¸cin M, t |= ϕ olmasıdır. (v) M, s |= U ϕ olması i¸cin (g.y.k.) her t d¨ unyası i¸cin M, t |= ϕ olmasıdır. (vi) M, s |= ϕ < ψ olması i¸cin (g.y.k.) {t|M, t |= ϕ} ≥B {t|M, t |= ψ} olmasıdır. (vii) M, s |= ϕ ψ olması i¸cin (g.y.k.) {t|M, t |= ϕ} >B {t|M, t |= ψ} olmasıdır. Burada U ϕ, modeldeki her m¨ umk¨ un d¨ unyada ϕ do˘grudur ¸seklinde ifade edilir. ¬U ¬ϕ’nin duali olan Eϕ ise modelde ϕ’nin do˘gru oldu˘gu bir d¨ unyanın varlı˘gını gösterir ve ϕ B ⊥ ¸seklinde ifade edilir [14]. KD45-O sistemi aksiyomatik olarak a¸sa˘gıdaki ¸sekilde tanımlanır: Tanım 2.2.6. KD45-O sistemi a¸sa˘gıda verilen aksiyom ve t¨ uretim kurallarından olu¸sur: (a) KD45 sisteminin aksiyomları (b) Sıralama aksiyomları Aksiyomlar: (i) ϕ <B ϕ (ii) (ϕ <B ψ) ∧ (ψ <B χ) → (ϕ <B χ) (iii) (ϕ B ψ) ↔ (ϕ <B ψ) ∧ ¬(ψ <B ϕ) (iv) (ϕ <B ψ) ∨ (ψ B ϕ) (v) (Bϕ ∧ ¬Bψ) → (ϕ B ψ) (vi) (ϕ <B ψ) → B(ϕ <B ψ) (vii) (ϕ B ψ) → B(ϕ B ψ) (viii) (⊥<B ¬(ϕ → ψ)) → (ψ <B ϕ) (ix) ϕ → (ϕ B ⊥) (x) (Bϕ B ⊥) → Bϕ T¨ uretim Kuralları: (R1) KD45 sisteminin t¨ uretim kuralları ϕ→ψ (R2) ψ<B ϕ 12.

(19) 2.2.4. ˙ Modal Modellerde Homomorfizma ve Izomorfizma. Bu böl¨ umde modal modeller arasındaki homomorfizma ve izomorfizma kavramlarını tanıtaca˘gız. Tanım 2.2.7. Bir S modal mantı˘gı i¸cin M = hS, R, V i ve M0 = hS 0 , R0 , V 0 i iki S model olsun. f : M → M0 fonksiyonu a¸sa˘gıdaki özellikleri sa˘glarsa bir homomorfizma olarak adlandırılır: (i) Her bir önerme de˘gi¸skeni p ve her s ∈ S i¸cin s ∈ V (p) ise f (s) ∈ V 0 ’d¨ ur. (ii) Her s, t ∈ S i¸cin (s, t) ∈ R ise (f (s), f (t)) ∈ R0 ’d¨ ur. Tanım 2.2.8. Bir S modal mantı˘gı i¸cin M = hS, R, V i ve M0 = hS 0 , R0 , V 0 i iki S model olsun. f : M → M0 fonksiyonu a¸sa˘gıdaki özellikleri sa˘glarsa bir kuvvetli homomorfizma olarak adlandırılır: (i) Her bir önerme de˘gi¸skeni p ve her s ∈ S i¸cin s ∈ V (p) olması i¸cin gerek ve yeter ko¸sul f (s) ∈ V 0 (p) olmasıdır. (ii) Her s, t ∈ S i¸cin (s, t) ∈ R olması i¸cin gerek ve yeter ko¸sul (f (s), f (t)) ∈ R0 olmasıdır. Tanım 2.2.9. Bijektif kuvvetli bir homomorfizmaya izomorfizma denir. M’den modelinden M0 ’n ye bir izomorfizma var ise M modeli M0 ’ye izomorftur denir ve M∼ = M0 ile gösterilir. ¨ Ornek 2.2.10. p ∈ P olmak u ¨zere, M = hN, <, V i ve M0 = hN − {0}, <, V 0 i modelleri a¸sa˘gıdaki gibi tanımlanmı¸s olsun. / •2. / •1. •0. p. M •1. p. modeli. / •2. / •3. p. M0. modeli. S¸ekil 2. M ve M0 modelleri Bu durumda f:. / •4 .... / •3. M → M0 n 7→ n + 1. ile tanımlı fonksiyonu bir izomorfizmadır. ˙ Ispat. (i) f fonksiyonu kuvvetli bir homomorfizmadır:. 13. / •4 ... p.

(20) – (⇒) : w ∈ V (p) olsun. Bu durumda bir n ∈ N i¸cin w = 2n + 1 ¸seklindedir. Buradan f (w) = w + 1 = 2n + 2 ∈ {2, 4, 6, ...} = V 0 (p) ¨ olur. Oylseyse f (w) ∈ V 0 ’d¨ ur. ¨ (⇐) : f (w) ∈ V 0 olsun. Oyleyse bir n ∈ N i¸cin f (w) = w + 1 = 2n ¸seklindedir. Buradan f (w) − 1 = w = 2n − 1 ∈ {1, 3, 5, ...} = V (p) elde edilir. O halde w ∈ V (p)’dir. – (⇒) : Her x, y ∈ N i¸cin x < y olsun. Bu durumda f (x) = x + 1 < y + 1 = f (y) olur. (⇐) : Her f (x), f (y) ∈ N − {0} i¸cin f (x) < f (y) olsun. Buradan f (x) = x + 1 < y + 1 = f (y)’dir. Bu durumda x + 1 − 1 < y + 1 − 1 yani x < y’dir. (ii) f fonksiyonu bijektiftir: – f bire birdir: f (x) = f (y) ⇒ x + 1 = y + 1 ⇒ x = y’dir. – f örtendir: E˘ger x ∈ N − {0} ise x − 1 ∈ N’dır. O halde her n ∈ N − {0} i¸cin ¨ y = n − 1 olacak ¸sekilde bir y ∈ N vardır. Oyleyse f o¨rtendir. . 14.

(21) ¨ lu ¨m 3 Bo S5EC ve KD45-O Modal Mantıkları i¸ cin Sa˘ glamlık Teoremleri 3.1. S5EC Modal Mantı˘ gında Sa˘ glamlık. Bu böl¨ umde S5EC ve KD45-O modal mantıklarının Tanım 2.1.16 ve Tanım 2.2.1’de verilen aksiyom sistemlerine göre sa˘glam oldukları kanıtlanacaktır. Herhangi bir modal mantı˘gın sa˘glamlık teoremi o mantıkta t¨ uretilebilir olan bir form¨ ul¨ un ge¸cerli oldu˘gunu ifade eder. Teorem 3.1.1. Herhangi bir ϕ form¨ ul¨ u i¸cin S5EC ` ϕ ⇒ S5EC |= ϕ’dir. ˙ ˙ Ispat. Ispat ϕ’nin t¨ uretiminin uzunlu˘gu u ¨zerinde t¨ umevarımla yapılır. Temel Adım: T¨ uretimin uzunlu˘gu n=1 olsun. Bu durumda ϕ bir aksiyomdur. Bu durumda KD45-O sistemindeki her bir aksiyomun ge¸cerli oldu˘gunu göstermeliyiz. M = hS, R1 , ...Rm , RE , RC , V i bir S5EC model, s ve t bu model u ¨zerinde herhangi iki durum olsun. (A1) ϕ form¨ ul¨ u bir totoloji olsun. Bu durumda |=P C ϕ’dir. Bununla birlikte, modal mantık önermeler mantı˘gını i¸cerdi˘ginden |= ϕ’dir. (A2) M, s |= Ki ϕ ve M, s |= Ki (ϕ → ψ) olsun. Bu durumda (s, t) ∈ Ri olan her ¨ ¨ t i¸cin M, t |= ϕ ve M, t |= ϕ → ψ. Oyleyse Onerme 2.1.5’ten (s, t) ∈ Ri olan her t i¸cin M, t |= ψ. Buradan M, s |= Ki ψ’dir. (A3) M, s |= Ki ϕ olsun. Bu durumda (s, t) ∈ Ri olan her t durumu i¸cin M, t |= ϕ’dir. Ri ba˘gıntısı yansımalı oldu˘gundan t durumu s olarak se¸cilirse M, s |= ϕ olur.. 15.

(22) ¨ (A4) M, s |= ¬Ki ϕ olsun. Oyleyse bir t ∈ S vardır oÿle ki (s, t) ∈ Ri ve M, t |= ¬ϕ’dir. M, s |= Ki ¬Ki ϕ yani (s, t0 ) ∈ Ri ¸seklindeki her t0 ∈ S i¸cin M, t0 |= ¬Kϕ oldu˘gunu göstermeliyiz. Bunun i¸cin (s, t0 ) ∈ Ri olsun. Ri ba˘gıntısı aynı zamanda simetrik oldu˘gundan (t0 , s) ∈ Ri ’dir. Bu durumda Ri ba˘gıntısının ge¸ci¸slilik özelli˘ginden (t0 , t) ∈ Ri olur. M, t |= ¬ϕ oldu˘gundan M, t0 |= ¬Kϕ olur. (A5) M, s |= ¬Ki ϕ olsun. Bu durumda (s, t) ∈ Ri olacak ¸sekilde bir t vardır oÿle ki M, t |= ¬ϕ. M’de keyfi bir u durumu alalım öyle ki (s, u) ∈ Ri olsun. (s, t) ∈ Ri ve Ri bir denklik ba˘gıntısı oldu˘gundan (u, t) ∈ Ri ’dir. M, t |= ¬ϕ oldu˘gu i¸cin M, u 2 ¬Ki ϕ. u, keyfi se¸cildi˘gi i¸cin M, s |= Ki ¬Ki ϕ. (A6) (⇒) : M, s |= Eϕ ve M, s 2 (K1 ϕ ∧ ... ∧ Km ϕ) olsun. Bu durumda en az bir i ≤ m i¸cin M, s 2 Ki ϕ’dir. O halde bir u ∈ S vardır oÿle ki (s, u) ∈ Ri ve M, u |= ¬ϕ’dir. (s, u) ∈ Ri oldu˘gundan s → u elde edilir. Buradan ise M, s 2 Eϕ olur ki bu bir ¸celi¸skidir. (⇐) : M, s |= (K1 ϕ ∧ ... ∧ Km ϕ) ve s → t olacak ¸sekilde bir t durumunu ele alalım. Bunun anlamı (s, t) ∈ R1 ∪ ... ∪ Rm , bu nedenle bazı i ≤ m’ler i¸cin (s, t) ∈ Ri . M, s |= Ki ϕ oldu˘gundan M, t |= ϕ. Bundan dolayı M, s |= Eϕ olur. (A7) M, s |= Cϕ. Buradan s t koiulu sa˘glayan her t i¸cin M, t |= ϕ. Bununla birlikte s → s oldu˘gundan s s’yi elde ederiz. Bu nedenle M, s |= ϕ. (A8) M, s |= Cϕ olsun. S¸u halde s t ko¸sulu sa˘glayan her t i¸cin M, t |= ϕ. s → u ¨ ve u v olacak ¸sekilde u, v ∈ S durumlarını ele alalım. Oyleyse s v olacak ¸sekilde bir ba˘gıntı vardır ve M, s |= Cϕ oldu˘gundan M, v |= ϕ’dir. Bununla birlikte u v oldu˘gundan ve v keyfi se¸cildi˘ginden M, u |= Cϕ. Buradan da M, s |= ECϕ’yi elde ederiz. (A9) M, s |= Cϕ∧C(ϕ → ψ) olsun. M, s |= Cψ yani s t ko¸sulunu sa˘glayan her t i¸cin M, t |= ψ oldu˘gunu göstermeliyiz. s t olsun. S¸u halde M, s |= Cϕ oldu˘gundan M, t |= ϕ ve yine M, s |= C(ϕ → ψ) oldu˘gundan M, t |= (ϕ → ¨ ψ)’dir. Onerme 2.1.5’ten M, t |= ψ’dir.. 16.

(23) (A10) M, s |= C(ϕ → Eϕ) ve M, s |= ϕ olsun. Göstermemiz gereken M, s |= Cϕ yani s t olan her t i¸cin M, t |= ϕ. s →k t olan b¨ ut¨ un t’ler i¸cin M, t |= ϕ’yi sa˘glayan her k ≥ 0 i¸cin k u ¨zerinde t¨ umevarımla göstermemiz yeterlidir. Temel adım olarak k=0 i¸cin a¸cıktır çu ¨nk¨ u bu durumda t, s’nin kendisidir ve M, s |= ϕ’dir. Her k < n i¸cin iddia do˘gru olsun. k = n i¸cin iddiayı ¨ ispatlayalım. t bir durum olsun oÿle ki s →n t olsun. Oyleyse bir u durumu vardır oÿle ki s →n−1 u → t. T¨ umevarım hipotezinden M, u |= ϕ. Ayrıca s u oldu˘gundan M, u |= ϕ → Eϕ. Buradan M, u |= Eϕ’dir yani u → v ¨ olan her v i¸cin M, v |= ϕ’dir. Ozellikle v, t olarak se¸cilirse M, t |= ϕ’dir. T¨ umevarım Hipotezi: Teorem t¨ uretimin uzunlu˘gu n i¸cin do˘gru olsun. T¨ umevarım Adımı: T¨ uretimin uzunlu˘gu n+1 olsun. Ge¸cerlili˘gin, t¨ uretimin uzunlu˘gu n+1 oldu˘gunda korundu˘gunu göstermeliyiz. (R1) ϕ form¨ ul¨ u MP ile n+1 adımda elde edilmi¸s olsun. Bu durumda ψ → ϕ ve ψ form¨ ulleri vardır öyle ki bu form¨ ullerin t¨ uretimlerinin uzunlu˘gu n’dir. ¨ T¨ umevarım hipotezinden, |= ψ ve |= ψ → ϕ elde edilir. Onerme 2.1.5’ten M, s |= ϕ elde edilir. M ve s keyfi olduklarından |= ϕ’dir. ¨ (R2) ϕ ` Ki ϕ olsun. Oylseyse ϕ form¨ ul¨ un¨ un t¨ uretiminin uzunlu˘gu n’dir ve t¨ umevarım hipotezinden |= ϕ olur. Buradan M, s |= ϕ’dir. (s, t) ∈ Ri olsun. |= ϕ oldu˘gundan M, t |= ϕ’dir. S¸u halde t keyfi se¸cildi˘ginden M, s |= Ki ϕ’dir. ¨ (R3) ϕ ` Ki ϕ olsun. Oylseyse ϕ form¨ ul¨ un¨ un t¨ uretiminin uzunlu˘gu n’dir ve t¨ umevarım hipotezinden |= ϕ olur. Bu durumda M, s |= ϕ’dir. (s, t) ∈ RC olsun. ¨ |= ϕ oldu˘gundan M, t |= ϕ’dir. Oyleyse M, s |= Ci ϕ’dir. . 3.2. KD45-O Modal Mantı˘ gında Sa˘ glamlık. Teorem 3.2.1. ϕ herhangi bir KD45-O form¨ ul olmak u ¨zere `KD45−O ϕ ⇒|=KD45−O ϕ. ˙ ˙ Ispat. Ispat ϕ’nin t¨ uretiminin uzunlu˘gu u ¨zerinde t¨ umevarımla yapılır.. 17.

(24) Temel Adım: T¨ uretimin uzunlu˘gu n=1 olsun. Bu durumda ϕ ya bir aksiyomdur ya da bir totolojidir. ϕ bir totoloji ise her model altında do˘grudur yani |= ϕ’dir. ϕ bir aksiyom ise KD45-O sistemindeki her bir aksiyomun ge¸cerli oldu˘gunu göstermeliyiz. M = hS, ≤, ≥B , V i bir KD45-O model ve s bu model u ¨zerinde bir durum olsun. (a) KD45 aksiyomları • (M, s) |= Bi ϕ ve (M, s) |= Bi (ϕ → ψ) olsun. S¸u halde ≤ ba˘gıntısına göre her minimal t i¸cin (M, t) |= ϕ ve (M, t) |= ϕ → ψ’dir. Buradan (M, t) |= ψ yani (M, s) |= Bi ψ. ¨ • (M, s) |= B ⊥ olsun. Oyleyse ≤ ba˘gıntısına göre her minimal t i¸cin (M, t) |=⊥ olur. Fakat böyle bir t bulunmadı˘gından (M, s) 2 B ⊥’dir. • (M, s) |= Bϕ olsun. S¸u halde ≤ ba˘gıntısına göre her minimal t i¸cin (M, t) |= ¨ ϕ’dir. Buradan her k ∈ S i¸cin (M, k) |= Bϕ’dir. Ozel olarak bu k’ler merkezdeki durumlardan se¸cilirse (M, s) |= BBϕ olur. • (M, s) |= ¬B¬Bϕ ⇒ (M, s) 2B¬Bϕ ⇒ (M, t) |= ¬Bϕ, ≤ ba˘gıntısına göre en az bir t i¸cin ⇒ (M, t) 2Bϕ ⇒ (M, t0 )2 ϕ, ≤ ba˘gıntısına göre en az bir t0 i¸cin ⇒ (M, s) |= ¬Bϕ (b) Sıralama aksiyomları (i) {t | (M, t) |= ϕ} ≥B {t | (M, t) |= ϕ}. Her iki k¨ ume birbirine e¸sit oldu˘gundan makull¨ ukleri de e¸sittir. S¸u halde (M, s) |= ϕ <B ϕ’dir. (ii) (M, s) |= (ϕ <B ψ) ∧ (ψ <B σ) olsun. Bu durumda {t | (M, t) |= ϕ} ≥B {t | (M, t) |= ψ} ve {t | (M, t) |= ψ} ≥B {t | (M, t) |= σ}’dır. Buradan ≥B ba˘gıntısı ge¸ci¸sli oldu˘gundan {t | (M, t) |= ϕ} ≥B {t | (M, t) |= σ} yani (M, s) |= ϕ <B σ elde edilir.. 18.

(25) (iii) (⇐) : (M, s) |= (ϕ <B ψ)∧¬(ψ <B ϕ) ve (M, s) 2 (ϕ B ψ) olsun. Buradan (M, s) |= ¬(ϕ B ψ)’dir yani bir w ∈ {t | (M, t) |= ψ} vardır öyle ki her w0 ∈ {t | (M, t) |= ϕ} i¸cin w ≤ w0 ’d¨ ur. Bu ise (M, s) |= ¬(ψ <B ϕ) olması ile bir ¸celi¸skidir. O halde (M, s) |= (ϕ <B ψ)∧¬(ψ <B ϕ) → ¬(ϕ B ψ)’dir. (⇒) : (M, s) |= (ϕ B ψ) ve (M, s) 2 (ϕ <B ψ) ∧ ¬(ψ <B ϕ) olsun. Bu durumda (M, s) |= ¬(ϕ <B ψ) ∨ (M, s) |= (ψ <B ϕ)’dir. • Durum 1. (M, s) |= ¬(ϕ <B ψ) ise bir w ∈ {t | (M, t) |= ψ} vardır öyle ki her w0 ∈ {t | (M, t) |= ϕ} i¸cin w < w0 ’d¨ ur. Bu ise (M, s) |= (ϕ B ψ) olması ile bir ¸celi¸skidir. • Durum 2. (M, s) |= (ψ <B ϕ) ise bir w ∈ {t | (M, t) |= ψ} vardır öyle ki her w0 ∈ {t | (M, t) |= ϕ} i¸cin w ≤ w0 ’d¨ ur. Bu ise (M, s) |= (ϕ B ψ) olması ile bir ¸celi¸skidir. O halde (M, s) |= (ϕ B ψ) → (ϕ <B ψ) ∧ ¬(ψ <B ϕ) elde edilir. (iv) (M, s) |= ¬(ϕ <B ψ) ve (M, s) |= ¬(ψ B ϕ) olsun. (M, s) |= ¬(ϕ <B ψ) ise bir w1 ∈ S vardır öyle ki w1 ∈ {t | (M, t) |= ψ} ve her w0 ∈ {t | (M, t) |= ϕ} i¸cin w1 < w0 ’d¨ ur. Bununla birlikte (M, s) |= ¬(ψ B ϕ) oldu˘gundan bir w2 ∈ S vardır oÿle ki w2 ∈ {t | (M, t) |= ϕ} ve her w00 ∈ {t | (M, t) |= ψ} ¨ i¸cin w2 ≤ w00 ’d¨ ur. Ozel olarak w00 , w1 olarak se¸cilirse bu durum w1 < w0 ile bir ¸celi¸skidir. O halde (M, s) |= (ϕ <B ψ) ∨ (ψ B ϕ)’dir. (v) (M, s) |= Bϕ ∧ ¬Bψ olsun. (M, s) |= ¬Bψ ise ≤ ba˘gıntısına göre en az bir minimal t i¸cin (M, t) 2 ψ’dir. (M, s) |= Bϕ ise ≤ ba˘gıntısına göre her minimal t i¸cin (M, t) |= ϕ. Böylece {t | (M, t) |= ϕ} >B {t | (M, t) |= ψ} oldu˘gundan |= ϕ B ψ. (vi) (M, s) |= ϕ <B ψ ve (M, s) 2 B(ϕ <B ψ) olsun. Bu durumda ≤ ba˘gıntısına göre en az bir minimal t i¸cin (M, t) 2 ϕ <B ψ’dir. Bu durumda bir w1 durumu vardır oÿle ki w1 ∈ {t | (M, t) |= ψ} ve her w2 ∈ {t | (M, t) |= ψ} i¸cin w1 < w2 ’dir. Bu ise (M, s) |= φ <B ψ olması ile ¸celi¸skidir. O halde (M, s) |= B(ϕ <B ψ)’dir.. 19.

(26) (vii) (M, s) |= φ B ψ ve (M, s) 2 B(ϕ B ψ) olsun. Bu durumda ≤ ba˘gıntısına göre en az bir minimal t i¸cin (M, t) 2 ϕ B ψ’dir. Bu durumda bir w1 durumu vardır oÿle ki w1 ∈ {t | (M, t) |= ψ} ve her w2 ∈ {t | (M, t) |= ψ} i¸cin w1 ≤ w2 ’dir. Bu ise (M, s) |= φ B ψ olması ile ¸celi¸skidir. O halde (M, s) |= B(ϕ B ψ)’dir. (viii) (M, s) |=⊥<B ¬(ϕ → ψ) ⇒ (M, s) |= U (ϕ → ψ) ⇒ ∀t ∈ S((M, t) |= (ϕ → ψ)) ⇒ ∀t ∈ S((M, t) |= ϕ ⇒ ((M, t) |= ψ) ⇒ ∀t ∈ S({t | ((M, t) |= ϕ} ⊆ {t | ((M, t) |= ψ}) ⇒ (M, s) |= ψ <B ϕ (ix) (M, s) |= ϕ. Buradan {t | (M, t) |=⊥} = ∅ oldu˘gundan {t | (M, t) |= ϕ} >B {t | (M, s) |=⊥} yani (M, s) |= ϕ B ⊥ elde edilir. (x) (M, s) |= ¬U ¬Bϕ ⇒ (M, s) 2 U ¬Bϕ ⇒ ∃t ∈ S, (M, t) 2 ¬Bϕ ⇒ ∃t ∈ S, (M, t) |= Bϕ ⇒ Her ≤ minimal t0 i¸cin, (M, t0 ) |= ϕ ⇒ (M, s) |= Bϕ. T¨ umevarım Hipotezi: Teorem t¨ uretimin uzunlu˘gu n i¸cin do˘gru olsun. T¨ umevarım Adımı: T¨ uretimin uzunlu˘gu n+1 olsun. Ge¸cerlili˘gin, t¨ uretimin uzunlu˘gu n+1 oldu˘gunda korundu˘gunu göstermeliyiz. (R1) ϕ form¨ ul¨ u MP ile n+1 adımda elde edilmi¸s olsun. Bu durumda ψ → ϕ ve ψ form¨ ulleri vardır öyle ki bu form¨ ullerin t¨ uretimlerinin uzunlu˘gu n’dir. ¨ T¨ umevarım hipotezinden, |= ψ ve |= ψ → ϕ elde edilir. Onerme 2.1.5’ten (M, s) |= ϕ elde edilir. M ve s keyfi olduklarından |= ϕ’dir. ¨ (R2) Bi ϕ form¨ ul¨ un¨ un t¨ uretiminin uzunlu˘gu n+1 olsun. Oylseyse ϕ form¨ ul¨ un¨ un t¨ uretiminin uzunlu˘gu n’dir ve t¨ umevarım hipotezinden |= ϕ olur. Buradan (M, s) |= ϕ’dir. Bununla birlikte ≤ ba˘gıntısına göre her minimal t i¸cin 20.

(27) (M.t) |= ϕ’dir. Buradan (M, s) |= Bi ϕ olur. O halde s keyfi se¸cildi˘ginden |= Bi ϕ’dir. ¨ (R3) ϕ → ψ `n+1 ψ <B ϕ olsun. Oylseyse ϕ → ψ form¨ ul¨ un¨ un t¨ uretiminin uzunlu˘gu n’dir ve t¨ umevarım hipotezinden |= ϕ → ψ olur. Bu durumda M, s |= ϕ → ψ’dir. Buradan {t | (M, t) |= ϕ} ⊆ {t | (M, t) |= ψ}’dir. ¨ Tanım 2.2.3 (ii)’den {t | (M, t) |= ψ} ≥B {t | (M, t) |= ϕ} olur. Oyleyse |= ψ <B ϕ elde edilir. . 21.

(28) ¨ lu ¨m 4 Bo S5EC ve KD45-O Modal Mantıkları i¸ cin Tamlık Teoremleri Bu böl¨ umde S5EC ve KD45-O sistemlerinin, Tanım 2.1.16 ve Tanım 2.2.1’de verilen aksiyom sistemlerine göre tam oldu˘gu ispatlanacaktır. Tamlık teoremleri bir mantıkta ger¸ceklenebilen form¨ ullerin t¨ uretiminin var oldu˘gunu gösteren teoremlerdir. Bununla birlikte ispatları ise model olu¸sturmaya dayalıdırlar. Bu modelleri olu¸sturmanın farklı yöntemleri vardır. Burada ise bu modelleri olu¸sturmanın u ¨¸c farklı yöntemi verilecektir: Kanonik model, sonlu Henkin yöntemi ve filtreleme yöntemi. Bu böl¨ umdeki t¨ um bilgiler [1], [2], [10] ve [5]’te de bulunabilir.. 4.1. Kanonik Model. Bu böl¨ umde maksimal tutarlı form¨ ul k¨ umelerinde model olu¸sturma yöntemi olan kanonik model yöntemi anlatılacaktır. Tanım 4.1.1. S bir modal mantık, ϕ bir S form¨ ul ve Γ bir form¨ ul k¨ umesi olmak u ¨zere, (i) 0S ¬ϕ ise ϕ form¨ ul¨ u S-tutarlıdır. (ii) Ψ = {ϕ1 , ..., ϕn } sonlu bir k¨ ume olmak u ¨zere e˘ger ϕ1 ∧ ... ∧ ϕn tutarlı ise Ψ k¨ umesi tutarlıdır. (iii) Sonlu olmayan epistemik form¨ uller k¨ umesi ϕ i¸cin e˘ger ϕ’nin her sonlu alt k¨ umesi tutarlı ise ϕ de tutarlıdır. (iv) E˘ger Γ 0S ⊥ ise Γ form¨ ul k¨ umesine S-tutarlıdır denir. Aksi halde, S-tutarsızdır denir. Tanım 4.1.2. Bir Γ form¨ uller k¨ umesinin maksimal S-tutarlı olması i¸cin gerek ve yeter ko¸sul (a) Γ k¨ umesinin S-tutarlı, 22.

(29) (b) Γ ⊆ Γ0 ve Γ0 tutarlı ise Γ = Γ0 olmasıdır. Lemma 4.1.3. Γ, maksimal S-tutarlı form¨ ul k¨ umesi olmak u ¨zere, (i) Her ϕ form¨ ul¨ u i¸cin, ϕ ∈ Γ veya ¬ϕ ∈ Γ’dır, (ii) ϕ ve ϕ → ψ ∈ Γ ise ψ ∈ Γ’dır, (iii) `S ϕ ise ϕ ∈ Γ’dır. (iv) ϕ ∧ ψ ∈ Γ olması i¸cin g.y.k. ϕ ∈ Γ ve ψ ∈ Γ olmasıdır, ˙ Ispat. (i) ϕ ∈ / Γ ve ¬ϕ ∈ / Γ olsun. Bu durumda maksimallik tanımı gere˘gi Γ ∪ {ϕ} ve ¨ Γ∪{¬ϕ} S-tutarsıdır. Oyleyse tanım 4.1.1 (iii)’den Γ’nın sonlu alt k¨ umeleri Γ0 , Γ00 vardır oÿle ki Γ0 ∪{ϕ} ve Γ00 ∪{¬ϕ} S-tutarsızdır. Γ0 ∪Γ00 = {ψ1 , ..., ψn } ve Ψ = ψ1 ∧ ...∧m olsun. Bu durumda tanım 4.1.1 (ii)’den ` ¬(Ψ ∧ ϕ ∧ ¬ϕ) olur. Buradan ` ¬Ψ ∨ ¬ϕ ∨ ϕ elde edilir. ϕ ∨ ¬ϕ totoloji oldu˘gundan ` ¬Ψ elde edilir ki bu ise {ψ1 , ..., ψn } k¨ umesinin S-tutarsız oldu˘gunu gösterir. Bu ise Γ’nın tutarlı olması ile bir ¸celi¸skidir. (ii) ϕ, ϕ → ψ ∈ Γ ve ψ ∈ / Γ olsun. Bu durumda Γ’nın sonlu bir alt k¨ umesi Γ0 vardır oÿle ki Γ0 ∪ {ψ}, S-tutarsızdır. Γ0 = {ψ1 , ..., ψn } ve Ψ = ψ1 ∧ ...∧m ¨ olsun. Oyleyse ` ¬(Ψ ∧ ψ)’dir. Γ0 ∪ {ϕ} ∪ {ϕ → ψ} `P C Ψ ∧ ψ oldu˘gundan Γ0 ∪ {ϕ} ∪ {ϕ → ψ} k¨ umesi S tutarsızdır bu ise Γ’nın S tutarlılı˘gı ile bir ¸celi¸skidir. (iii) ϕ ∈ / Γ olsun. Bu durumda (i)’den ¬ϕ ∈ Γ ’dır. T¨ uretim tanımından Γ ` ¬ϕ olur. O halde Γ `P C ϕ ∧ ¬ϕ’dir. Buradan Γ `⊥ olur ki bu Γ’nın tutarlılı˘gı ile bir çeli¸skidir. (iv) (⇒) : ϕ ∧ ψ ∈ Γ olsun. Bu durumda Γ ` ϕ ∧ ψ’dir. Buradan Γ `P C ϕ ve Γ `P C ψ elde edilir. (iii)’den ϕ ∈ Γ ve ψ ∈ Γ’dır. (⇐) : ϕ ∈ Γ ve ψ ∈ Γ olsun. T¨ uretim tanımından Γ `P C ϕ ve Γ `P C ψ olur. Buradan Γ ` ϕ ∧ ψ’dir. (iii)’den ϕ ∧ ψ ∈ Γ’dır. Tanım 4.1.4. S modal mantı˘gı i¸cin kanonik model MS = hWS , RS , VS i a¸sa˘gıdaki ¸sekilde tanımlanır: 23.

(30) (i) WS = {Γ | Γ maksimal S tutarlı form¨ ul k¨ umesi }, (ii) RS = {hΓ, Γ0 i | ϕ ∈ Γ ise ϕ ∈ Γ0 ’d¨ ur}, (iii) VS (p) = {Γ ∈ WS | p ∈ Γ}. Lemma 4.1.5. (Lindenbaum) Γ, S tutarlı form¨ uller k¨ umesi olsun. Bu durumda maksimal S-tutarlı bir Γ0 k¨ umesi vardır öyle ki Γ ⊆ Γ0 dır. ˙ Ispat. Γ’nın maksimal S-tutarlı bir geni¸slemesi Γ0 oldu˘gunu göstermeliyiz. Γ’nın S-tutarlı ve dilin form¨ ullerinin ϕ1 , ϕ2 , ... ¸seklinde numaralandırıldı˘gını varsayalım. Γ0 a¸sa˘gıdaki ¸sekilde tanımlanır: Γ0 = Γ   . Γn+1 =   Γ0 =. S. n>0. Γn ∪ {ϕn }. e˘ger Γn ∪ {ϕn }, S tutarlıysa. Γn ∪ {¬ϕn } di˘ger hallerde. Γn. S¸imdi Γ0 ’n¨ un maksimal ve S-tutarlı oldu˘gunu gösterelim. Γ0 , S-tutarlıdır: Γ0 , S-tutarlı olmasın. S¸u halde Γ0 ’nın tutarlı olmayan bir Ψ alt k¨ umesi vardır öyle ki bir n i¸cin Ψ ⊆ Γn ’dir. Fakat her Γn , S-tutarlı oldu˘gu i¸cin bu bir ¸celi¸skidir. O halde Γ0 S-tutarlıdır. Γ0 maksimaldir: Keyfi bir ϕn form¨ ul olsun oÿle ki ϕn ∈ / Γ0 . S¸u halde aynı zamanda ϕn ∈ / Γn ’dir. Γn ∪ {ϕn } tutarsız oldu˘gundan Γ0 ∪ {ϕn } de tutarsıdır. O halde Γ0 ’n¨ un S-tutarlı bir geni¸slemesi yoktur. Buradan Γ0 ’n¨ un maksimal oldu˘gu elde edilir.. . Lemma 4.1.6. (Truth) MS = hWS , RS , VS i modeli, S modal mantı˘gı i¸cin kanonik model olsun. Her ϕ form¨ ul¨ u ve Γ ∈ WS i¸cin ϕ ∈ Γ ⇔ MS , Γ |= ϕ. ˙ ˙ Ispat. Ispat ϕ form¨ ul¨ un¨ un karma¸sıklı˘gı u ¨zerinde t¨ umevarımla yapılır. • ϕ : p olsun. (⇒) : p ∈ Γ ise tanım 4.1.5 (iii)’den Γ ∈ VS (p)’dir. Model olma tanımından M, Γ |= p’dir. (⇐) : ¬p ∈ Γ olsun. Bu durumda tanım 4.1.5 (iii)’den M, Γ |= ¬p olur. Buradan M, Γ 2 p’dir. 24.

(31) • ϕ : ¬ψ ve lemma ψ i¸cin do˘gru olsun. ¬ψ ∈ Γ ⇔ Γ maksimal tutarlı oldu˘gundan, ψ ∈ /Γ⇔ T¨ umevarım hipotezinden, M, Γ 2 ψ ⇔ M, Γ |= ¬ψ’dir. • ϕ : ψ1 ∧ ψ2 ve lemma ψ1 ve ψ2 i¸cin do˘gru olsun. ψ1 ∧ ψ2 ∈ Γ ⇔ ψ1 ∈ Γ ∧ ψ2 ∈ Γ ⇔ T¨ umevarım hipoezinden, M, Γ |= ψ1 ∧ M, Γ |= ψ2 ⇔ M, Γ |= ψ1 ∧ ψ2 ’dir. • ϕ : ψ ve lemma ψ i¸cin do˘gru olsun. (⇒): ψ ∈ Γ ve hΓ, Γ0 i ∈ RS olacak ¸sekilde keyfi bir Γ0 ∈ WS ele alalım. RS ba˘gıntısının tanımından ψ ∈ Γ0 elde edilir. T¨ umevarım hipotezinden M, Γ0 |= ψ’dir. Γ0 keyfi bir durum oldu˘gundan M, Γ |= ψ elde edilir. (⇐): M, Γ |= ψ olsun. P = {α | α ∈ Γ} ∪ {¬ψ} k¨ umesinin tutarsız oldu˘gunu gösterelim. P ∪ {¬α} k¨ umesi tutarlı olsun. O halde bu k¨ umenin maksimal bir geni¸slemesi P 0 vardır ve ¬ψ ∈ P 0 ’d¨ ur. Bununla birlikte P’nin tanımından hΓ, P 0 i ∈ RS ’dir. ¬ψ ∈ P 0 oldu˘gundan t¨ umevarım hipoteziyle M, P 0 |= ¬ψ elde edilir. Buradan M, Γ |= ¬ψ olur. Bu ise bir ¸celi¸skidir. O halde P {α | α ∈ Γ} ∪ {¬ψ} k¨ umesi tutarsızdır. S¸u halde ϕ1 , ..., ϕn ∈ P olmak u ¨zere P ∪ {¬ψ} k¨ umesinin bir alt k¨ umesi vardır oÿle ki ϕ1 , ..., ϕk , ¬ψ tutarsızdır. Buradan ` ¬(ϕ1 ∧ ... ∧ ϕk ∧ ¬ψ) elde ¨ edilir. Oyleyse ` (ϕ1 → ϕ2 → (....(ϕk → ψ)...))’dir. (1) ϕ2 → (....(ϕk → ψ)...) ifadesini σ ile gösterelim. ` (ϕ1 → σ) ` (ϕ1 → σ) K aksiyomundan ` ϕ1 → σ olur. 25.

(32) Γ k¨ umesi maksimal tutarlı oldu˘gundan b¨ ut¨ un totolojileri i¸cerir: ϕ1 → σ ∈ Γ’dır. ϕ1 ∈ Γ oldu˘gundan σ ∈ Γ’dır. Bu i¸slem k defa tekrarlanırsa ψ ∈ Γ elde edilir. Teorem 4.1.7. Herhangi bir modal mantık S, kanonik modeli MS ’ye göre tamdır. ˙ Ispat. ϕ, S’de tutarlı bir form¨ ul olsun. Bu durumda Γ = {ϕ} k¨ umesi de tutarlıdır. Buradan, Lindenbaum lemması ile Γ ⊆ Γ0 olacak ¸sekilde maksimal tutarlı bir Γ0 k¨ umesinin oldu˘gu elde edilir. Truth lemmasından, S’deki her ψ form¨ ul¨ u i¸cin ¨ Mbf S , Γ0 |= ψ’dir. Ozel olarak bu ψ’ler Γ’dan se¸cilirse MS , Γ0 |= Γ yani MS , Γ0 |= ϕ olur.. . 4.1.1. S5EC’nin Kanonik Modeli. c c Tanım 4.1.8. S5EC mantı˘gının kanonik modeli Mc = hS c , R1c , ..., Rm , RE , RCc , V c i modeli a¸sa˘gıdaki gibi tanımlanır:. (i) S c = {Γ | Γ maksimal tutarlı form¨ ul k¨ umesi }, (ii) Ric ={(Γ, Γ0 ) | Γ/Ki ⊆ Γ0 }, RE c = {(Γ, Γ0 ) | Γ/EB ⊆ Γ0 }, RC c = {(Γ, Γ0 ) | Γ/CB ⊆ Γ0 }, (iii) V (p) = {Γ ∈ Γ | p ∈ Γ}. Burada Γ/Ki = {ϕ | Ki ϕ ∈ Γ}, Γ/E = {ϕ | Eϕ ∈ Γ} ve Γ/C = {ϕ | Cϕ ∈ Γ}’dir. c Teorem 4.1.9. S5EC’nin kanonik modeli Mc = hS c , R1c , ..., Rm , RE c , RC c , V c i a¸sa˘gıdaki özellikleri sa˘glar:. (i) Ric bir denklik ba˘gıntısıdır. c (ii) RE c = R1c ∪ ... ∪ Rm. (iii) (RE c )∗ ⊆ RC c ˙ Ispat. (i) Ric ’nin bir denklik ba˘gıntısı oldu˘gunu göstermek i¸cin yansımalı ve o¨klidyen oldu˘gunu göstermek yeterlidir. 26.

(33) (a) Ric yansımalıdır : (Γ, Γ0 ) ∈ Ric olsun. (A3): Ki ϕ → ϕ ∈ Γ’dan e˘ger ϕ ∈ Γ/Ki ise ϕ ∈ Γ’dır. Γ maksimal tutarlı ve modus ponens altında kapalı oldu˘gundan: Ki ϕ ∈ Γ ve Ki ϕ → ϕ ∈ Γ ise ϕ ∈ Γ. Bu nedenle Γ/Ki ⊆ Γ, yani (Γ, Γ) ∈ Ric ’dir. (b) Ric o¨klidyendir: (Θ, Ψ), (Θ, Σ) ∈ Ric ve ϕ ∈ Ψ/Ki olsun. ϕ ∈ Σ oldu˘gunu göstermemiz gerekir. Tersini varsayalım. ϕ ∈ Σ olmasın. θ/Ki ⊆ Σ oldu˘gundan ϕ ∈ / Θ/Ki ’dir. Ba¸ska bir ifadeyle Ki ϕ ∈ / Θ’dır. Θ maksimal tutarlı oldu˘gundan ¬Ki ϕ’dir. (A5) aksiyomu ve modus ponensten Ki ¬Ki ϕ ∈ Θ’dır. Son olarak Θ/Ki ⊆ Ψ’den ¬Ki ϕ ∈ Ψ elde edilir ki bu ise ψ’nin tutatlılı˘gı ile çeli¸sir. O halde (Θ, Ψ) ∈ Ric ’dir yani, Ric o¨klidyendir. (ii) RE c ⊆ R1c ∪ ... ∪ Rmc ve R1c ∪ ... ∪ Rmc ⊆ RE c oldu˘gu göstermeliyiz. (⊆) (Θ, Ψ) ∈ RE c ve bazı 1 ≤ i ≤ m i¸cin (Θ, Ψ) ∈ / Ric olsun. S¸u halde her 1 ≤ i ≤ m i¸cin ϕ ∈ Θ/Ki ve ϕ ∈ / Ψ ko¸sullarını sa˘glayan bir ϕ vardır. Bu nedenle her i i¸cin Ki ϕ ∈ Θ’dır ve Ψ’nin maksimal tutarlılı˘gından ¬ϕi ∈ ¨ Ψ’dir. Oyleyse ¬ϕ1 ∧ ... ∧ ¬ϕm ∈ Ψ’dir. ϕ = ϕ1 ∨ ... ∨ ϕm olsun. ` ϕi → ϕ oldu˘gundan ` Ki (ϕi → ϕ)’dir. K aksiyomundan ` Ki ϕi → Ki ϕ’dir. Θ maksimal tutarlı oldu˘gundan Ki ϕi → Ki ϕ ∈ Θ, buradan da her i i¸cin Ki ϕ ∈ Θ’dır. Böylece K1 ϕ ∧ ...Km ϕ ∈ Θ oldu˘gundan (A6) aksiyomu gere˘gi Eϕ ∈ Θ’dır. Bu sonu¸ctan ϕ ∈ Θ/E ⊆ Ψ elde edilir. Ayrıca ¬ϕ1 ∧ ... ∧ ¬ϕm ∈ Ψ oldu˘gundan ¬ϕ ∈ Ψ’dir. Bu bir çeli¸skidir. S¸u halde bazı i’ler i¸cin (Θ, Ψ) ∈ Ric ’dir. ¨ (⊇) (Θ, Ψ) ∈ R1c ∪ ... ∪ Rmc olsun. Oyleyse bazı j’ler i¸cin (Θ, Ψ) ∈ Rj c ’dir. ¨ ϕ ∈ Θ/E olsun. (A6) aksiyomundan her i i¸cin Ki ϕ ∈ Θ’dır.Ozellikle Kj ϕ ∈ Θ ve bu nedenle Θ/Kj ⊆ Ψ. O halde Θ/E ⊆ Ψ’dir. (iii) (Θ, Ψ) ∈ (RE c )∗ olsun. (Θ, Ψ) ∈ RC c oldu˘gunu göstermeliyiz. S¸u halde Θ = Γ0 , ..., Γn = Ψ dizisi vardır öyle ki (Γi , Γi+1 ) ∈ RE c ’dir. ϕ ∈ Θ/C olsun. (A8) aksiyomundan ECϕ ∈ Θ = Γ0 ’dır. Buradan Cϕ ∈ Γ0 /E ⊆ Γ1 elde edilir. Bu i¸slemi n-1 defa tekrarlarsak Cϕ ∈ Γn = ψ’yi elde ederiz. S¸u halde ϕ ∈ ψ’dir. 27.

(34) Burada (RE c )∗ = RC c olmadı˘gı i¸cin elde edilen model bir yarı-S5EC modeldir.. 4.1.2. KD45-O’nun Kanonik Modeli. Tanım 4.1.10. KD45-O mantı˘gının kanonik modeli Mc = hS c , RB , RU , V c i a¸sa˘gıdaki ¸sekilde tanımlanır: (i) S c = {Γ | Γ maksimal KD45-O tutarlı }, (ii) RB = {(Γ, Γ0 ) | Bϕ ∈ Γ ⇒ ϕ ∈ Γ0 }, RU = {(Γ, Γ0 ) | U ϕ ∈ Γ ⇒ ϕ ∈ Γ0 } (iii) V c (p) = {Γ | p ∈ Γ}. Tanım 4.1.10 (ii)’de verilen RU ba˘gıntısı b¨ ut¨ un d¨ unyalar arasında tanımlı olmadı˘gından bir evrensel ba˘gıntı de˘gildir. Dolayısıyla elde edilen kanonik model, KD45-O model olma o¨zelliklerini sa˘glamak i¸cin yetersiz kalır. Bu nedenle hem S5EC hem de KD45-O modal mantıkları i¸cin kanonik modeller de˘gi¸stirilerek bu modellerin ba¸ska bir bi¸cimleri olu¸sturulacaktır. Bu yeni modelleri elde etmek i¸cin [1], [2] ve [10]’dan yararlanılacaktır.. 4.2. ¨ Sonlu Model Ozelli˘ gi. Sonlu model o¨zelli˘gi, bir mantı˘gın dilindeki herhangi bir form¨ ul¨ un modeli varsa onun sonlu modelinin de var oldu˘gunu söyleyen o¨nemli bir özelliktir. Bu sonlu modeli elde etmenin ¸ce¸sitli yöntemleri vardır. Bu böl¨ umde sonlu model elde etmenin yöntemlerinden ikisi olan sonlu Henkin yöntemi ve filtreleme yöntemi verilecektir. Tanım 4.2.1. Bir S mantı˘gının sonlu model özelli˘gine sahip olması i¸cin gerek ve yeter ko¸sul S’de sa˘glanabilen her bir form¨ ul¨ un, bir sonlu modelde de sa˘glanmasıdır. Tanım 4.2.2. ϕ ve φ birer form¨ ul olsun. Bir form¨ ul k¨ umesi Φ’nin, alt form¨ ulleri altında kapalı olması i¸cin gerek ve yeter ko¸sul a¸sa˘gıdakilerin sa˘glanmasıdır. (i) ϕ ∧ ψ ∈ Φ ise ϕ, ψ ∈ Φ’dir. (ii) ¬ϕ ∈ Φ ise ϕ ∈ Φ’dir. (iii) ϕ ∈ Φ ise ϕ ∈ Φ’dir.. 28.

(35) 4.2.1. Sonlu Henkin Y¨ ontemi. Bu böl¨ umde o¨ncelikle bir S modal mantı˘gı i¸cin sonlu Henkin yöntemi a¸cıklanacak, sonra S5EC ve KD45-O modal mantıklarının bu yöntemle elde edilen modelleri tanıtılacaktır. Tanım 4.2.3. Φ ve Γ, Γ ⊆ Φ olacak ¸sekilde iki form¨ ul k¨ umesi olsun. Γ’nın, Φ’de maksimal S-tutarlı olması i¸cin gerek ve yeter ko¸sul Γ’nın S-tutarlı ve Γ ⊂ Γ0 olacak ¸sekilde S-tutarlı bir Γ0 ⊆ Φ form¨ ul k¨ umesinin bulunmamasıdır. Tanım 4.2.4. Φ sonlu ve yeterli bir form¨ ul k¨ umesi olsun. Bu durumda S modal Φ Φ Φ mantı˘gının sonlu Henkin yöntemi ile elde edilen MΦ S = hWS , RS , VS i modeli a¸sa˘gıdaki gibi tanımlanır; (i) WSΦ = {Γ | Γ, Φ’de maksimal S-tutarlıdır }, (ii) RSΦ = {hΓ, Γ0 i | her ϕ i¸cin ϕ ∈ Γ olması i¸cin gerek ve yeter ko¸sul ϕ ∈ Γ0 olmasıdır}, (iii) VSΦ (p) = {Γ | p ∈ Γ}. Lemma 4.2.5. (Lindenbaum) Φ sonlu ve yeterli bir form¨ ul k¨ umesi ve Γ ⊆ Φ, S-tutarlı ise Γ’nın Γ0 ⊆ Φ olacak ¸sekilde maksimal S-tutarlı bir geni¸slemesi vardır. ˙ Ispat. Φ’de S-tutarlı olan Γ form¨ ul k¨ umesinin yine Φ’de maksimal S-tutarlı bir Γ0 form¨ ul k¨ umesine geni¸sletilebilece˘gi gösterilmelidir. Φ k¨ umesi sonlu ve eleman sayısı k olsun ve Φ’deki form¨ ulleri ϕ1 , ..., ϕk ¸seklinde numaralandıralım. Γ0 k¨ umesini, a¸sa˘gıdaki gibi tanımlanmı¸s olan S-tutarlı k¨ umelerin birle¸simi olarak tanımlanacaktır. Γ0 = Γ   . Γn+1 =   Γ0 =. S. n<k. Γn ∪ {ϕn }. e˘ger Γn ∪ {ϕn }, Φ0 deS tutarlıysa. Γn ∪ {¬ϕn } di˘ger hallerde. Γn . S¸imdi de elde edilen Γ0 k¨ umesinin Φ’de maksimal S-tutarlı oldu˘gu. gösterilmelidir. Γ0 , Φ’de S-tutarlıdır: Γ0 , Φ’de S-tutarlı olmasın. S¸u halde Γ0 ’nın tutarlı olmayan bir Ψ alt k¨ umesi vardır oÿle ki bir n i¸cin Ψ ⊆ Γn ’dir. Fakat her Γn , Φ’de S-tutarlı oldu˘gu i¸cin bu bir çeli¸skidir. O halde Γ0 , Φ’de S-tutarlıdır. Γ0 maksimaldir: Keyfi bir ϕn ∈ Φ form¨ ul olsun oÿle ki ϕn ∈ / Γ0 . S¸u halde aynı zamanda ϕn ∈ / Γn ’dir. Γn ∪ {ϕn } Φ’de tutarsız oldu˘gundan Γ0 ∪ {ϕn } de. 29.

(36) tutarsıdır. O halde Γ0 ’n¨ un Φ’de S-tutarlı bir geni¸slemesi yoktur. Buradan Γ0 ’n¨ un Φ k¨ umesinde maksimal oldu˘gu elde edilir. Lemma 4.2.6. Φ sonlu ve yeterli bir form¨ ul k¨ umesi ve Γ, Φ de maksimal S-tutarlı ise a¸sa˘gıdakiler sa˘glanır: (i) Γ k¨ umesi Φ’de t¨ uretim altında kapalıdır. (ii) ¬ϕ ∈ Φ ise ¬ϕ ∈ Γ olması i¸cin gerek ve yeter ko¸sul ϕ ∈ / Γ olmasıdır. (iii) ϕ ∧ ψ ∈ Φ ise ϕ ∧ ψ ∈ Γ olması i¸cin gerek ve yeter ko¸sul ϕ ∈ Γ ve ψ ∈ Γ olmasıdır. ˙ Ispat. (i) ϕ ∈ / Γ olsun. Bu durumda (i)’den ¬ϕ ∈ Γ ’dır. T¨ uretim tanımından Γ ` ¬ϕ olur. O halde Γ `P C ϕ ∧ ¬ϕ’dir. Buradan Γ `⊥ olur ki bu Γ’nın tutarlılı˘gı ile bir çeli¸skidir. (ii) (⇐): ¬ϕ ∈ Γ olsun. Φ alt form¨ uller altında kapalı oldu˘gundan ϕ ∈ Φ’dir. Γ, Φ’de S-tutarlı oldu˘gu i¸cin ϕ ∈ / Γ’dır. (⇒): ϕ ∈ / Γ olsun. Bu durumda Γ ∪ {ϕ} k¨ umesi tutarsızdır yani Γ ∪ {ϕ} `⊥’dur. Buradan Γ ` ϕ →⊥ elde edilir. S¸u halde Γ ` ¬ϕ’dir. Lemmanın (i) ko¸sulu gere˘gi ¬ϕ ∈ Γ olur. (iii) (⇒) : ϕ∧ψ ∈ Γ olsun. ϕ∧ψ ∈ Φ ve Φ alt form¨ uller altında kapalı oldu˘gundan ϕ, ψ ∈ Φ’dır. ϕ ∧ ψ ∈ Γ ise bu durumda Γ ` ϕ ∧ ψ’dir. Buradan Γ `P C ϕ ve Γ `P C ψ elde edilir. (iii)’den ϕ ∈ Γ ve ψ ∈ Γ’dır. (⇐) : ϕ ∈ Γ ve ψ ∈ Γ olsun. T¨ uretim tanımından Γ `P C ϕ ve Γ `P C ψ olur. Buradan Γ ` ϕ ∧ ψ’dir. (iii)’den ϕ ∧ ψ ∈ Γ’dır. . 4.2.2. S5EC i¸ cin Sonlu Henkin Y¨ ontemi. S¸imdi S5EC i¸cin sonlu Henkin yöntemiyle elde edilen modeli tanımlayabiliriz. Tanım 4.2.7. ϕ bir form¨ ul ve 30.

(37) • Φ1 = {ψ, ¬ψ | ψ, ϕ’ nin bir alt form¨ ul¨ ud¨ ur }, • Φ2 = {Ki ψ, ¬Ki ψ | Eψ ∈ Φ1 }, • Φ3 = {Ki Cψ, ¬Ki Cψ, ECψ , ECψ | Cψ ∈ Φ1 } olsun. Φ = Φ1 ∪ Φ2 ∪ Φ3 k¨ umesine ϕ’nin alt form¨ ullerinin yeterli k¨ umesidir denir. Burada Φ sonlu, ϕ ∈ Φ ve Φ alt form¨ uller altında kapalıdır. Tanım 4.2.8. Φ sonlu ve yeterli bir form¨ ul k¨ umesi olmak u ¨zere, S5EC mantı˘gının Φ Φ Henkin metoduyla elde edilen modeli MΦ = hS Φ , R1Φ , ..., Rm , RE , RCΦ , V Φ i a¸sa˘gıdaki gibi tanımlanır: S Φ = {Γ | Γ, Φ’de maksimal tutarlı form¨ ul k¨ umesi} Φ 0 Ri ={(Γ, Γ ) | her ϕ ∈ Φ i¸cin Ki ϕ ∈ Γ olması i¸cin gerek ve yeter ko¸sul Ki ϕ ∈ Γ0 olmasıdır} Φ RE = {(Γ, Γ0 ) | her ϕ ∈ Φ i¸cin Ei ϕ ∈ Γ ise ϕ, Ei ϕ ∈ Γ0 ’dır} RCΦ = {(Γ, Γ0 ) | her ϕ ∈ Φ i¸cin Ci ϕ ∈ Γ olması i¸cin gerek ve yeter ko¸sul Ci ϕ ∈ Γ0 olmasıdır} V Φ (p) = {Γ ∈ S Φ | p ∈ Γ} ˆ form¨ ˆ = Tanım 4.2.9. Γ = {ϕ1 , ..., ϕn } form¨ ul k¨ umesi verilmi¸s olsun. Γ ul¨ u Γ ϕ1 ∧ ... ∧ ϕn ¸seklinde tanımlanır. Lemma 4.2.10. Φ yeterli bir k¨ ume olmak u ¨zere Γ ve Σ k¨ umeleri Φ’de maksimal ˆ < Ki > Σ tutarlı ise (Γ, Σ) ∈ RΦ ’dir. tutarlı olsun. Γ∧ i ˆ < Ki > Σ form¨ ˙ ul¨ un¨ un tutarsız oldu˘gunu gösterIspat. (Γ, Σ) ∈ / RiΦ olsun. Γ∧ meliyiz. Bu durumda bir ϕ ∈ Φ form¨ ul¨ u i¸cin Ki ϕ ∈ Γ ve Ki ϕ ∈ / Σ’dır. Buradan ˆ → Ki ϕ ve ` Σ ˆ → ¬Ki ϕ elde edilir. Bu durumda a¸sa˘gıdaki t¨ `Γ uretimi verebiliriz. ˆ → ¬Ki ϕ 1. ` Σ ˆ 2. ` Ki ϕ → ¬Σ 3. ` Ki (Ki ϕ → ¬ˆ) (Zorunluluk kuralından) ˆ (K aksiyomundan) 4. ` Ki Ki ϕ → Ki ¬Σ ˆ (Ki ϕ → Ki Ki ϕ aksiyomundan) 5. ` Ki ϕ → Ki ¬Σ ˆ → Ki ¬Σ ˆ (` Γ ˆ → Ki ϕ oldu˘gundan) 6. ` Γ ˆ → ¬ < Ki > Σ ˆ 7. ` Γ ˆ < Ki > Σ) ˆ 8. ` ¬(Γ∧ ˆ < Ki > Σ) ˆ →⊥ 9. ` (Γ∧ ˆ < Ki > Σ ˆ form¨ ¨ ˆ < K >i Σ elde edilir. O halde Γ∧ ul¨ u tutarsızdır. Oyleyse Γ∧ tutarlı ise (Γ, ∆) ∈ Ki ’dir.. . 31.

(38) Lemma 4.2.11. Γ, Φ’de maksimal tutarlı bir k¨ ume olmak u ¨zere, her Cϕ ∈ Φ i¸cin, Cϕ ∈ Γ olması i¸cin gerek ve yeter ko¸sul hem Cϕ hem de ϕ’nin Γ = Θ0 , ..., Θn = Γ0 zincirindeki her bir k¨ umenin elemanı olmasıdır. ˙ ˙ Ispat. (⇒): Cϕ ∈ Γ olsun. Ispat zincirin uzunlu˘gu u ¨zerine t¨ umevarımla yapılır. Temel Adım: Zincirin uzunlu˘gu n=0 olsun. Bu durumda Γ = Θ0 = Γ0 ’d¨ ur. Cϕ ∈ Φ ve Φ yeterli bir k¨ ume oldu˘gundan ϕ ∈ Φ’dir. Bununla birlikte ` Cϕ → ϕ ve Γ, Φ’de t¨ uretim altında kapalı oldu˘gundan ϕ ∈ Γ’dır. T¨ umevarım Hipotezi: Zincirin uzunlu˘gu n ve lemma n i¸cin do˘gru olsun. T¨ umevarım Adımı: Zincirin uzunlu˘gu n+1 olsun. T¨ umevarım hipotezinden Cϕ ∈ Θn ’dir. (Θn , Θn+1 ) ∈ RiΦ olsun. Cϕ → ECϕ bir aksiyom, Θn maksimal tutarlı bir k¨ ume ve t¨ uretim altında kapalı oldu˘gundan ECϕ ∈ Θn ’dir. Bununla birlikte, Eϕ ↔ Kϕ1 ∧...∧Kϕm aksiyomundan her a ∈ B i¸cin ` Eϕ → Ka ϕ’yi elde ederiz. Buradan Ka Cϕ ∈ Θn ’dir. (Θn , Θn+1 ) ∈ Ri oldu˘gundan Cϕ ∈ Θn+1 ’dir. Temel adıma benzer olarak ϕ ∈ Θn+1 elde edilir. (⇐): Hem Cϕ hem de ϕ, Γ = Θ0 , ..., Θn = Γ0 zincirindeki her bir k¨ umenin elemanı olsun. Her Cϕ ∈ Φ i¸cin Cϕ ∈ Γ oldu˘gunu göstermeliyiz. CΦ k¨ umesi Φ’deki maksimal tutarlı Σ k¨ umelerinin k¨ umesi olsun oÿle ki ϕ form¨ ul¨ u, Σ = χ0 , ..., χk = Σ0 zincirindeki her k¨ umenin elemanıdır. Ψ=. W. Σ∈CΦ. ˆ Σ. ˆ form¨ form¨ ul¨ un¨ u göz o¨n¨ une alalım. Φ’de tutarlı Γ ul¨ u Ψ form¨ ul¨ un¨ un bir alt ˆ → Ψ’dır. Bununla birlikte Σ ∈ CΦ ise ϕ ∈ Σ’dır. form¨ ul¨ u oldu˘gundan ` Γ ˆ ˆ form¨ S¸u halde ϕ form¨ ul¨ u Σ’nın bir alt form¨ ul¨ u ve Σ ul¨ u Ψ form¨ ul¨ un¨ un bir alt form¨ ul¨ u oldu˘gundan ` Ψ → ϕ’dir. S¸imdi de ` Ψ → EΨ oldu˘gunu gösterelim. Bunun i¸cin Ψ ∧ ¬EΨ form¨ ul¨ u tuˆ vardır oÿle ki Σ ˆ ∧ ¬EΨ tutarlı olsun. Bu durumda Ψ’nin bir alt form¨ ul¨ u Σ ˆ < Ka > ¬Ψ form¨ tarlıdır. Buradan bir a ki¸sisi i¸cin Σ∧ ul¨ un¨ un tutarlı oldu˘gu ˆ < Ka > WΩ∈(S Φ −C ) Ω ˆ form¨ ul¨ u tutarlıdır. elde edilir. ¬Ψ tutarlı oldu˘gundan Σ∧ Φ ˆ ∧ WΩ∈(S Φ −C ) < Ka > Ω ˆ form¨ Σ ul¨ u de tutarlıdır. Bu durumda Φ’de maksimal Φ ˆ ∈ ˆ ∧ WΛ∈(S Φ −C ) < Ka > Λ ˆ tutarlı tutarlı bir Ω form¨ ul k¨ umesi i¸cin Ω / CΦ ve Σ Φ oldu˘gu elde edilir. Lemma 4.2.10’dan (Σ, Ω) ∈ RaΦ ’dır. Bununla birlikte Ω ∈ / CΦ oldu˘gundan Ω’da bir zincir vardır oÿle ki ϕ bu zincirdeki k¨ umelerden en az birinin elemanı de˘gildir. S¸u halde ilk elemanı Σ olan bir zincir vardır oÿle ki ϕ 32.