07.pdf
(
121 KB
)
Pobierz
c:\3\7.dvi
2.2. KLASYCZNYRACHUNEK PREDYKATÓW
179
2.3.3. Reguły rachunku predykatów a prawdziwość
Udowodnimy teraz kilka twierdzeń pokazujących niezawodność
reguł rachunku predykatów. Pokazane więc zostanie, że biorąc jako
przesłankiformułyspełnionewjakimśmodeluikorzystającwyłącz-
niezregułrachunkupredykatów,określonych wdefinicjidowoduw
tym rachunku, jako wniosek otrzymamy formułę spełnioną w tym
modelu.
TWIERDZENIE11.
Niech wszystkie zmienne wolne formuły
ϕ
znajdują się w ciągu
v
0
,v
1
,...,v
n
. Jeżeli
ϕ
jest tautologią języka rachunku predykatów
lubaksjomatemteoriiidentyczności,todladowolnegomodelu
M
idowolnego ciąguprzedmiotów
x
0
,x
1
,...,x
n
M|
DOWÓD
Niech
ϕ
będzietautologiąjeżykarachunkukwantyfikatorów.Ist-
nieje zatem tautologia języka rachunku zdań taka, z której
ϕ
jest
otrzymaneprzezwpisanieformuł,powiedzmy,
ϕ
1
,ϕ
2
,...,ϕ
m
wmiej-
sce liter zdaniowych – jednocześnie za tę samą literę tej samej for-
muły. Zauważmy, że
ϕ
zbudowane jest tylko za pomocą spójników
zdaniowych z formuł
ϕ
1
,ϕ
2
,...,ϕ
m
. Zatem zgodnie ze znaczeniami
spójników zdaniowych
ϕ
będzie spełnione w modelu
M
dla ciągu
przedmiotów
[
x
0
x
1
...x
n
]
bezwzględunato,czy
ϕ
i
,
1
≤
i
≤
m
będzie,
czy też nie będzie spełnione w modelu
M
dla ciągu przedmiotów
[
x
0
x
1
...x
n
]
.
Wwypadkuaksjomatówidentycznościzauważmy,żeId1wynika
bezpośredniozdefinicjispełniania.Id2jestwnioskiemztw.4,aId3
wnioskiemztw.5.
TWIERDZENIE12.
Niechwszystkiezmiennewolneformuł
ϕ
i
φ
znajdująsięwciągu
v
0
,v
1
,...,v
n
. Dla dowolnego modelu
M
i dowolnego ciągu przed-
miotów
x
0
,x
1
,...,x
n
=
ϕ
[
x
0
x
1
...x
n
]
.
180
2. LOGIKA PREDYKATÓW
jeżeli
=(
ϕ
⇒
φ
)[
x
0
x
1
...x
n
]
oraz
M|
=
ϕ
[
x
0
x
1
...x
n
]
,
totakże
M|
=
φ
[
x
0
x
1
...x
n
]
.
DOWÓD
Niechdlamodelu
M
orazciągu
x
0
,x
1
,...,x
n
zachodzi
M|
=(
ϕ
⇒
φ
)[
x
0
x
1
...x
n
]
oraz
=
ϕ
[
x
0
x
1
...x
n
]
.
Zgodniezdefinicjąspełnianiamamy,żegdy
M|
M|
=(
ϕ
⇒
φ
)[
x
0
x
1
...x
n
]
,
tojeżeli
M|
=
ϕ
[
x
0
x
1
...x
n
]
,
to
M|
=
φ
[
x
0
x
1
...x
n
]
.
Zatemdostajemy,że
M|
=
φ
[
x
0
x
1
...x
n
]
.
WNIOSEK1.
Niech wszystkie zmienne wolne występujące w formułach
ϕ
i
φ
znajdująsięwciągu
v
0
,v
1
,...,v
n
.Dladowolnegomodelu
M
:jeżeli
dladowolnegociągu
x
0
,x
1
,...,x
n
zachodzi
M|
=(
ϕ
⇒
φ
)[
x
0
x
1
...x
n
]
oraz
dladowolnegociągu
x
0
,x
1
,...,x
n
zachodzi
M|
=
ϕ
[
x
0
x
1
...x
n
]
,
to
dladowolnegociągu
x
0
,x
1
,...,x
n
zachodzi
M|
2.2. KLASYCZNYRACHUNEK PREDYKATÓW
181
=
φ
[
x
0
x
1
...x
n
]
.
WNIOSEK2.
Niech wszystkie zmienne wolne występujące w formułach
ϕ
i
φ
znajdują się w ciągu
v
0
,v
1
,...,v
n
. Jeżeli dla dowolnych modelu
M
iciągu
x
0
,x
1
,...,x
n
zachodzi
M|
oraz
dladowolnychmodelu
M
iciągu
x
0
,x
1
,...,x
n
zachodzi
M|
=
ϕ
[
x
0
x
1
...x
n
]
,
=
φ
[
x
0
x
1
...x
n
]
.
Wszczególności,gdy
ϕ
i
φ
sązdaniamimamy
jeżeli
|
=
ϕ
⇒
φ
i
|
=
ϕ
,to
|
=
φ
.
Zatrzymajmysięchwilęnadsposobemwnioskowaniazastosowa-
nymprzyotrzymywaniuobuwniosków.Otóżprzesłanka,wtymwy-
padkutwierdzenie12,było–najogólniejtoujmując–postaci
∀
v
1
,v
2
.
(
ϕ
⇒
φ
)
natejpodstawiewnioskowaliśmy,że
∀
v
1
.
(
∀
v
2
.ϕ
⇒∀
v
2
.φ
)
.
Tak–pomijającszczegóły–otrzymaliśmywniosek1.Wniosek2
zostałotrzymanywanalogicznysposóbzwniosku1.Podobnewnioski
jakztwierdzenia12wanalogicznysposóbbędziemymogliotrzymać
zdowodzonychniżejtwierdzeńoregułachrachunkupredykatów.
TWIERDZENIE13.
Niech wszystkie zmienne wolne formuły
ϕ
znajdują się w ciągu
v
0
,v
1
,...,v
n
.Niechterm
t
będziepodstawialnywformule
ϕ
wmiej-
scezmiennej
v
i
iniechwszystkie zmienne wolne formuły
ϕ
(
v
i
/t
)
znajdująsięwciągu
v
0
,v
1
,...,v
m
.Dladowolnego modelu
M
jeżelidladowolnego ciąguprzedmiotów
x
0
,x
1
,...,x
n
M|
=(
ϕ
⇒
φ
)[
x
0
x
1
...x
n
]
to
dladowolnychmodelu
M
iciągu
x
0
,x
1
,...,x
n
zachodzi
M|
182
2. LOGIKA PREDYKATÓW
=
ϕ
[
x
0
x
1
...x
n
]
,
totakżedladowolnego ciąguprzedmiotów
x
0
,x
1
,...,x
m
M|
M|
=
ϕ
(
v
i
/t
)[
x
0
x
1
...x
m
]
.
DOWÓD
Rozważmy wpierw wypadek, gdy zmienna
v
i
nie występuje w
termie
t
.Niechdladowolnegociągu
x
0
,x
1
,...,x
n
M|
=
ϕ
(
v
i
/t
)[
x
0
x
1
...x
m
]
,
to na podstawie twierdzenia 5 nie zachodzi to również dla ciągu
x
0
,x
1
,...,x
m
,...,x
k
;
m,n
≤
k
.
Z założenia zmienna
v
i
nie występuje w termie
t
,więcnapod-
stawietwierdzenia7dlaciągu
x
0
,x
1
,...,x
i
−
1
,t
[
x
0
x
1
...x
k
]
,x
i
+1
,...,x
k
niezachodzi
=
ϕ
[
x
0
x
1
...x
i
−
1
t
[
x
0
x
1
...x
k
]
x
i
+1
...x
n
...x
k
]
.
Azgodnieztwierdzeniem5niezachodzi
M|
M|
=
ϕ
[
x
0
x
1
...x
i
−
1
t
[
x
0
x
1
...x
k
]
x
i
+1
...x
n
]
,
coprzeczyzałożeniu,żedladowolnegociągu
x
0
,x
1
,...,x
n
M|
=
ϕ
[
x
0
x
1
...x
n
]
.
W wypadku, gdy zmienna
v
i
występuje w termie
t
bierzemy
zmienną
v
l
taką, któraniewystępujeaniwformule
ϕ
,aniwtermie
t
.Zdefinicjipodstawianiajestjasne,żeformuła
(
ϕ
(
v
i
/v
l
))(
v
l
/t
)
jestrównokształtnazformułą
ϕ
(
v
i
/t
)
.
Niechwszystkiezmiennewolneformuły
ϕ
(
v
i
/v
l
)
znajdująsięwciągu
v
0
,v
1
,...,v
q
. Na podstawie powyższego jeżeli dla dowolnego ciągu
x
0
,x
1
,...,x
q
zachodzi
=
ϕ
(
v
i
/v
l
)[
x
0
x
1
...x
q
]
,
=
ϕ
[
x
0
x
1
...x
n
]
.
Jeżelidlajakiegośmodelu
M
iciągu
x
0
,x
1
,...,x
m
niezachodzi
M|
M|
2.2. KLASYCZNYRACHUNEK PREDYKATÓW
183
=(
ϕ
(
v
i
/v
l
))(
v
l
/t
)[
x
0
x
1
...x
m
]
,
cowzwiązkuzrównokształtnością
(
ϕ
(
v
i
/v
l
))(
v
l
/t
)
z
=
ϕ
(
v
i
/t
)[
x
0
x
1
...x
m
]
.
Napodstawiewnioskuztwierdzenia7mamyjednak,żedladowolnego
ciągu
x
0
,x
1
,...,x
n
zachodzi
M|
=
ϕ
[
x
0
x
1
...x
n
]
wtedyitylkowtedy,gdydladowolnegociągu
x
0
,x
1
,...,x
q
zachodzi
M|
=
ϕ
(
v
i
/v
l
)[
x
0
x
1
...x
q
]
.
Ostateczniewięcjeżelidladowolnegociągu
x
0
,x
1
,...,x
n
zachodzi
M|
=
ϕ
[
x
0
x
1
...x
n
]
,
todladowolnegociągu
x
0
,x
1
,...,x
n
zachodzi
M|
=
ϕ
(
v
i
/t
)[
x
0
x
1
...x
m
]
.
TWIERDZENIE14.
Niech wszystkie zmienne wolne występujące w formułach
ϕ
i
φ
znajdująsięwciągu
v
0
,v
1
,...,v
n
.Dladowolnegomodelu
M
ido-
wolnegociągu
x
0
,x
1
,...,x
n
jeżeli
M|
=(
ϕ
⇒∀
v
i
.φ
)[
x
0
x
1
...x
n
]
,to
M|
=(
ϕ
⇒
φ
)[
x
0
x
1
...x
n
]
.
DOWÓD
Niech dla dowolnego modelu
M
i dowolnego ciągu
x
0
,x
1
,...,x
n
zachodzi
=(
ϕ
⇒∀
v
i
.φ
)[
x
0
x
1
...x
n
]
.
Niechdlapewnegomodelu
M
iciągu
x
0
,x
1
,...,x
n
niezachodzi
M|
M|
=(
ϕ
⇒
φ
)[
x
0
x
1
...x
n
]
.
Zatemzdefinicjispełnianiamamy,że
todladowolnegociągu
x
0
,x
1
,...,x
m
zachodzi
M|
ϕ
(
v
i
/t
)
daje,iżdladowolnegociągu
x
0
,x
1
,...,x
m
zachodzi
M|
Plik z chomika:
czarnaczek
Inne pliki z tego folderu:
wyklad.pdf
(697 KB)
tw_tarskiego.pdf
(144 KB)
13.pdf
(331 KB)
12.pdf
(255 KB)
11.pdf
(323 KB)
Inne foldery tego chomika:
Dokumenty
Galeria
mp3
Prywatne
Studia
Zgłoś jeśli
naruszono regulamin