1Semantykalogikipierwszegorz˛edu W 5 :M H IA R M D T

M

D

T

I A

R

W 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 P^I ⊆ Dⁿ (b) ka˙zdemu n-argumentowemu symbolowi funkcyjnemu f ∈ F funkcj˛e

f^I : Dⁿ→ D

(c) ka˙zdej stałej c ∈ C element c^I ∈ 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 x^Aoznacza 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 t^I,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 x^A= t^I. 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. t^I= 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 t^I,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 x^A = t^I. 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 x^A = a^I. 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 a^J= x^A.

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 a^J= x^A, 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 c^I = c.

2. Je´sli f jest n-argumentowym symbolem funkcyjnym w L oraz t₁, t₂, . . . , t_n s ˛a elementami D, to f^I(t₁, t₂, . . . , t_n) jest termem domkni˛etym f (t₁, t₂, . . . , t_n).

3. Je´sli R jest n-argumentowym predykatem w L oraz t₁, t₂, . . . , t_ns ˛a elemen- tami D, to (t1, t₂, . . . , t_n) ∈ R^Iwtedy i tylko wtedy, gdy zdanie R(t1, t₂, . . . , t_n) 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(t₁, t₂, . . . , t_n) jest zdaniem, ka˙zdy t_i jest termem domkni˛etym, a wi˛ec t^I,A_i = t^I_i = ti. Z zało˙zenia, ˙ze R(t1, t2, . . . , tn) nale˙zy do H i z definicji zbioru Hintikki mamy: (t1, t2, . . . , tn) ∈ R^I. Ostatecznie:

(t^I,A₁ , t^I,A₂ , . . . , t^I,A_n ) ∈ R^I,

czyli (R(t1, t₂, . . . , t_n))^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 L^parrozumiemy 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 L^par, 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 L^par. 2. Je´sli δ ∈ S, to S ∪ {δ(a)} ∈ C dla pewnego parametru a j˛ezyka L^par.

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 L^par).

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 L^par ma przeliczaln ˛a liczb˛e symboli, wi˛ec ma te˙z przeliczal- nie wiele zda´n. Niech Φ1, Φ₂, Φ₃, . . . 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 = S_n∪ {Φ_n}.

4. Je´sli Sn∪ {Φ_n} ∈ C^∗ oraz Φnjest zdaniem δ, to niesko´nczona liczba para- metrów b˛edzie nowa dla S_n∪ {Φ_n}; wybieramy jeden z nich, powiedzmy a i definiujemy: Sn+1= S_n∪ {Φ_n} ∪ {δ(a)}.

Na mocy powy˙zszej konstrukcji, dla ka˙zdego n: Sn ∈ C^∗ oraz Sn ⊆ S_n+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 L^par.

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 L^par.

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 L^par, 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 L^par, 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 pogon@amu.edu.pl