Rachunek sekwentów Gentzena dla rachunku kwantyfikatorów Opuszczę sobie nudne wprowadzenie, zakładam, że znacie sekwenty dla rachunku zdań i wiecie, jak się nimi obchodzić. Dla kwantyfikatorów sprawa lekko się rypie, ale nie do końca.
Wezmę przykład z książki Huzarosa:
Przykład
∀x• p(x) => ∃y • p(y)
Po „przetłumaczeniu” wygląda to mniej więcej tak: jeżeli dla każdego „x” jest spełniony jakiśtam predykat/warunek (gwoli wytłumaczenia – predykat to po prostu funkcja logiczna, formuła itp.
która daje prawdę albo fałsz), to jest spełniony dla jakiegośtam „y”. Jak się za to zabrać?
Może, żebyśmy nie mieli tutaj grochu z kapustą, zamieńmy se drugą część na kwantyfikator ogólny, zgodnie ze „wzorkiem”:
∃y • A = –∀y• –A
Po prostu – „odwracamy” kwantyfikator, dodajemy negację przed nim oraz dodajemy negację „w środku”.
So, nasz przykład wygląda tak:
∀x• p(x) –> – ∀y • p(y)
(tutaj znak implikacji zastąpiliśmy już tę, że się tak wyrażę, „strzałeczką normalną”, oznaczającą, że teraz bawimy się już w sekwenty).
Wyrażenie po prawej stronie możemy przenieść na lewą, zmieniając znak (analogicznie jak w np.
równaniach na matematyce):
∀x• p(x), ∀y • p(y) –>
I teraz: korzystamy z takiej śmiesznej właściwości... Chociaż szczerze się przyznam – nie wiem, czy to jest taka normalna właściwość, po prostu tak wywnioskowałem z przykładu w książce.
Mianowicie, po pierwsze, jak mamy po lewej stronie kwantyfikatory ogólne (bez negacji), to możemy je wyjebać, jednocześnie „zmieniając” sobie zmienną w predykatach (fachowo – zmienić wartościowanie) na taką, jaką nam się podoba. No dobra, zmienię se iksa na zeta, i igreka też se zamienię na zeta. Formalnie należy to zapisać tak (czemu się tutaj pojawił znaczek „prim”, o tym za chwilę):
p(x)[x::=z], p(y)[x::=z] –>
p(z'), p(z') –>
Teraz, przenosząc ten negatywny predykat z lewej na prawą, otrzymujemy coś takiego: p(z') –> p(z')
Sekwenty Gentzena dla RK
Autor: Verbox
1/5
I tutaj nie ma bata, jak po jednej stronie jest gówno, to jest i po drugiej, a jak po jednej stronie jest prawda, to i po drugiej musi być. To jest właśnie ukryty mechanizm sekwentów – pokazać, że np.
taki Huzaros może być jednocześnie dobry i zły. Jak się dojdzie właśnie do takiego wniosku, że Huzaros musi być jednocześnie dobry i zły (znaczy się – po obydwu stronach będzie to samo), to znaczy, że cały sekwent, że się tak wyrażę, jest „prawdziwy”. Po prostu – jeżeli po obydwu stronach będzie to samo, to przykład jest tautologią.
I teraz najważniejsza chyba uwaga. Jeżeli wypieprzamy kwantyfikator, to te zmienne, które nam
zostają, to są tak naprawdę „udawane” (obojętnie, czy kwantyfikator jest wywalany z lewej, czy z
prawej, o czym za chwilę). Nie ma problemu, jeżeli po obydwóch stronach są udawane. Ale warto
sobie te zmienne „udawane” oznaczać np. znaczkiem prim (').
Rozpatrzmy drugi przykład z książki:
Przykład
∃y • p(y) => ∀x• p(x)
Wydaje się „fajnie, to samo, więc jest prawdziwe, więc kończymy flaszkę, egzamin i idziemy do domu”. Jednak, niestety, nie jest to samo.
Zmieńmy se lewą część sekwentu, zgodnie z wcześniejszym wzorem zamiany kwantyfikatora szczegółowego (a może się pisze „szczególnego”? Mniejsza z tym) na kwantyfikator ogólny. Więc po zamianie:
– ∀y • p(y) –> ∀x• p(x)
Wykopmy lewą część na prawą (by pozbyć się znaku negacji przed kwantyfikatorem):
–> ∀x• p(x) , ∀y • p(y)
Jeżeli mamy kwantyfikatory ogólne po prawej stronie, to te śmieszne znaczki kwantyfikatorów również możemy wypierdolić na łono Abrahama. Ale... Ale... właśnie, nie ma najlepszej części –
nie możemy se niestety zmienić zmiennej na takiej, jaka nam odpowiada, jednakże – odznaczmy, że ona jest lipna. Niestety, to tam nieco chyba pokrzyżuje plany:
–>p(x') , p(y')
„Prawy do lewego”:
p(y') –> p(x')
Jak widzimy, w tej samej funkcji logicznej mamy dwie różne zmienne, które mogą dać różny efekt.
By to lepiej wytłumaczyć, załóżmy, że p(x) oznacza taką funkcję logiczną: x > 0
Patrzcie, jak podstawicie sobie za iksa cokolwiek, to możecie stwierdzić, że te całe powyższe porównanie jest prawdziwe lub fałszywe.
Sekwenty Gentzena dla RK
Autor: Verbox
2/5
A więc jeżeli na przykład za igreka podstawię 2 (pisze gdzieś, że mi nie wolno? Wolno), a za iksa minus 666, to lewa strona będzie prawdziwa, a prawa fałszywa. Naszą implikację idzie o kant dupy roztłuc, bo będzie bullshitem. A tautologia musi być zawsze prawdziwa, obojętnie, co sobie wymyślimy.
No dobra, ktoś powie „to czemu sobie w pierwszy przykładzie dopasowałeś tak zmienne, żeby pasowało”? Odpowiadam – bo tak wolno, jak mam kwantyfikator (w tym i w następnym akapicie mam na myśli kwantyfikatory ogólne) po lewej stronie, to mogę mu nawet powiedzieć, że jego stara rwie rzepę w Familiadzie. Kwantyfikatory po lewej stronie są tolerancyjne, pozwalają na dowolną „podmianę” zmiennej. „Wiedzą”, że teoretycznie tego nie wolno, ale przymykają na to oko.
Natomiast te po prawej stronie sekwentu są formalistami. Owszem, pozwalają się wydymać w dupsko i odejdą z niesmakiem, ale na „odchodne” nie pozwalają na mieszanie w zmiennych.
Zróbmy sobie jakieś zadanko z listy zadań:
Przykład (zadanie 4, lista 7)
a)
(∃x • p(x)) ⇒ p(x)
Więc dobra, jesteśmy wielkimi przeciwnikami szczegółów, więc zróbmy porządek z kwantyfikatorem:
–
∀x• p(x) –> p(x)
Przeniesienie:
–> ∀x• p(x), p(x)
Wyrzucenie kwantyfikatora (pamiętajmy, że jest po prawej stronie sekwentu, więc nie możemy oszukiwać):
–> –p(x'), p(x)
Przeniesienie predykatu – p(x'):
p(x') –> p(x)
Niestety, tutaj mamy do czynienia z konfrontacją „udawanej” (po zniknięciu kwantyfikatora) zmiennej x z „prawdziwą”. Niestety, łatwo można nas nakryć na kłamstwie, więc to niestety nie jest tautologia (co było do wykazania)
d)
(∃x • p(x)) ∧ (∃x • q(x)) ⇒ (∃x • p(x) ∧ q(x))
Oj, będzie się działo. Najpierw zapis „sekwencyjny”:
(∃x • p(x)) ∧ (∃x • q(x)) > ∃ x •
p(x) ∧ q(x)
(Dla przejrzystości używam podkreślenia po prawej stronie, żeby odróżnić dwie, rózne bądź
co bądź, formuły)
Sekwenty Gentzena dla RK
Autor: Verbox
3/5
Nie, jeszcze nie zmieniamy kwantyfikatorów. Napierw załóżmy, że te dwa wielkie chuje po lewej stronie to po prostu jakieś funkcje logiczne z prawa rachunku zdań. Wiemy, że jeżeli mamy koniunkcję po lewej stronie (z rachunku Gentzena dla rachunku zdań), to możemy ją z czystym sumieniem wypierdolić, wstawiając po prostu dwa twory, które były w tej koniunkcji.
∃x • p(x), ∃x • q(x) > ∃ x •
p(x) ∧ q(x)
To teraz spokojnie możemy już zrobić sobie dobrze:
∀ x • – p(x), – ∀x • – q(x) > –
∀
x •
p(x)
∧ q(x)
Jeżeli mamy koniunkcję z prawej strony, to niestety, musimy cały sekwent rozmnożyć na dwa, raz zastępując prawą część sekwentu jedną częścią koniunkcji, a raz drugą częścią. Dlatego dalsze kroki:
∀ x • – p(x), – ∀x • – q(x) > – ∀x • p(x) ∀ x • – p(x), – ∀x • – q(x) > q(x) By pozbyć się negacji, żąglujemy formułkami:
Znowu – żąglerka:
∀x • p(x) –> ∀x • – p(x), ∀x • – q(x)
–> ∀x • – p(x), ∀x • – q(x), q(x)
Wypieprzając kwantyfikatory (zauważcie, że po I zróbmy z kwantyfikatorami to, co daj Boże, lewej stronie powinniśmy formalnie zapisać
zrobimy z Huzarosem po egzaminie:
podstawienie, my jednak to sobie darujemy)
–> –p(x'), –q(x'), q(x)
– p(x') –> – p(x'), – q(x')
Przeniesienie:
Zarówno po lewej i po prawej stronie istnieje ten
sam predykat, więc na tym etapie wszystko jest p(x'), q(x') –> q(x) w porządku.
Niestety, formalnie, to my tutaj mamy dwie
różne zmienne. Dlatego nie ma tutaj ani
jednej wspólnej części. Jeżeli gdzieś, rysując
te całe drzewko, trafimy na taki kawałek,
gdzie po obydwu stronach nie znajdziemy tej
samej części – przykro mi, na pewno nie
znajdziemy tutaj tautologii.
Na koniec, spójrzmy na taki przykład:
∀x• p(x) –> ∃x • p(x)
Intuicyjnie możemy sobie odpowiedzieć, że to jest tautologia. No bo jeżeli każdy student pije, to wiadomo, że znajdzie się chociaż jeden, który pije. Ale to nie jest chemia, tylko nielogika, więc pomieszajmy. Zamieńmy se prawy kwantyfikator:
∀x• p(x) –> – ∀x • p(x)
Sekwenty Gentzena dla RK
Autor: Verbox
4/5
∀x• p(x), ∀x • p(x) –>
I tutaj widzimy, że nawet specjalnie nie musimy oszukiwać, ale zróbmy to dla formalności: p(x)[x::=x], p(x)[x::=x] –>
p(x') –> p(x')
No, tutaj ładnie wychodzi nam tautologia, bjutiful, co zresztą jest zgodne z prawdą.
A teraz taki:
∃ x • p(x) –> ∀ x• p(x)
Ten kwantyfikator po lewej mi się nie podoba:
– ∀ x • p(x) –> ∀ x• p(x)
–> ∀ x• p(x), ∀ x • p(x)
–> p(x'), – p(x')
p(x') –> p(x')
Niestety, nie doszedłem jeszcze, czemu tutaj wychodzi tautologia, chociaż teoretycznie nie powinna.
Jak znajdę odpowiedź (albo Wy to zrobicie), to na pewno dam znać.
Sekwenty Gentzena dla RK
Autor: Verbox
5/5