Zadanie 1 z laboratorium z Coqa. Termin wykonania:
28 marca 2002 Zadanie ma na celu wymodelowanie w Coqu intuicjonistycznego rachunku
zdań wraz z semantyką Kripkego i systemem dowodzenia -- gentzenowskim
rachunkiem sekwentów. Udowodnimy (udowodnicie :-) poprawność systemu
formalnego względem tej semantyki oraz napiszemy funkcję tłumaczącą
model formuł rachunku zdań na formuły Coqa.
1 Formuły rachunku zdań.
Mając dany zbior zmiennych X, zbiór formuł F definiujemy
następująco:
Ł Í G × G jest quasi porządkiem na G (czyli
relacją zwrotną i przechodnią)
|= Í G × X jest zachowywane przez Ł,
czyli
" xÎ X " gŁ g'
g|= xg'|= x
W powyższej trójce G zwane jest zbiorem światów, relacja
Ł to relacja następstwa światów, gdzie g Ł h oznacza
intuicyjnie, że h jest możliwą przyszłością dla g, lub po
prostu następnikiemg. Warunek trzeci powyższej definicji
oznacza, że jeśli zmienna zdaniowa x wystąpi w danym świecie,
to wystąpi również we wszystkich jego następnikach.
Określimy teraz relację spełniania, która dla struktury Kripkego
K=(G,Ł,|=) mówi, kiedy w strukturze K w stanie gÎ G
spełniona jest formuła F, co (lekko nadużywając notacji) oznaczać
będziemy przez K,g |= F lub po prostu g |= F. Relacja ta
określona jest przez indukcję po budowie F:
F=x Î X, to g |= F wttw g |= x (tutaj |=
oznacza trzeci element z definicji K),
F=^, to g Ź |=F,
F=AÚ B, to g |= F wttw g |= A lub g |=
B,
F=AŮ B, to g |= F wttw g |= A i g |=
B,
F=AŽ B, to g |= F wttw gdy dla każdego h t.że
gŁ h jeśli h|= A to h|= B.
Jeśli mówimy, że w K spełniona jest formuła F (co zapisujemy
K|= F), to oznacza to, że jest ona spełniona w każdym świecie
K. Zapis |= F oznacza, że F jest tautologią
intuicjonistycznego rachunku zdań, czyli, że jest prawdziwe w każdej
strukturze Kripkego (dla każdego K zachodzi K|= V).
3 Intuicjonistyczny rachunek sekwentów Gentzena
Sekwent to para, złożona ze zbioru formuł oraz formuły, zapisywana
G |- F. Intuicjonistyczny rachunek sekwentów Gentzena
zawiera jeden aksjomat oraz dla każdego spójnika logicznego,
odpowiadające mu reguły lewe i prawe, mówiące jak taki spójnik uzyskać
odpowiednio po lewej i prawej strone |-.
Uwaga! Notacja G,A oznacza tak naprawdę
G Č {A} i nic nie mówi o tym, czy A Î G, czy nie!
Aksjomat G, A |- A
Reguły:
^-lewa
G, ^ |- A
Ú-lewa
G, A |- C G, B |- C
G, A Ú B |- C
Ú-prawa1
G |- A
G |- AÚ B
Ú-prawa2
G |- B
G |- AÚ B
Ů-lewa1
G, A |- C
G, A Ů B |- C
Ů-lewa2
G, B |- C
G, A Ů B |- C
Ů-prawa
G |- A G |- B
G |- AŮ B
Ž-lewa
G, B |- C G |- A
G, AŽ B |- C
Ž-prawa
G, A |- B
G |- A Ž B
Jeżeli zachodzi |- A, to mówimy, że A jest twierdzeniem.
4 Polecenia
Sformalizować w Coqu typ reprezentujący formuły rachunku zdań.
Sformalizować semantykę Kripkego oraz podać kilka przykładów
ciekawych formuł oraz ciekawych struktur, w ktorych te formuły są
spełnione (i udowodnić to w Coqu).
Sformalizować rachunek sekwentów Gentzena, podać wyprowadzenie
sekwentu |- ((p Ú (pŽ^))Ž^)Ž^1 oraz kilku innych twierdzeń intuicjonistycznego
rachunku zdań.
Udowodnić poprawność systemu dowodzenia względem podanej
semantyki, tj.
Dla dowolnej formuły F, jeśli |- F,
to|= F
Napisać w Coqu funkcję F : (X Ž Prop) Ž
Formula Ž Prop, tłumaczącą termy typu Formuła
(z punktu 1), na formuły Coqa. Pierwszym argumentem funkcji F
jest wartościowanie zmiennych.
Funkcja F ma mieć następujące własności (dowiedzione w Coqu):
jeśli formuła jest zmienną x : X, to dla dowolnego v : X Ž
Prop zachodzi (F v (Var x)) Ť (vx)
jeśli formuła F jest twierdzeniem intuicjonistycznego rachunku
zdań, to dla dowolnego wartościowania v zachodzi (F vF).
jeśli zachodzi |- F Ž ^ to dla dowolnego
wartościowania v zachodzi ~(F vF)
Myślę, że rozwiązanie zadania nie powinno sprawić (zbyt dużych)
kłopotów. Jeśli znaleźlibyście w powyższej treści jakieś błędy, to
bardzo proszę o poinformowanie mnie o tym fakcie. Życzę powodzenia Jacek Chrząszcz, 28 lutego 2002 ostatnia zmiana: March 4, 2002