M
ETODYD
OWODZENIAT
WIERDZE ´NI A
UTOMATYZACJAR
OZUMOWA ´NW YKŁAD 5 A : M ODELE H ERBRANDA
III rok kognitywistyki UAM, 2016–2017
Zakładamy, ˙ze słuchacze pami˛etaj ˛a wiadomo´sci z kursu Logika I dotycz ˛ace se- mantyki KRP. W tym wykładzie poka˙zemy, jak budowa´c modele pewnego szcze- gólnego typu.
1 Semantyka logiki pierwszego rz˛edu
1.1 Modele
Przez model j˛ezyka pierwszego rz˛edu L o sygnaturze zło˙zonej ze zbioru predyka- tów R, symboli funkcyjnych F oraz stałych indywidualnych C rozumiemy par˛e M = (D, I), gdzie:
1. D jest niepustym zbiorem (dziedzin ˛aM)
2. I jest odwzorowaniem (interpretacj ˛a), które przyporz ˛adkowuje:
(a) ka˙zdemu n-argumentowemu predykatowi P ∈ R relacj˛e PI ⊆ Dn (b) ka˙zdemu n-argumentowemu symbolowi funkcyjnemu f ∈ F funkcj˛e
fI : Dn→ D
(c) ka˙zdej stałej c ∈ C element cI ∈ D.
Zakładamy, ˙ze słuchacze pami˛etaj ˛a definicje nast˛epuj ˛acych poj˛e´c:
1. Warto´sciowanie (w dziedzinie modelu)
2. Podstawienie (termu za zmienn ˛a w termie lub formule) 3. Warto´s´c termu/formuły w modelu dla danego warto´sciowania 4. Spełnianie i prawdziwo´s´c formuł w modelu
5. Wynikanie logiczne
W notacji proponowanej przez Fittinga:
1. Podstawienie σ : V → T (funkcja ze zbioru zmiennych w zbiór termów).
(a) Je´sli σ jest podstawieniem, to σxjest podstawieniem, które przyjmuje warto´s´c x dla argumentu x, a pozostałe warto´sci ma takie same, jak podstawienie σ.
(b) Operacj˛e podstawiania rozszerzamy w znany sposób na zbiór formuł.
(c) Warto´s´c podstawienia σ dla formuły Φ oznaczamy przez Φσ.
2. Warto´sciowanie A : V → D (funkcja ze zbioru zmiennych w dziedzin˛e modelu). Niech xAoznacza warto´s´c A dla argumentu x.
(a) Warto´sciowania rozszerzamy w znany sposób na zbiory: termów oraz formuł.
(b) Warto´s´c termu t w modelu M = (D, I) przy warto´sciowaniu A ozna- czamy przez tI,A.
(c) Warto´s´c formuły Φ w modelu M = (D, I) przy warto´sciowaniu A oznaczamy przez ΦI,A.
Znany Fakt. Załó˙zmy, ˙ze t jest termem domkni˛etym, Φ formuł ˛a j˛ezyka pierw- szego rz˛edu L, a M = (D, I) modelem dla L. Niech x b˛edzie zmienn ˛a, za´s A warto´sciowaniem takim, ˙ze xA= tI. Wtedy: (Φ(x/t))I,A= ΦI,A.
1.2 Modele Herbranda
Model M = (D, I) dla j˛ezyka L nazywamy modelem Herbranda, gdy:
1. D jest zbiorem wszystkich termów domkni˛etych (bazowych) j˛ezyka L.
2. tI= t dla ka˙zdego termu domkni˛etego t.
Zauwa˙zmy, ˙ze w modelu Herbranda warto´sciowania pokrywaj ˛a si˛e z podsta- wieniami. W konsekwencji (co łatwo dowie´s´c przez indukcj˛e strukturaln ˛a; zob.
Fitting 1990, 108):
1. Je´sli M = (D, I) jest modelem Herbranda dla L, to tI,A = (tA)I dla ka˙z- dego termu j˛ezyka L.
2. Je´sli M = (D, I) jest modelem Herbranda dla L, to ΦI,A= (ΦA)I.
Warunki prawdziwo´sci dla kwantyfikatorów w modelu Herbranda:
1. M |= ∀xΦ wtedy i tylko wtedy, gdy M |= Φ[x/d] dla wszystkich d ∈ D.
2. M |= ∃xΦ wtedy i tylko wtedy, gdy M |= Φ[x/d] dla pewnego d ∈ D.
1.3 Jednolita notacja dla j˛ezyka logiki pierwszego rz˛edu
Notacja Smullyana dla j˛ezyków pierwszego rz˛edu oprócz podanych wcze´sniej kon- wencji dla funktorów prawdziwo´sciowych uwzgl˛ednia jeszcze notacj˛e dla formuł skwantyfikowanych oraz ich negacji. Rozró˙znia si˛e dwa typy: γ-formuły, które
„działaj ˛a” uniwersalnie (czyli formuły z kwantyfikatorem generalnym lub z za- przeczeniem kwantyfikatora egzystencjalnego) oraz δ-formuły, które „działaj ˛a” eg- zystencjalnie (czyli formuły z kwantyfikatorem egzystencjalnym lub z zaprzecze- niem kwantyfikatora generalnego). Dla ka˙zdego z tych typów formuł oraz dowol- nego termu t okre´sla si˛e ich instancje w sposób nast˛epuj ˛acy:
γ γ(t) δ δ(t)
∀xϕ ϕ(x/t) ∃xϕ ϕ(x/t)
¬∃xϕ ¬ϕ(x/t) ¬∀xϕ ¬ϕ(x/t)
Ta konwencja zostaje nieco zmodyfikowana w przypadku j˛ezyków pierwszego rz˛edu z symbolami funkcyjnymi (gdzie uwzgl˛edniamy dodatkowo unifikacj˛e termu wyst˛epuj ˛acego w instancjach), jak zobaczymy pó´zniej.
U˙zyteczny Lemat. Niech S b˛edzie zbiorem zda´n, a γ, δ zdaniami. Wtedy:
1. Je´sli S ∪ {γ} jest spełnialny, to spełnialny jest S ∪ {γ, γ(t)} dla dowolnego termu domkni˛etego t.
2. Je´sli S ∪ {δ} jest spełnialny, to spełnialny jest S ∪ {δ, δ(a)} dla dowolnej stałej a, która nie wyst˛epuje ani w S ani w δ.
Dowód U˙zytecznego Lematu. Zauwa˙zmy, ˙ze w lemacie jest mowa wył ˛acznie o zdaniach.
Dowód punktu 1. Załó˙zmy, ˙ze S ∪ {γ} jest spełnialny w modelu M = (D, I).
Poka˙zemy, ˙ze w tym samym modelu spełnialny jest S ∪ {γ, γ(t)} dla dowolnego termu domkni˛etego t.
1. Poniewa˙z w modelu M prawdziwe jest γ, wi˛ec w modelu tym prawdziwe jest tak˙ze ∀xγ(x), gdzie x jest zmienn ˛a nie wyst˛epuj ˛ac ˛a w γ.
2. Tak wi˛ec, dla ka˙zdego warto´sciowania A, w M prawdziwe jest (γ(x))I,A.
3. Niech A b˛edzie warto´sciowaniem takim, ˙ze xA = tI. Na mocy przywoła- nego wcze´sniej Znanego Faktu, mamy:
(γ(t))I,A= (γ(x/t))I,A= (γ(x))I,A= 1.
Dowód punktu 2. Załó˙zmy, ˙ze S ∪ {δ} jest spełnialny w modelu M = (D, I) oraz
˙ze a jest stał ˛a nie wyst˛epuj ˛ac ˛a ani w S ani w δ. Poka˙zemy, ˙ze S ∪ {δ, δ(a)} jest spełnialny w pewnym modelu dla L.
1. Poniewa˙z w modelu M prawdziwe jest δ, wi˛ec w modelu tym prawdziwe jest tak˙ze ∃xδ(x), gdzie x jest zmienn ˛a nie wyst˛epuj ˛ac ˛a w δ.
2. Tak wi˛ec, (δ(x))I,A = 1 dla pewnego warto´sciowania A. Nie mo˙zna jednak dogmatycznie zało˙zy´c, ˙ze xA = aI. Mimo to, damy rad˛e, wPiSuj ˛ac si˛e w deklaracj˛e powszechnego optymizmu.
3. Budujemy nowy model M∗ = (D, J) o tej samej dziedzinie D co model M oraz interpretacji J, która nie ró˙zni si˛e od I dla wszystkich symboli ró˙znych od a, natomiast aJ= xA.
4. Zdania nie zawieraj ˛ace stałej a maj ˛a te same warto´sci w modelach M oraz M∗.
5. A zatem S ∪ {δ} jest spełnialny w modelu M∗oraz (δ(x/a))J,A= 1.
6. Poniewa˙z aJ= xA, wi˛ec mamy:
(δ(a))J,A= (δ(x/a))J,A= (δ(x))J,A = 1.
7. A zatem S ∪ {δ, δ(a)} jest spełnialny w modelu M∗. Szczególny przypadek powy˙zszego lematu to:
Fakt. Je´sli M = (D, I) jest modelem Herbranda dla L, to:
1. M |= γ wtedy i tylko wtedy, gdy M |= γ(d) dla wszystkich d ∈ D.
2. M |= δ wtedy i tylko wtedy, gdy M |= δ(d) dla pewnego d ∈ D.
W j˛ezykach pierwszego rz˛edu zachodz ˛a twierdzenia: o indukcji strukturalnej oraz rekursji strukturalnej (zob. Fitting 1990, 111-112).
1.4 Lemat Hintikki
Zbiór zda´n H j˛ezyka pierwszego rz˛edu L jest zbiorem Hintikki pierwszego rz˛edu (dla L), gdy H jest zdaniowym zbiorem Hintikki (zob.: wykład drugi) oraz:
1. Je´sli γ ∈ H, to γ(t) ∈ H, dla ka˙zdego termu domkni˛etego j˛ezyka L.
2. Je´sli δ ∈ H, to δ(t) ∈ H, dla pewnego termu domkni˛etego j˛ezyka L.
Lemat Hintikki. Załó˙zmy, ˙ze zbiór termów domkni˛etych j˛ezyka pierwszego rz˛edu L jest niepusty. Je´sli H zbiorem Hintikki pierwszego rz˛edu dla L, to H jest speł- nialny w modelu Herbranda dla L.
Dowód Lematu Hintikki. Niech H b˛edzie zbiorem Hintikki pierwszego rz˛edu dla L. Skonstruujemy model Herbranda M = (D, I) dla L, a potem poka˙zemy, ˙ze H jest spełnialny w M.
Niech D b˛edzie zbiorem termów domkni˛etych j˛ezyka L. Z zało˙zenia: D 6= ∅.
Okre´slamy interpretacj˛e I:
1. Je´sli c jest stał ˛a j˛ezyka L, to cI = c.
2. Je´sli f jest n-argumentowym symbolem funkcyjnym w L oraz t1, t2, . . . , tn s ˛a elementami D, to fI(t1, t2, . . . , tn) jest termem domkni˛etym f (t1, t2, . . . , tn).
3. Je´sli R jest n-argumentowym predykatem w L oraz t1, t2, . . . , tns ˛a elemen- tami D, to (t1, t2, . . . , tn) ∈ RIwtedy i tylko wtedy, gdy zdanie R(t1, t2, . . . , tn) nale˙zy do H.
Przez indukcj˛e strukturaln ˛a poka˙zemy teraz, ˙ze dla ka˙zdego zdania Φ j˛ezyka L: je´sli Φ ∈ H, to M |= Φ.
1. Załó˙zmy, ˙ze zdanie atomowe R(t1, t2, . . . , tn) nale˙zy do H. Trzeba poka- za´c, ˙ze (R(t1, t2, . . . , tn))I,A= 1 dla ka˙zdego warto´sciowania A. Poniewa˙z R(t1, t2, . . . , tn) jest zdaniem, ka˙zdy ti jest termem domkni˛etym, a wi˛ec tI,Ai = tIi = ti. Z zało˙zenia, ˙ze R(t1, t2, . . . , tn) nale˙zy do H i z definicji zbioru Hintikki mamy: (t1, t2, . . . , tn) ∈ RI. Ostatecznie:
(tI,A1 , tI,A2 , . . . , tI,An ) ∈ RI,
czyli (R(t1, t2, . . . , tn))I,A = 1 dla wszystkich warto´sciowa´n A, a wi˛ec pokazali´smy, ˙ze M |= R(t1, t2, . . . , tn).
2. Kroki dotycz ˛ace ⊥, > s ˛a oczywiste (definicja relacji |=).
3. Kroki indukcyjne dla funktorów prawdziwo´sciowych s ˛a tak˙ze oczywiste (de- finicja relacji |=).
4. Załó˙zmy, ˙ze γ jest zdaniem w L oraz γ ∈ H. Poka˙zemy, ˙ze M |= γ. Po- niewa˙z γ ∈ H, wi˛ec γ(t) ∈ H dla ka˙zdego termu domkni˛etego t (na mocy definicji zbioru Hintikki). Na mocy zało˙zenia indukcyjnego oraz faktu, ˙ze D jest zbiorem wszystkich termów domkni˛etych mamy: M |= γ(t) dla ka˙z- degotermu domkni˛etego t. Na mocy U˙zytecznego Lematu, M |= γ.
5. Załó˙zmy, ˙ze δ jest zdaniem w L oraz δ ∈ H. Poka˙zemy, ˙ze M |= δ. Po- niewa˙z δ ∈ H, wi˛ec δ(t) ∈ H dla pewnego termu domkni˛etego t (na mocy definicji zbioru Hintikki). Na mocy zało˙zenia indukcyjnego oraz faktu, ˙ze D jest zbiorem wszystkich termów domkni˛etych mamy: M |= δ(t) dla pew- negotermu domkni˛etego t. Na mocy U˙zytecznego Lematu, M |= δ.
Uwaga. W dalszej cz˛e´sci wykorzystywa´c b˛edziemy cz˛esto nowe symbole (stałe) dodawane do rozwa˙zanego j˛ezyka pierwszego rz˛edu L. Je´sli L(R, F, C) jest j˛e- zykiem ze zbiorem predykatów R, zbiorem symboli funkcyjnych F oraz zbiorem stałych C, za´s par jest przeliczalnym zbiorem stałych takim, ˙ze C ∩ par = ∅, to przez Lparrozumiemy j˛ezyk L(R, F, C ∪ par). Elementy zbioru par nazywamy nowymi stałymialbo parametrami.
1.5 Własno´sci niesprzeczno´sci
Je´sli C jest rodzin ˛a zbiorów zda´n j˛ezyka Lpar, to C nazywamy własno´sci ˛a nie- sprzeczno´sci pierwszego rz˛edu(dla j˛ezyka L), gdy C jest zdaniow ˛a własno´sci ˛a nie- sprzeczno´sci (zob. wykład drugi) oraz dla ka˙zdego S ∈ C:
1. Je´sli γ ∈ S, to S ∪ {γ(t)} ∈ C dla ka˙zdego termu domkni˛etego j˛ezyka Lpar. 2. Je´sli δ ∈ S, to S ∪ {δ(a)} ∈ C dla pewnego parametru a j˛ezyka Lpar.
Przez alternatywn ˛a własno´s´c niesprzeczno´sci pierwszego rz˛edurozumiemy ro- dzin˛e C spełniaj ˛ac ˛a warunki nakładane na własno´sci niesprzeczno´sci pierwszego rz˛edu ale przy zast ˛apieniu warunku dla δ-formuł przez warunek:
• Je´sli δ ∈ S, to S ∪ {δ(a)} ∈ C dla ka˙zdego parametru a, który nie wyst˛epuje w S.
Przez podstawienie parametru rozumiemy dowolne odwzorowanie zbioru par w siebie. Je´sli π jest takim odwzorowaniem, Φ jest formuł ˛a, a S zbiorem formuł, to:
1. Φπ jest formuł ˛a powstaj ˛ac ˛a z Φ przez dokonanie podstawienia π.
2. Sπ jest zbiorem formuł {Φπ : Φ ∈ S}.
Fakt. Niech C b˛edzie własno´sci ˛a niesprzeczno´sci pierwszego rz˛edu domkni˛et ˛a na podzbiory. Definiujemy C+: S ∈ C+wtedy i tylko wtedy, gdy Sπ ∈ C dla pewnego podstawienia parametrów π. Wtedy:
1. C ⊆ C+
2. C+jest domkni˛eta na podzbiory.
3. C+jest alternatywn ˛a własno´sci ˛a niesprzeczno´sci pierwszego rz˛edu.
Ka˙zda alternatywna własno´s´c niesprzeczno´sci pierwszego rz˛edu, która jest do- mkni˛eta na podzbiory mo˙ze zosta´c rozszerzona do własno´sci niesprzeczno´sci cha- rakteru sko´nczonego.
1.6 Twierdzenie o Istnieniu Modelu
Twierdzenie o Istnieniu Modelu. Je´sli C jest własno´sci ˛a niesprzeczno´sci pierw- szego rz˛edu dla L, a S jest zbiorem zda´n z L oraz S ∈ C, to S jest spełnialny (w modelu Herbranda dla j˛ezyka Lpar).
Dowód. Załó˙zmy, C jest własno´sci ˛a niesprzeczno´sci pierwszego rz˛edu dla L, a S jest zbiorem zda´n z L oraz S ∈ C. Zbudujemy model, w którym prawdziwe b˛ed ˛a wszystkie zdania z S.
Rozszerzamy C do alternatywnej własno´sci niesprzeczno´sci pierwszego rz˛edu charakteru sko´nczonego C∗. Wtedy oczywi´scie S ∈ C∗.
Poniewa˙z j˛ezyk Lpar ma przeliczaln ˛a liczb˛e symboli, wi˛ec ma te˙z przeliczal- nie wiele zda´n. Niech Φ1, Φ2, Φ3, . . . b˛edzie wyliczeniem tych wszystkich zda´n w ustalonym porz ˛adku. Zdefiniujemy teraz ci ˛ag S1, S2, S3, . . . zbiorów nale˙z ˛acych do C∗ w ten sposób, ˙ze dla ka˙zdego takiego zbioru Snliczba dot ˛ad nieu˙zywanych w tych zbiorach parametrów b˛edzie niesko´nczona (jest tak oczywi´scie dla S, po- niewa˙z w S nie ma ˙zadnych parametrów). Niech mianowicie:
1. S1= S.
2. Je´sli Sn∪ {Φn} /∈ C∗, to niech Sn+1 = Sn.
3. Je´sli Sn∪ {Φn} ∈ C∗ oraz Φn nie jest δ-zdaniem, to niech Sn+1 = Sn∪ {Φn}.
4. Je´sli Sn∪ {Φn} ∈ C∗ oraz Φnjest zdaniem δ, to niesko´nczona liczba para- metrów b˛edzie nowa dla Sn∪ {Φn}; wybieramy jeden z nich, powiedzmy a i definiujemy: Sn+1= Sn∪ {Φn} ∪ {δ(a)}.
Na mocy powy˙zszej konstrukcji, dla ka˙zdego n: Sn ∈ C∗ oraz Sn ⊆ Sn+1. Niech H = S
n
Sn. Wtedy S ⊆ H. Tak, jak w przypadku zdaniowych zbiorów Hintikki (zob.: wykład drugi) dowodzimy, ˙ze:
1. H ∈ C∗
2. H jest elementem maksymalnym w C∗
3. H jest zbiorem Hintikki pierwszego rz˛edu dla j˛ezyka Lpar.
Na mocy Lematu Hintikki H jest spełnialny, a poniewa˙z S ⊆ H, wi˛ec tak˙ze S jest spełnialny w modelu Herbranda dla Lpar.
Fitting 1990 (117–119) podaje kilka bezpo´srednich zastosowa´n Twierdzenia o Istnieniu Modelu:
1. Twierdzenie o Zwarto´sci. Niech S b˛edzie zbiorem zda´n j˛ezyka pierwszego rz˛edu L. Je´sli ka˙zdy sko´nczony podzbiór zbioru S jest spełnialny, to S jest spełnialny.
2. Wniosek. Je´sli S jest zbiorem zda´n j˛ezyka pierwszego rz˛edu i S jest speł- nialny w dowolnie du˙zych modelach sko´nczonych, to S jest spełnialny w modelu niesko´nczonym.
3. Twierdzenie Löwenheima-Skolema. Niech S b˛edzie zbiorem zda´n j˛ezyka pierwszego rz˛edu L. Je´sli S jest spełnialny, to S jest spełnialny w modelu przeliczalnym.
Dowód Twierdzenia o Zwarto´sci otrzymujemy zauwa˙zaj ˛ac, ˙ze własno´sci ˛a nie- sprzeczno´sci pierwszego rz˛edu jest rodzina takich zbiorów W zda´n j˛ezyka Lpar, dla których:
1. ka˙zdy sko´nczony podzbiór zbioru W jest spełnialny 2. niesko´nczenie wiele parametrów jest nowych dla W .
Dowód Twierdzenia Löwenheima-Skolema otrzymujemy zauwa˙zaj ˛ac, ˙ze wła- sno´sci ˛a niesprzeczno´sci pierwszego rz˛edu jest rodzina takich zbiorów W zda´n j˛e- zyka Lpar, dla których:
1. W jest spełnialny
2. niesko´nczenie wiele parametrów jest nowych dla W .
Dodajmy na marginesie, ˙ze na mocy powy˙zszych wyników widoczne jest m.in.,
˙ze:
1. Poj˛ecie sko´nczono´sci nie jest wyra˙zalne w logice pierwszego rz˛edu.
2. Je´sli teoria mnogo´sci pierwszego rz˛edu jest niesprzeczna, to ma model prze- liczalny. Nie stoi to w sprzeczno´sci z faktem, i˙z w teorii mnogo´sci dowo- dzimy istnienia zbiorów nieprzeliczalnych. Ujmuj ˛ac rzecz w wielkim skró- cie, przeliczalny model dla teorii mnogo´sci nie zawiera wystarczaj ˛acej liczby bijekcji.
Nieco pó´zniej powiemy jeszcze par˛e słów o Twierdzeniu Herbranda.
JERZYPOGONOWSKI
Zakład Logiki i Kognitywistyki UAM www.kognitywistyka.amu.edu.pl http://logic.amu.edu.pl/index.php/Dydaktyka [email protected]
