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)

By pozbyć się negacji, żąglujemy formułkami:

∀

x

•

p(x) –>

∀

x

•

– p(x),

∀

x

•

– q(x)

Wypieprzając kwantyfikatory (zauważcie, że po
lewej stronie powinniśmy formalnie zapisać
podstawienie, my jednak to sobie darujemy)

– p(x') –> – p(x'), – q(x')

Zarówno po lewej i po prawej stronie istnieje ten
sam predykat, więc na tym etapie wszystko jest
w porządku.

∀

x

•

– p(x), –

∀

x

•

– q(x)

>

q(x)

Znowu – żąglerka:

–>

∀

x

•

– p(x),

∀

x

•

– q(x), q(x)

I zróbmy z kwantyfikatorami to, co daj Boże,
zrobimy z Huzarosem po egzaminie:

–> –p(x'), –q(x'), q(x)

Przeniesienie:

p(x'), q(x') –> q(x)

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

Wyjebmy na lewo:

∀

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